Prove the introduction of conjunction using axioms in a Hilbert system

Question

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.

Answer 1

Thanks to the hints and further guidance from Mauro, I've finally managed to solve this! The full proof would be way too long to include here in an answer (as it turns out, proofs that avoid the use of the deductivity theorem turn out to become much longer), but it can be found in the following gist:
https://gist.github.com/Isti115/fbc66bd20901c2d209fe0185c62b4afe#file-hilbert-agda-L428

The link should point to the line number, but in case it does not, just search for ∧-intro.

Answer 2

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.

Answer 3

First, we shall write the axioms in the following way: $$I: a → a,\quad K: a → b → a,\quad S: (a → b → c) → (a → b) → a → c,$$ adopting the usual convention that bracketing occurs to the right, i.e. $a → b → c = a → (b → c)$.

Second, given proofs $f: a → b$ and $g: a$, we shall denote the application of modus ponens as $f g: b$, adopting the usual convention that bracketing for products occurs to the left, i.e. $fgh = (fg)h$.

This is motivated by the Curry-Howard Correspondence. As part of that correspondence we note that the following equivalences of proofs: $$I x = x,\quad K x y = x,\quad S x y z = x z (y z),$$ which you can verify by writing each set out, using the conventions just described.

The deduction theorem, under this correspondence, asserts that if $f x = g x$, where $x$ is independent of $f$ and $g$, then $f = g$. This corresponds to the η-rule, or "extensionality". In particular, we note that $$S K x y = K y (x y) = y = I y,$$ therefore $S K x = I$, for any $x$. The usual choice made is $x = K$, with $I = S K K$ taken as a definition. When written out as a proof, $S K x$ takes on the form $$\begin{align} S:& (a → b → c) → (a → b) → a → c,\\ K:& a → b → a,\\ S K:& (a → b) → a → c,\\ x:& a → b,\\ S K x:& a → c, \end{align}$$ where the constraint $a = c$ arises from making $S K$ fit to modus ponens in the third step; thus yielding the result $S K x: a → a$.

Other useful theorems may be established similarly as follows: $$ B = S (K S) K: (b → c) → (a → b) → a → c,\\ C = S (B B S) (K K): (a → b → c) → b → a → c,\\ W = S S (K I): (a → a → b) → a → b, $$ with the corresponding equivalences $$B x y z = x (y z),\quad C x y z = x z y,\quad W x y = x y y,$$ derivable from the definitions.

We can do composition with $B$, noting that if $φ: α → β$ and $ψ: β → γ$, then $B ψ φ: α → γ$. We can also use $C$ as an operator two swap the order of hypotheses, so that if $φ: α → β → γ$, then $C φ: β → α → γ$. This can be used to reverse the order of composition, as: $CBfg = Bgf$.

We can also use $B$ on a single argument to extend an implication to the right. Thus, if $φ: α → β$, then $Bφ: (γ → α) → γ → β$. To extend to the right, we use $CB$ instead: $CBφ: (β → γ) → α → γ$. Note that this reverses $α$ and $β$ since they're now on the "negative" side of the implication operator "$→$".

The additional axiom will be denoted $$Z: (¬a → ¬b) → b → a.$$ For the following, the definition $¬a = a → ⊥$ won't be needed. The rule of contradiction is, effectively, given by $$V = B Z K: ¬a → a → b,$$ and the double-negative rules are given by $$N = S (B Z V) I: ¬¬a → a,\quad Z N: a → ¬¬a.$$

The result you're seeking is $$f: a → b → a ∧ b = ¬(¬a ∨ ¬b) = ¬(¬¬a → ¬b).$$ This can be written as a composition with $Z$: $f = B g Z$, where $$g: a → ¬¬(¬¬a → ¬b) → ¬b.$$ In turn, this can be written as the result of swapping the first two hypotheses, using $C$: $g = C h$, where $$h: ¬¬(¬¬a → ¬b) → a → ¬b.$$ This can be arrived at as the composition $h = B k N$, of the double negative rule $N$ with $k$, where $$k: (¬¬a → b) → a → ¬b.$$ This is just the converse double negative rule $ZN$ extended to the right: $k = CB(ZN)$. Thus $$f = B g Z = B (C h) Z = B (C (B k N)) Z = B (C (B (C B (Z N)))) Z,$$ where $$N = S (B Z V) I,\quad V = B Z K.$$

Running this in Combo, which I put up on GitHub not too long ago, as the expression $$ V = B Z K,\quad N = S (B Z V) I,\quad k = C B (Z N),\quad h = B k N,\quad g = C h,\quad f = B g Z,\quad f$$ and turning on extensionality, the following is the result $$\_0 = B Z,\quad \_1 = W (\_0 (\_0 K)),\quad B (C \_1) (B (Z \_1) Z).$$

That effectively calls out lemma $\_0$ for $B Z$, lemma $\_1$ for $W (\_0 (\_0 K))$ with the result being $B (C \_1) (B (Z \_1) Z)$.

This can be reduced to just $SKI$ form, if you wish, by making use of the following equivalences (proven using extensionality): $$B x = S (K x),\quad C x y = S x (K y),\quad W x = S x I,\quad C x = B (S x) K = S (K (S x)) K.$$ Then we have $$\_0 = S (K Z),\quad \_1 = S (\_0 (\_0 K)) I,\quad \_2 = S (K (S \_1)) K,\quad S (K \_2) (S (K (Z \_1)) Z).$$

The number of lines in a proof is $2n - 1$, where $n$ is the total number of $SKIZ$'s. The $SKIZ$-counts are: $3$ for $\_0$, $3 + 2×3 = 9$ for $\_1$, $4 + 9 = 13$ for $\_2$ and $6 + 9 + 13 = 28$ for the main result, for a total of $55$ lines.