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

### License

BSD License

### Topics

- Logic/Philosophical aspects

### Session Aristotles_Assertoric_Syllogistic

- AristotlesAssertoric

## Cite

×

Aristotles_Assertoric_Syllogistic-AFP

    @article{Aristotles_Assertoric_Syllogistic-AFP,
      author  = {Angeliki Koutsoukou-Argyraki},
      title   = {Aristotle's Assertoric Syllogistic},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2019},
      note    = {\url{https://isa-afp.org/entries/Aristotles_Assertoric_Syllogistic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Oct 17, 2019 : Isabelle2019