(* Title: Aristotle's Assertoric Syllogistic Author: Angeliki Koutsoukou-Argyraki, University of Cambridge. October 2019 We formalise with Isabelle/HOL some basic elements of Aristotle's assertoric syllogistic following the article from the Stanford Encyclopedia of Philosophy by Robin Smith: https://plato.stanford.edu/entries/aristotle-logic/. To this end, we use a set theoretic formulation (covering both individual and general predication). In particular, we formalise the deductions in the Figures and after that we present Aristotle's metatheoretical observation that all deductions in the Figures can in fact be reduced to either Barbara or Celarent. As the formal proofs prove to be straightforward, the interest of this entry lies in illustrating the functionality of Isabelle and high efficiency of Sledgehammer for simple exercises in philosophy.*) section‹Aristotle's Assertoric Syllogistic› theory AristotlesAssertoric imports Main begin subsection‹Aristotelean Categorical Sentences› text‹ Aristotle's universal, particular and indefinite predications (affirmations and denials) are expressed here using a set theoretic formulation. Aristotle handles in the same way individual and general predications i.e. he gives the same logical analysis to "Socrates is an animal" and "humans are animals". Here we define the general predication i.e. predications are defined as relations between sets. This has the benefit that individual predication can also be expressed as set membership (e.g. see the lemma SocratesMortal). › definition universal_affirmation :: "'a set ⇒'a set ⇒ bool" (infixr "Q" 80) where "A Q B ≡ ∀ b ∈ B . b ∈ A " definition universal_denial :: "'a set ⇒'a set ⇒ bool" (infixr "E" 80) where "A E B ≡ ∀ b ∈ B. ( b ∉ A) " definition particular_affirmation :: " 'a set ⇒'a set ⇒ bool" (infixr "I" 80) where "A I B ≡ ∃ b ∈ B. ( b ∈ A) " definition particular_denial :: "'a set ⇒'a set ⇒ bool" (infixr "Z" 80) where "A Z B ≡ ∃ b ∈ B. ( b ∉ A) " text‹ The above four definitions are known as the "square of opposition".› definition indefinite_affirmation :: " 'a set ⇒'a set ⇒ bool" (infixr "QI" 80) where "A QI B ≡(( ∀ b ∈ B. (b ∈ A)) ∨ (∃ b ∈ B. (b ∈ A))) " definition indefinite_denial :: "'a set ⇒'a set ⇒ bool" (infixr "EZ" 80) where "A EZ B ≡ (( ∀ b ∈ B. (b ∉ A)) ∨ (∃ b ∈ B. (b ∉ A))) " lemma aristo_conversion1 : assumes "A E B" shows "B E A" using assms universal_denial_def by blast lemma aristo_conversion2 : assumes "A I B" shows "B I A" using assms unfolding particular_affirmation_def by blast lemma aristo_conversion3 : assumes "A Q B" and "B ≠{} " shows "B I A" using assms unfolding universal_affirmation_def particular_affirmation_def by blast text‹Remark: Aristotle in general supposes that sets have to be nonempty. Indeed, we observe that in many instances it is necessary to assume that the sets are nonempty, otherwise Isabelle's automation finds counterexamples.› subsection‹The Deductions in the Figures ("Moods")› text‹The medieval mnemonic names are used.› subsubsection‹First Figure› lemma Barbara: assumes "A Q B " and "B Q C" shows "A Q C" by (meson assms universal_affirmation_def) lemma Celarent: assumes "A E B " and "B Q C" shows "A E C" by (meson assms universal_affirmation_def universal_denial_def) lemma Darii: assumes "A Q B" and "B I C" shows "A I C" by (meson assms particular_affirmation_def universal_affirmation_def) lemma Ferio: assumes "A E B" and "B I C" shows "A Z C" by (meson assms particular_affirmation_def particular_denial_def universal_denial_def) subsubsection‹Second Figure› lemma Cesare: assumes "A E B " and "A Q C" shows "B E C" using Celarent aristo_conversion1 assms by blast lemma Camestres: assumes "A Q B " and "A E C" shows "B E C " using Cesare aristo_conversion1 assms by blast lemma Festino: assumes "A E B " and "A I C" shows "B Z C " using Ferio aristo_conversion1 assms by blast lemma Baroco: assumes "A Q B " and "A Z C" shows "B Z C " by (meson assms particular_denial_def universal_affirmation_def) subsubsection‹Third Figure› lemma Darapti: assumes "A Q C " and "B Q C" and "C ≠{}" shows "A I B " using Darii assms unfolding universal_affirmation_def particular_affirmation_def by blast lemma Felapton: assumes "A E C" and "B Q C" and "C ≠{}" shows "A Z B" using Festino aristo_conversion1 aristo_conversion3 assms by blast lemma Disamis: assumes "A I C" and "B Q C" shows "A I B" using Darii aristo_conversion2 assms by blast lemma Datisi: assumes "A Q C" and "B I C" shows "A I B" using Disamis aristo_conversion2 assms by blast lemma Bocardo: assumes "A Z C" and "B Q C" shows "A Z B" by (meson assms particular_denial_def universal_affirmation_def) lemma Ferison: assumes "A E C " and "B I C" shows "A Z B " using Ferio aristo_conversion2 assms by blast subsubsection‹Examples› text‹Example of a deduction with general predication.› lemma GreekMortal : assumes "Mortal Q Human" and "Human Q Greek " shows " Mortal Q Greek " using assms Barbara by auto text‹Example of a deduction with individual predication.› lemma SocratesMortal: assumes "Socrates ∈ Human " and "Mortal Q Human" shows "Socrates ∈ Mortal " using assms by (simp add: universal_affirmation_def) subsection‹Metatheoretical comments› text‹The following are presented to demonstrate one of Aristotle's metatheoretical explorations. Namely, Aristotle's metatheorem that: "All deductions in all three Figures can eventually be reduced to either Barbara or Celarent" is demonstrated by the proofs below and by considering the proofs from the previous subsection. › lemma Darii_reducedto_Camestres: assumes "A Q B " and "B I C" and "A E C " (*assms, concl. of Darii and A E C *) shows "A I C" proof- have "B E C" using Camestres ‹ A Q B › ‹A E C› by blast show ?thesis using ‹ B I C › ‹B E C› by (simp add: particular_affirmation_def universal_denial_def) qed text‹It is already evident from the proofs in the previous subsection that: Camestres can be reduced to Cesare. Cesare can be reduced to Celarent. Festino can be reduced to Ferio.› lemma Ferio_reducedto_Cesare: assumes "A E B " and "B I C" and "A Q C " (*assms, concl. of Ferio and A Q C *) shows "A Z C" proof- have "B E C" using Cesare ‹A E B › ‹A Q C› by blast show ?thesis using ‹B I C › ‹B E C› by (simp add: particular_affirmation_def universal_denial_def) qed lemma Baroco_reducedto_Barbara : assumes "A Q B " and " A Z C " and " B Q C " shows "B Z C" (*assms , concl. of Baroco and B Q C *) proof- have "A Q C" using ‹A Q B › ‹ B Q C › Barbara by blast show ?thesis using ‹A Q C› ‹ A Z C › by (simp add: particular_denial_def universal_affirmation_def) qed lemma Bocardo_reducedto_Barbara : assumes " A Z C" and "B Q C" and "A Q B" shows "A Z B" (*assms, concl of Bocardo and A Q B *) proof- have "A Q C" using ‹B Q C› ‹ A Q B› using Barbara by blast show ?thesis using ‹A Q C› ‹ A Z C› by (simp add: particular_denial_def universal_affirmation_def) qed text‹Finally, it is already evident from the proofs in the previous subsection that : Darapti can be reduced to Darii. Felapton can be reduced to Festino. Disamis can be reduced to Darii. Datisi can be reduced to Disamis. Ferison can be reduced to Ferio. › text‹In conclusion, the aforementioned deductions have thus been shown to be reduced to either Barbara or Celarent as follows: Baroco $\Rightarrow$ Barbara Bocardo $\Rightarrow$ Barbara Felapton $\Rightarrow$ Festino $\Rightarrow$ Ferio $\Rightarrow$ Cesare $\Rightarrow$ Celarent Datisi $\Rightarrow$ Disamis $\Rightarrow$ Darii $\Rightarrow$ Camestres $\Rightarrow$ Cesare Darapti $\Rightarrow$ Darii Ferison $\Rightarrow$ Ferio › subsection‹Acknowledgements› text‹A.K.-A. was supported by the ERC Advanced Grant ALEXANDRIA (Project 742178) funded by the European Research Council and led by Professor Lawrence Paulson at the University of Cambridge, UK. Thanks to Wenda Li.› subsection‹Bibliography› text‹Smith, Robin, "Aristotle's Logic", The Stanford Encyclopedia of Philosophy (Summer 2019 Edition), Edward N. Zalta (ed.), URL = @{url "https://plato.stanford.edu/archives/sum2019/entries/aristotle-logic/"} › end