Prove the introduction of conjunction using axioms in a Hilbert system

hilbert-calculuslogic

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:

$(\alpha \to (\beta \to \lnot (\alpha \to \lnot \beta)))$.

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.

Related Question