Abstract
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. 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.