Theorem darii
"Darii", one of the syllogisms of Aristotelian logic. All \( \varphi \) is
\( \psi \), and some \( \chi \) is \( \varphi \), therefore some \( \chi \) is \( \psi \).
In Aristotelian notation, AII-1: MaP and SiM therefore SiP. For
example, given "All rabbits have fur" and "Some pets are rabbits",
therefore "Some pets have fur". Example from
https://en.wikipedia.org/wiki/Syllogism. See dariiALT for a
shorter proof requiring more axioms. (Contributed by David A. Wheeler,
24-Aug-2016.) Reduce dependencies on axioms. (Revised by BJ,
16-Sep-2022.)
Hypotheses
darii.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
darii.min
\( \vdash \exists x \, (\chi \wedge \varphi) \)
Conclusion
\( \vdash \exists x \, (\chi \wedge \psi) \)
Proof
l0
darii.maj
\( \vdash \forall x \, (\varphi \rightarrow \psi) \)
id
anim2d _
alimi _
\( \vdash \forall x \, (\varphi \rightarrow \psi) \rightarrow \forall x \, (\chi \wedge \varphi \rightarrow \chi \wedge \psi) \)
l4
ax-mp l0 _
\( \vdash \forall x \, (\chi \wedge \varphi \rightarrow \chi \wedge \psi) \)
l5
darii.min
\( \vdash \exists x \, (\chi \wedge \varphi) \)
exim
\( \vdash \forall x \, (\chi \wedge \varphi \rightarrow \chi \wedge \psi) \rightarrow \exists x \, (\chi \wedge \varphi) \rightarrow \exists x \, (\chi \wedge \psi) \)
mp2 l4 l5 _