# Prove the introduction of conjunction using axioms in a Hilbert system

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.

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.

• Thank you very much for the hint! :) I formalized the system in Agda and got some help from the auto solver in proving the ¬-intro tautology, but I cannot figure out a way to implement a proof for the Deduction theorem. Can that be done formally? Commented Apr 29, 2020 at 13:35
• @Isti115 - no; the DT is a meta-theorem, i.e. a "rule" about the calculus and not in the calculus. Of course, we can avoid it... Commented Apr 29, 2020 at 13:40
• But there has to be a way in which proofs that use the DT can be converted to proofs without it, right? In that case that could be implemented. (I don't know if you are familiar with Agda, or some other implementations of Type Theory, but I think that the way I formalized the system allows meta-reasoning as well.) Commented Apr 29, 2020 at 13:41
• @Isti115 - here you can find an wxample of how to avoid DT. Commented Apr 29, 2020 at 14:15
• @Isti115 Of course, since Agda is such a powerful system, it provides you with everything you need to prove the deduction theorem. Here, Agda acts as the meta-logic. You can simply do a dependent pattern matching on the proof object, and follow the proof of the deduction theorem on most logic books, and you're done! Commented May 8, 2020 at 3:48

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.

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.