Tricks for Constructing Hilbert-Style Proofs

Several times in my studies, I've come across Hilbert-style proof systems for various systems of logic, and when an author says, "Theorem: $\varphi$ is provable in system $\cal H$," or "Theorem: the following axiomatizations of $\cal H$ are equivalent: ...," I usually just take the author's word as an oracle instead of actually trying to construct a Hilbert-style proof (can you blame me?). However, I would like to change this habit and least be in a position where I could check these claims in principle.

On the few occasions where I actually did try to construct a (not-so-short) Hilbert-style proof from scratch, I found it easier to first construct a proof in the corresponding natural deduction system, show that the natural deduction system and the Hilbert system were equivalent, and then try to deconstruct the natural deduction system into a Hilbert-style proof (in the style of Anderson and Belnap). The problem with that (apart from being tortuous) is that I would need the natural deduction system first, and it's not always obvious to me how to construct the natural deduction system given the axioms (sometimes it's not so bad; it's easy to see, for instance, that $(A \rightarrow (A \rightarrow B)) \rightarrow (A \rightarrow B)$ corresponds to contraction; but it's not always that easy...).

So I'm wondering: are there "standard tricks" for constructing Hilbert-style proofs floating around out there? Or are there tricks for constructing a corresponding natural deduction system given a set of Hilbert axioms? Or is it better to just accept proof-by-oracle?

Solution 1:

Regarding "tricks for constructing a corresponding natural deduction system given a set of Hilbert axioms": Constructing natural deduction systems corresponding to axiomatic propositional or first-order systems isn't too hard when most of the axioms have fairly clear 'meanings', but I think it gets a bit tricker with nonclassical logics. Pelletier & Hazen's Natural Deduction gives a good overview of some different types of natural deduction systems. See, in particular, §2.3, pp. 6–12, The Beginnings of Natural Deduction: Jaśkowski and Gentzen (and Suppes) on Representing Natural Deduction Proofs. I think that there are three types of natural deduction systems that should be considered (in order of increasing ease of translation from the natural deduction system to the axiomatic system): Gentzen-style; Fitch-style (Jaśkowski's first method); and Suppes-style (Jaśkowski's second method).

Gentzen-style Natural Deduction

Gentzen-style natural deduction use proof trees composed of instances of inference rules. Inference rules typically look like this:

$$ \begin{array}{c} A \quad B \\ \hline A \land B \end{array}\land I \qquad \begin{array}{c} A \\ \hline A \lor B \end{array}\lor I \qquad \begin{array}{c} [A] \\ \vdots \\ B \\ \hline A \to B \end{array}\to I $$

A significant difference between axiomatic systems and Gentzen-style natural deduction is that intermediate deductions can be cited by any later line in an axiomatic system, but can only used once in a proof tree. For instance, to prove $(P \land Q) \land P$ from $P \land Q$ requires three instances of the assumption $P \land Q$ in a proof tree:

$$ \frac{\displaystyle \frac{\displaystyle \frac{[P \land Q]}{Q} \quad \frac{[P \land Q]}{P}}{Q \land P} \quad \frac{[P \land Q]}{P} }{ (Q \land P) \land P } $$

There's no way to reuse the intermediate deduction of $P$ from $P \land Q$. A naïve translation of a proof tree into corresponding axiomatic deductions will probably be pretty verbose with lots of repeated work (but it would be easy to check for and eliminate redundant deductions in the axiomatic proof). A very nice benefit of these systems, however, is that it is very easy to determine where a rule can be applied, and whether a formula is "in-scope" for use as a premise. Fitch-style and Suppes-style systems are more complicated in this regard.

Fitch-style Natural Deduction Systems

Fitch-style natural deduction systems for propositional logic have a type of subproof for conditional introduction. These capture "Suppose $\phi$. … $\psi$. Therefore (no longer supposing $\phi$), $\phi \to \psi$.) Even in this simplest type of subproof, the natural deduction has proof-construction rules about how lines in subproofs may be cited (e.g., a line outside of a subproof can't cite lines within the subproof). Still, unlike proof trees, some reusability is gained. For instance, in the Barwise & Etchemendy's Fitch (from Language, Proof, and Logic), would simplify the proof by reusing the deduction of $P$ from $P \land Q$:

1. • $P \land Q$ Assume.
2. • $P$ by conjunction elimination with 1.
3. • $Q$ by conjunction elimination with with 1.
4. • $Q \land P$ by conjunction introduction with 2 and 3.
5. • $(Q \land P) \land P$ by conjunction introduction with 2 and 4.

Some presentations allow for conditional introduction from any line top-level line within a subproof. In these presentations, not only can intermediate deductions be reused, but entire subproofs:

1. • $P \land Q$ Assume.
2. • $P$ by conjunction elimination with 1.
3. • $Q$ by conjunction elimination with with 1.
4. $(P \land Q) \to P$ by conditional introduction with 1–3.
5. $(P \land Q) \to Q$ by conditional introduction with 1–3.

In the first-order case, not only are there subproofs for conditional introduction, but there are subproofs for introducing new 'temporary' individuals (e.g., generic instances for universal introduction, or witnesses for existential elimination). These subproofs require special rules about where the individual of concern may appear.

Kenneth Konyndyk's Introductory Modal Logic gives Fitch-style natural deduction systems for T, S4, and S5. In addition to a condtional introduction, these have modal subproofs for necessity-introduction, and those subproofs require special rules for reiterating formulae into the subproof. For instance, in T, only a modal formula $\Box \phi$ can be reiterated into a subproof, and when it does, the $\Box$ is dropped. That is, when $\Box \phi$ is outside a subproof, $\phi$ can be reiterated in (but only through one 'layer' of subproof). In S4, $\Box\phi$ can still be reiterated into a modal subproof, but the $\Box$ need not be dropped. In S5 both $\Box\phi$ and $\Diamond\phi$ can be reiterated into a modal subproof, and neither modality needs to be dropped.

The point to all this is that in the propositional case, many Hilbert-style axioms correspond nicely to Fitch-style natural deduction style rules, but it seems that the nicest cases are those for boolean connectives. E.g.,

$$ A \to \left( A \lor B \right) $$

and

$$ A \to \left( B \to (A \land B)\right) $$

turn into "left disjunction introduction" and "conjunction introduction" pretty easily. However, more complicated axiom schemata (such as what would be used for universal introduction, or modal necessitation) that really require new types of subproofs for good natural deduction treatment are trickier to handle nicely.

Suppes-style Natural Deduction Systems

There are, of course, other formalizations of natural deduction than Fitch's. Some of these might make for easier translation from axiomatic systems. For instance, consider a proof of $(A \to (B \to (A \land B))) \land (B \to (A \to (A \land B)))$. In a Fitch-style proof, the left conjunct, $A \to \dots$, would have to be proved in a subproof assuming $A$ containing a subproof containing $B$:

1. • Assume $A$.
2. • • Assume $B$.
3. • • $A \land B$ by conjunction introduction with 1 and 2.
4. • $B \to (A \land B)$ by conditional introduction with 2–3.
5. $A \to (B \to (A \land B))$ by conditional introduction with 1–4.

Then another five lines are needed to get $B \to (A \to (A \land B))$, and an eleventh for the final conjunction introduction. In Suppes's system, this is shorter (eight lines) because any in-scope assumption can be discharged by conditional introduction, so we can "get out of the subproofs" in different orders:

1. {1} $A$ Assume.
2. {2} $B$ Assume.
3. {1,2} $A \land B$ $\land$-introduction with 1 and 2.
4. {1} $B \to (A \land B)$ $\to$-introduction with 3.
5. {} $A \to (B \to (A \land B))$ $\to$-introduction with 4.
6. {2} $A \to (A \land B)$ $\to$-introduction with 3.
7. {} $B \to (A \to (A \land B))$ $\to$-introduction with 4.
8. {} $(A \to (B \to (A \land B))) \land (B \to (A \to (A \land B)))$ $\land$-introduction with 5 and 7.

(Note: some implementations of Fitch's system allow this for conditional introduction as well. E.g., in Fitch from Barwise and Etchemendy's Language, Proof and Logic conditional introduction can cite a subproof that starts with an assumption $A$ and contains lines $B$ and $C$ to infer both $A \to B$ and $A \to C$.)

To use this approach, each inference rule must also specify how the set of tracked assumptions for its conclusion is determined based on the premises of the rule. For most rules, the assumptions of a conclusion are just the union of the assumptions of the premises. Conditional introduction is the obvious exception. This approach also specifies that only lines with empty assumption sets are theorems.

This "tracking" approach, though, can be used for other properties too. The same considerations apply: each rule must specify how the tracked properties of the conclusion are computed from the premises, and the proof system must define which sentences are theorems.

For instance, in a system for first-order logic, the set of new individuals (for universal generalization or existential elimination) can be tracked, with most rules giving their conclusion the "union of the premises' individuals", with existential elimination and universal introduction the exceptions. Theorems are those sentences with an empty set of individuals and an empty set of assumptions.

This approach works nicely for modal logics, too. A Suppes-style proof system for K, for instance, in addition to tracking assumptions, tracks a "modal context", which is a natural number or $\infty$. The modal context indicates how many "necessitation contexts" we're in (intuitively, how many times we should be able to apply necessity introduction to a formula). In terms of Kripke semantics, the modal context is how far removed from the designated world we are. Sentences without any assumptions have context $\infty$, corresponding to the $\vdash \phi / \vdash \Box\phi$ rule. The inference rules require that their premises have compatible modal contexts (i.e., all non-$\infty$ modal contexts are the same). The default modal propagation is that the context of the conclusion is the same as the minimum context of the premises. The exceptions are that $\Box$ introduction subtracts 1, and $\Box$ elimination adds 1. Theorems are those sentences that have no assumptions and modal context $\infty$.

1. {1} (0) $\Box P$ Assume.
2. {2} (0) $\Box (P \to Q)$ Assume.
3. {1} (1) $P$ $\Box$-elimination with 1.
4. {2} (1) $P \to Q$ $\Box$-elimination with 2.
5. {1,2} (1) $Q$ $\to$-elimination with 3 and 4.
6. {1,2} (0) $\Box Q$ $\Box$-introduction with 5.
7. {2} (0) $\Box P \to \Box Q$ $\to$-introduction with 6.
8. {} ($\infty$) $\Box(P \to Q) \to (\Box P \to \Box Q)$ $\to$-introduction with 7.

In Suppes-style proof systems, the question is no longer about reiteration rules, about about property tracking and propagation rules. The purposes are similar, but in practice, certain kinds of axiomatic systems might be easier to translate into one kind or another.

Solution 2:

It's a long list of postings, a lot of it in Polish notation that is hard to read. Anyway, the systematic way to do it is to define a translation algorithm from derivations in ND to derivations in axiomatic logic. This is done in my recent "Elements of Logical Reasoning" section 3.6.(c). ND is there written in SC notation with the open assumptions displayed at the left of a turnstile.

I don't know if anyone ever mastered fully axiomatic logic. Russell was very bad at it, didn't even notice that one of his axioms was in fact a theorem! I needed the translation to be able to produce some of the more elaborate axiomatic derivations. Would be nice if someone implemented the algorithm.