Theory AristotlesAssertoric

(*
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