Theorem fesapo
"Fesapo", one of the syllogisms of Aristotelian logic. No \( \varphi \) is
\( \psi \), all \( \psi \) is \( \chi \), and \( \psi \) exist, therefore some \( \chi \)
is not \( \varphi \). In Aristotelian notation, EAO-4: PeM and MaS therefore
SoP. (Contributed by David A. Wheeler, 28-Aug-2016.) Reduce
dependencies on axioms. (Revised by BJ, 16-Sep-2022.)
Hypotheses
fesapo.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
fesapo.min
\( \vdash \forall x \, (\psi \rightarrow \chi) \)
fesapo.e
\( \vdash \exists x \, \psi \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \neg \varphi) \)
Proof
l0
fesapo.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
con2
alimi _
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \rightarrow \forall x \, (\psi \rightarrow \neg \varphi) \)
l3
ax-mp l0 _
\( \vdash \forall x \, (\psi \rightarrow \neg \varphi) \)
l4
fesapo.min
\( \vdash \forall x \, (\psi \rightarrow \chi) \)
fesapo.e
\( \vdash \exists x \, \psi \)
felapton l3 l4 _