Understanding Hilbert's program

Question

Upon covering Hilbert's program in class and consulting https://plato.stanford.edu/entries/hilbert-program/, there were some questions I had on Hilbert's work, and was trying to find answers to them.

1. For Hilbert's Finitism, how does it manage to inherit/salvage methods of classical mathematics while still catering to the intuitionist's concerns?

I can see that Hilbert tried to eliminate all that was infinite (could be wrong on this statement) and only wanted to keep things that were finite but I don't see how he catered to intuitionism

2. What is the idea of a conservative extension and how does it relate to Hilbert's program?

Looking into the wiki article (https://en.wikipedia.org/wiki/Hilbert_system#Conservative_extensions), it's not quite clear to me of what the extension is referring to and when it mentions being fully extended, a hilbert-style system will resemble a system of natural deduction?

Thanks!

Answer 1

You can see :

• David Hilbert & Wilhelm Ackermann, Grundzüge der theoretischen Logik (1928), English transaltion of the second 1936 edition, page 27 for the "Hilbert-style" presentation of the sentential calculus.

The axiom system is a simplification (due to Paul Bernays in 1926) of the axiom system of Alfred North Whitehead and Bertrand Russell, Principia Mathematica, 3 vols (1910-1913).

As you can see (page 27), the primitive conncetives are disjunction ($X \lor Y$) and negation ($\overline X$), while $\to$ is an abbreviation:

$X \to Y$ is to be merely a more convenient way of writing $\overline X \lor Y$.

Wiki's entry refers to the application to logical calculus of the more general concept of conservative extension meaning that:

if a formula $φ$ involving the new connective $\to$ [e.g.: $X \to (Y \to X)$] is rewritten as a logically equivalent formula $θ$ involving only negation and disjunction [i.e. as: $\overline X \lor \overline Y \lor X$], then $φ$ is derivable in the extended system if and only if $θ$ is derivable in the original system [i.e. from the axioms and rules of page 27-on].

---

Natural Deduction is a proof system with no axioms and with all the (main) conncetives as primitives.

It was developed by Gerhard Gentzen, a student of Paul Barnays, in the 1930s and it is based on previous researches of Hilbert's school.

A 10-axioms system with all the conncetives as primitive was used by Hilbert and Bernays already in 1922-23 (see Jan von Plato, Gentzen's proof systems: byproducts in a work of genius, Bull Symb Log (2012)).

Note. Propositional Natural Deduction is sound and complete proof system for tautologies, as well as Hilbert & Ackermann axiom system (with Modus Ponens and Substitution rules); thus, they can be seen as different "organizations" of the same logical principles: the tautologies of classical logic (and the same concept applies to the corresponding proof systems for e.g. Intuitionsitic Logic, with regards to the suitable semantics).

---

For a short overview, you can see The Development of Proof Theory.

For more details:

• Paolo Mancosu, The Adventure of Reason: Interplay Between Philosophy of Mathematics and Mathematical Logic, 1900-1940, Oxford UP (2010), Parts I and II.

Answer 2

For Hilbert's Finitism, how does it manage to inherit/salvage methods of classical mathematics while still catering to the intuitionist's concerns? I can see that Hilbert tried to eliminate all that was infinite (could be wrong on this statement) and only wanted to keep things that were finite but I don't see how he catered to intuitionism.

I don't think it is right to think of Hilbert as trying to eliminate all that was infinite -- after all, he was one of the great (if not the greatest of) early 20th Century mathematicians, justly famous and revered for his ground-breaking work on various areas of classical (thoroughly infinitary) mathematics. He wasn't trying to sabotage his own work by sawing off the branches he was sitting on and "eliminating all that was infinite".

No, better to think of him as trying to secure the infinite by showing that classical mathematical ideas were not really threatened by apparent inconsistencies generated by the paradoxes and foundational problems that loomed early in the 20th Century, or by the critiques of intuitionists like Brouwer who claimed to find the classical theories incoherent.

How then did Hilbert (and his pupil then assistant Bernays, who perhaps was the philosophically clearer of the two) plan to secure classical mathematics?

The plan is (i) to give rigorous axiomatic presentations of chunks of classical mathematics (maybe we can do this wholesale by reducing it all to some set theory, or to arithmetic plus type theory, or something). (ii) Now stand back from such axiomatic theories and note that -- while the theories may be about infinitary whatnots -- the theories themselves are finitary structures (in the sense that their sentences are finite objects, properties like being-a-correctly-formed-proof are finitely checkable, etc., etc.). So this means we can use finitary reasoning about the theories.

And now here is the hopeful thought (and it is a quite brilliant one): we can in particular aim to use finitary reasoning -- reasoning acceptable to even the sternest critics of classical mathematics including the intuitionists -- to show that our classical theories are consistent after all(?!?!) That project is known as Hilbert's Programme.

It turns out, however, that we can't pull that off. For example, even though Zermelo Set Theory as a theory is a finitary object, we need infinitary reasoning at least as problematic as Zermelo Set Theory itself to show that the theory is consistent (we learn this from Gödel). Drat. Hilbert's Programme is a failure -- though a glorious failure, as it still leads to all kinds of highly important work in proof theory etc.

For a bit more on some details, and on the impact of Gödel's work (not an entirely straightforward matter), see my Introduction to Gödel's Theorems.