Converting Fitch to Hilbert proof

Question

I was wondering if anyone knows an algorithmic way of converting a natural deduction (Fitch) style proof into a axiomatic (or Hilbert) style proof. I am aware of one briefly introduced in Thomason (1970) but it seems unusable and I suspect that the author may have made mistakes. Can anyone point me to any others? Thanks!

Answer 1

The details will vary significantly depending on your target Hilbert-style system. For convenience I shall assume one that has the usual boolean connectives instead of just a measly "$\to$". In all cases, do the translation from inside out, namely starting from the innermost context and replacing the Fitch-style subproof by a Hilbert-style subproof before translating the context scoping itself. $ \def\TO{\ \mathrel{\huge➩}\ } \def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}} \def\block#1{\begin{array}{|l}#1\end{array}} $

In the innermost context, translate the application of the simple rules line by line:

$\fitch{A \\ B}{A \land B} \TO \fitch{A \\ B}{A \to ( B \to A \land B ) \quad [\land I] \\ B \to A \land B \\ A \land B}$

$\fitch{A \lor B \\ A \to C \\ B \to C}{C} \TO \fitch{A \lor B \\ A \to C \\ B \to C}{A \lor B \to ( ( A \to C ) \to ( ( B \to C ) \to C ) ) \quad [\lor E] \\ ( A \to C ) \to ( ( B \to C ) \to C ) \\ ( B \to C ) \to C \\ C}$

$\fitch{A \\ \neg A}{\bot} \TO \fitch{A \\ \neg A}{\neg A \to ( A \to \bot ) \quad [\neg E] \\ A \to \bot \\ \bot}$

$\fitch{\neg \neg A}{A} \TO \fitch{\neg \neg A}{\neg \neg A \to ( \neg A \to \bot ) \quad [\neg E] \\ \neg A \to \bot \\ ( \neg A \to \bot ) \to A \quad [\bot E] \\ A}$

Similarly for $\land$-Elim and $\lor$-Intro and $\neg$-Intro.

The lines with a label in square-brackets are Hilbert-style axioms that correspond to the Fitch-style inference rule. If they are not the ones you have in your system, simply replace them by a proof of them! The other rules are similar or easier, so I shall leave them to you.

Note that after translating the subproof in the innermost context, every line is either an axiom or deduced by MP (modus ponens).

Finally, the most important step is to translate the $\to$-Intro, which is the only Fitch-style rule that crucially requires handling different context scopes:

$\fitch{\fitch{A}{\vdots \\ B \quad [MP] \\ B \to C \quad [Axiom] \\ \vdots \\ C}}{A \to C} \TO \fitch{}{A \to A \\ \vdots \\ A \to B \\ B \to C \quad [Axiom] \\ ( B \to C ) \to ( A \to ( B \to C ) ) \quad [Sub{-}Restate] \\ A \to ( B \to C ) \\ \vdots \\ ( A \to B ) \to ( ( A \to ( B \to C ) ) \to ( A \to C ) ) \quad [Sub{-}MP] \\ ( A \to ( B \to C ) ) \to ( A \to C ) \\ A \to C }$

  Here I have just shown an illustrative example, and it should be clear how to generalize.

The Hilbert-style axioms [Sub-Restate] and [Sub-MP] are commonly found in many presentations of Hilbert-style first-order logic. The first corresponds to restating a previously deduced statement inside a subcontext. The second corresponds to using MP inside a subcontext, and as you can see allows one to unbind the subproof; each statement $C$ deduced inside a subcontext $A$ translates to the statement $( A \to C )$ outside that subcontext.

Incidentally, exactly the same technique can be applied to translate a proof in any Fitch-style system to a Hilbert-style system, so it is not at all restricted to propositional logic. The technique also shows you a method to systematically devise Hilbert-style axioms to capture the Fitch-style inference rules correctly and completely.