Theorem festino
"Festino", one of the syllogisms of Aristotelian logic. No \( \varphi \) is
\( \psi \), and some \( \chi \) is \( \psi \), therefore some \( \chi \) is not
\( \varphi \). In Aristotelian notation, EIO-2: PeM and SiM therefore SoP.
(Contributed by David A. Wheeler, 25-Nov-2016.) Reduce dependencies on
axioms. (Revised by BJ, 16-Sep-2022.)
Hypotheses
festino.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
festino.min
\( \vdash \exists x \, (\chi \wedge \psi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \neg \varphi) \)
Proof
l0
festino.maj
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \)
con2
anim2d _
alimi _
\( \vdash \forall x \, (\varphi \rightarrow \neg \psi) \rightarrow \forall x \, (\chi \wedge \psi \rightarrow \chi \wedge \neg \varphi) \)
l4
ax-mp l0 _
\( \vdash \forall x \, (\chi \wedge \psi \rightarrow \chi \wedge \neg \varphi) \)
l5
festino.min
\( \vdash \exists x \, (\chi \wedge \psi) \)
exim
\( \vdash \forall x \, (\chi \wedge \psi \rightarrow \chi \wedge \neg \varphi) \rightarrow \exists x \, (\chi \wedge \psi) \rightarrow \exists x \, (\chi \wedge \neg \varphi) \)
mp2 l4 l5 _