Deductions in Hilbert Systems

Hilbert systems are systems of deduction based on a large set of axioms and a minimal set of inference rules. Since deductions in Hilbert systems can be very hard to come up with, I will discuss some tips and tricks that I learned when I tried to solve this problem in Troelstra’s Basic Proof Theory:¹

Prove that the following two sets of axioms are equivalent.²
System $A$:

1. $P \imp (Q \imp P)$
2. $(P \imp Q \imp R) \imp (P \imp Q) \imp (P \imp R)$

System $B$:

3. $A \imp (B \imp A)$ (identical to 1)
4. $(A \imp A \imp B) \imp (A \imp B)$ (Contraction)
5. $(A \imp B) \imp (C \imp A) \imp (C \imp B)$ (Pseudo-Transitivity)³
6. $(A \imp B \imp C) \imp (B \imp A \imp C)$ (Permutation)

The only inference rules available are Modus Ponens (MP; also called $\imp$-Elimination).⁴

Note that here, we use the convention that $\imp$ is right associative, meaning

$A \imp B \imp C \equiv (A \imp (B \imp C))$

We may drop or add parenthesis so long that it does not change the structure of the formulas. For a conditional of the form $\phi \imp (\psi \imp \chi)$, we say that the (first and second) antecedents are $\phi$ and $\psi$, and the consequent is $\chi$.

Proving Principle of Identity

For practice, consider proving $A \imp A$ (the principle of identity) in the first system. How do we approach this?

We start by fitting the formula into the last part of the axioms. We have two options:
Try axiom 1: $(A \imp A) \imp\ ?\ \imp (A \imp A)$
or axiom 2: $(A \imp\ ?\ \imp A) \imp\ (A \imp\ ?\ ) \imp (A \imp A)$

Axiom 1 isn’t usually useful, because if we want to use Modus Ponens to get the final consequent, we must apply the antecedents in order, but its first antecedent is precisely what we want to prove!

So, let’s go with axiom 2. What should we substitute in for the question mark? In order to use Modus Ponens, we know that the antecedents must be theorems. It is not hard to see, then, that if we substitute $A \rightarrow A$ itself, then both antecedents are theorems. So, we have the following proof:

We are now ready to tackle the problem presented earlier. Although there is a solution in the book, it utilizes the fact that the first system was proved to be equivalent a Natural Deduction system. Here, we present a more direct proof by deriving each axiom from the other system.

Proving System B from System A

We prove that axioms 4, 5, and 6 are provable from 1 and 2.

Contraction (Axiom 4)

Contraction: $(A \imp A \imp B) \imp (A \imp B)$

Contraction seems easy to prove, as it fits the last part of axiom 2 (Let $P$ be $A$, $Q$ be $A\imp B$, and $R$ be $B$). Once we see that, we almost have a proof:

But we need to fill in the rule at line 2. We know we are on the right track because $A \imp (A \imp B) \imp B$ looks provable——it is just a conditional form of Modus Ponens!

We start the proof by observing that $(A\imp B)\imp B$ fits the consequent of axiom 2. This may seem weird, because the first $A$ of $A \imp ((A \imp B) \imp B)$ is not part of the instantiated axiom, but it works out if we have proven axiom 5 already (line 5). We will do that now.

Pseudo-Transitivity (Axiom 5)

Pseudo-Transitivity: $(A \imp B) \imp (C \imp A) \imp (C \imp B)$

Plugging this in to axiom 2, we have (Let $P$ be $A \imp B$ and $R$ be the rest):
$((A \imp B) \imp\ ?\ \imp ((C \imp A) \imp (C \imp B)))$ $\imp ((A \imp B) \imp\ ?\ )$ $\imp ((A \imp B) \imp ((C \imp A) \imp (C \imp B)))$

When thinking about what to substitute in for the question mark, we need a crucial trick:⁵

VC Rule: If $S$ is proven, then we can derive $T \imp S$ (for any $T$)

So let $?$ be $(C \imp A \imp B)$. Then the first antecedent becomes:
$((A \imp B) \imp\ (C \imp A \imp B) \imp ((C \imp A) \imp (C \imp B)))$
Since $(C \imp A \imp B) \imp ((C \imp A) \imp (C \imp B))$ is a theorem (axiom 2), the first antecedent is provable after an application of VC. The second antecedent becomes an instance of axiom 1: $(A \imp B) \imp (C \imp A \imp B)$

Here’s the full proof:

Permutation (Axiom 6)

Permutation: $(A \imp B \imp C) \imp (B \imp A \imp C)$

It is obvious that we should use axiom 2:
$((A \imp B \imp C) \imp\ ? \ \imp (B \imp A \imp C))$ $\imp ((A \imp B \imp C) \imp\ ? \ )$ $\imp (A \imp B \imp C) \imp (B \imp A \imp C)$

We will substitute $?$ with $(B \imp A \imp B)$. Why? Consider the two antecedents:
$(A \imp B \imp C) \imp (B \imp A \imp B) \imp (B \imp A \imp C)$
$(A \imp B \imp C) \imp (B \imp A \imp B)$
We can straightforwardly prove the second antecedent by the VC rule, because $(B \imp A \imp B)$ is already a theorem. What about the first antecedent? Notice that the following two formulas are instantiations of axiom 5 (which we have already proved) and axiom 2, respectively:
$((A \imp B) \imp (A \imp C)) \imp (B \imp A \imp B) \imp (B \imp A \imp C)$
$(A \imp B \imp C) \imp (A \imp B) \imp (A \imp C)$
And if we use axiom 5 on these two formulas, we immediate get the first antecedent.

Let $\phi$ be $(B \imp A \imp B) \imp (B \imp A \imp C)$.

Note that I have omitted a few steps by using Pseudo-Transitivity (axiom 5) as a derived rule.

Proving System A from System B

We prove that axiom 2 is derivable from axiom 4~6. This direction of the proof is relatively easier because we have more axioms to work with. First, let us first prove this derived rule:

Transitivity*: Given $P \imp Q \imp R$ and $R \imp D$, we can derive $P \imp Q \imp D$

Now that we have this rule under our belt, we can prove axiom 2. Let $\psi$ be $(Q \imp P \imp R) \imp (P \imp Q) \imp (P \imp R)$.

The first step has axiom 2 as its consequent, and its second antecedent is a straighforward application of the permutation axiom. The first consequent took more work to prove; it required recognizing that the second step is possible from axiom 5, and that we can utilize Contraction and Transitivity*.

Lessons

To sum it up, we showed that the usual first step is to find an axiom whose consequent fits the goal, then consider filling in the $?$ in a way that makes each antecedent provable. In the case where an antecedent is not straightforwardly provable, we also utilizes other tricks like VC, (pseudo-)transitivity, and other already-proven axioms. The order of proving axioms is important; we had to recognize that we need axiom 5 to prove axiom 4 and 6, and whenever we search for axioms to fit the goal, we want to include the ones we have already proven.