Theorem baroco
"Baroco", one of the syllogisms of Aristotelian logic. All \( \varphi \) is
\( \psi \), and some \( \chi \) is not \( \psi \), therefore some \( \chi \) is not
\( \varphi \). In Aristotelian notation, AOO-2: PaM and SoM therefore SoP.
For example, "All informative things are useful", "Some websites are not
useful", therefore "Some websites are not informative". (Contributed by
David A. Wheeler, 28-Aug-2016.) Reduce dependencies on axioms.
(Revised by BJ, 16-Sep-2022.)
Hypotheses
baroco.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
baroco.min
\( \vdash \exists x \, (\chi \wedge \neg \psi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \neg \varphi) \)
Proof
l0
baroco.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
con3
anim2d _
alimi _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, (\chi \wedge \neg \psi \rightarrow \chi \wedge \neg \varphi) \)
l4
ax-mp l0 _
\( \vdash \forall x \, (\chi \wedge \neg \psi \rightarrow \chi \wedge \neg \varphi) \)
l5
baroco.min
\( \vdash \exists x \, (\chi \wedge \neg \psi) \)
exim
\( \vdash \forall x \, (\chi \wedge \neg \psi \rightarrow \chi \wedge \neg \varphi) \rightarrow \exists x \, (\chi \wedge \neg \psi) \rightarrow \exists x \, (\chi \wedge \neg \varphi) \)
mp2 l4 l5 _