Given a Hilbert system with the axioms (and of course the Modus Ponens):
$
A1.\ \phi \to \phi \\
A2.\ \phi \to ( \psi \to \phi ) \\
A3.\ ( \phi \to ( \psi \to \xi )) \to (( \phi \to \psi ) \to ( \phi \to \xi )) \\
A4.\ ( \lnot \phi \to \lnot \psi ) \to ( \psi \to \phi ) \\
-\\
MP.\ \phi \to \psi \; , \; \phi \; \vdash \; \psi
$
I would like to prove the introduction of conjunction $(\alpha \to (\beta \to (\alpha \land \beta)))$ where the logical operators are all defined in terms of implication:
- $ \lnot \phi = \phi \to \bot $
- $ \phi \lor \psi = \lnot \phi \to \psi $
- $ \phi \land \psi = \lnot (\lnot \phi \lor \lnot \psi) $
I have already managed to prove one of the introductions of disjunction $(\alpha \to (\beta \to (\alpha \lor \beta)))$ as practice, but cannot find the solution to conjunction.
$
\begin{alignat}{3}
&1.\ \beta \to ((\alpha \to \bot) \to \beta)
\; && [A2] \; (\phi || \beta \;,\; \psi || (\alpha \to \bot)) \\
&2.\ \beta \to ((\alpha \to \bot) \to \beta)) \to (\alpha \to (\beta \to ((\alpha \to \bot) \to \beta))
\; && [A2] \; (\phi || 1. \;,\; \psi || \alpha) \\
&3.\ \alpha \to (\beta \to ((\alpha \to \bot) \to \beta))
\; && [MP] \; (\phi || 2. \;,\; \psi || 1.)
\end{alignat}
$
Any help would be appreciated! I think that it should be doable, since it is supposed to be only a conservative extension of the core system.
Best Answer
Hint
What you have to prove is:
In order to do this, you have to prove negation introduction: $(\phi \to \psi) \to ((\phi \to \lnot \psi) \to \lnot \phi)$.
Using it we have:
1) $\alpha, \beta, \alpha \to \lnot \beta \vdash \beta$
2) $\alpha, \beta, \alpha \to \lnot \beta \vdash \lnot \beta$ --- by MP
3) $\alpha, \beta \vdash \lnot (\alpha \to \lnot \beta)$ --- using the law above.
The result follows by Deduction Theorem.