Email Gateway (Aug 22 2022 at 20:45): Email Gateway (Aug 22 2022 at 20:45):From: Tobias Nipkow <nipkow@in.tum.de>
Aristotle's Assertoric Syllogistic
Angeliki Koutsoukou-Argyraki
We formalise with Isabelle/HOL some basic elements of Aristotle's assertoric
syllogistic following the <a
href="https://plato.stanford.edu/entries/aristotle-logic/">article from the
Stanford Encyclopedia of Philosophy by Robin Smith.</a> 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.
https://www.isa-afp.org/entries/Aristotles_Assertoric_Syllogistic.html
Enjoy!
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC