Do Godel\'s Incompleteness Theorems undermine Hilbert\'s program?

ENO AGOLLI – MATHEMATICAL LOGIC – SUPERVISION IV
Topic: Do Gödel's Incompleteness Theorems undermine Hilbert's Program?



In the most mature statement of his program for the foundations of mathematics, On the Infinite (1926), Hilbert outlines his vision for providing a justification of classical mathematics, like analysis, set theory, and arithmetic. His program consisted in a distinction between real and ideal mathematical statements corresponding to a wider distinction between a finitary and an infinitary part of such mathematics. His aim was to show that infinitary mathematics, which was taken to include finitary mathematics, is epistemically secure, in the sense that it could never lead to false real statements. This could be achieved only by showing the consistency of infinitary mathematics. However, my thesis is that this very last ambition was shown to be untenable by Gödel's second incompleteness theorem. I consider and reply to the most prominent response to my thesis, namely that Gödel's theorem concerns only standard formalizations of infinitary mathematics so that some non-standard formalization of infinitary mathematics could show the consistency thereof and, hence accomplish Hilbert's program.
I will try to define and explain certain recurring concepts in the following exposition. Firstly, formal theory is some set of sentences expressed in the language of an underlying logic. Typically, the underlying logic is first-order logic, which includes, among other things, some set of rules of inference, such as the law of the excluded middle (LEM). Such rules are crucial because, when applied to a given sentence, they can generate a further sentence in the theory. The generation of a further sentence in this way is called a derivation of that sentence. More precisely, a formalized theory may be defined as a set of sentences T that is closed under the relation of logical consequence, i.e. if a sentence S is a logical consequence of T, then it is called a theorem of T and it is a member of T. The special set of sentences of T of which all theorems of T are logical consequences are called axioms.
If T is axiomatizable then for any theorem S in T, there is some derivation, i.e. a finite sequence of sentences the last member of which is S and each of which is either an axiom or a sentence that is the logical consequence of an axiom. If we are able to decide, by means of some effective procedure by means of which one can decide, after a finite series of operations, whether any given sentence in the proof fulfills one of the aforementioned conditions, then we say that the derivation is decidable. For this to be the case, the set of axioms must be decidable: for any given sentence of T we must be able to decide, again by means of some similar procedure, whether or not it is an axiom. There is a third case of decidability, as it pertains to particular sentences. A sentence of the language of T is said to be decidable just in case it or its negation are theorems of T. Deciding whether a sentence is a theorem of T is possible only be means of some derivation from the axioms of T. Hence, there is a derivation in T of any sentence of the language of T iff T is complete. Lastly, T is said to be consistent iff, for any sentence, only either it or its negation are derivable in T.
Hilbert's program (1926) was inspired by primarily epistemological considerations (Giaquinto, p. 148). His intention was to provide a basic set of theorems that could serve as the foundation of the rest of mathematics – mainly arithmetic, set theory, and analysis – in the sense that the rest of mathematics could be shown to be reducible to such theorems – or, otherwise put, be a logical consequence thereof. Such a set of theorems was to be epistemologically secure. So construed, Hilbert's program could be achieved only by means of a formal, axiomatizable theory, for only such a theory could provide the capacity to perform the aforementioned reductions to a formally specified set of axioms. My task henceforth will be to specify the notion of "epistemologically secure" and Hilbert's exact vision of the appropriate way of showing that a set of axioms is such.
Towards this end, I will introduce Hilbert's distinctions between real and ideal mathematical statements and the corresponding finitary and infinitary mathematics. The part of mathematics that Hilbert calls finitary involves only objects which are "intuitively present as immediate experience prior to all thought" and reasoning which does not involve (appeal to) infinite entities. Such objects are known as numerals which are nothing but a series of different concatenations of "strokes". For example, """ is the numeral commonly represented by number "3". One can perform several operations with them, such as addition, i.e. a further concatenation of two or more numerals to obtain a new one, or comparisons. The finitary part of mathematics can be represented or translated in a formal system and the statements of the formal system that refer to this part, i.e. to finitary objects or facts about them, are called real. It is unproblematic within the formal representation of finitary mathematics, to apply rules of inference to real statements, because the domain of the language is finite. In general, finitary mathematics is supposed to be accepted by all parties involved in debates regarding mathematical foundations and are taken to be epistemically secure: "Knowledge of properties and relations [of numerals] is intuitive and unmediated by logical inference, [therefore the resulting formalized theory is] secure: no contradictions can arise because there is no logical structure in the [statements thereof], […] because formulas and proofs are similarly based in a logic-free intuitive capacity which guarantees certainty of knowledge." (Zach, §1.3)
However, theories like analysis, set theory etc. contain not only real statements but also ideal ones. Such statements contain terms like quantifiers, infinite sets which do not seem to refer to any finitary objects or facts about them; quite the contrary, they seem to refer to infinite entities. Hence, there is no obvious reason to think that application of rules of inference to such statements is epistemologically secure, especially when ideal statements are used in order to, purportedly, derive real statements.
To see this, consider LEM for existential quantifiers, namely either x satisfies φ or there is some x that satisfies ~φ. As it stands, this proposition seems to be appealing to some infinite entity, for the existential quantifier could be ranging over some infinite domain. Hence, for LEM to qualify as a real statement, under a finitary methodological standpoint, there must either be a finitary procedure "by which one can specify a bound b for which we can prove every integer smaller than b satisfies the instance" (Giaquinto, p. 146). More generally, although Hilbert never fully clarified the notion of real statements, it does seem certain that as such qualify "numerical equations and their negations, bounded existential and universal quantifications of these, and at least some universal generalizations, [i.e. included in] Π01 sentences." (Raatikainen, p. 160) Lastly, finitary mathematics may be identified with PRA.
Instead of rejecting infinitary mathematics for this reason, Hilbert's program was to show that infinitary mathematics, and the ideal statements in which it consists, is indeed epistemologically secure, and to do so by means of the only epistemologically secure reasoning available, i.e. finitary reasoning. Instead of rejecting, for example, the unrestricted version quantifier version of LEM, he wanted to maintain it because of its usefulness in accomplishing proofs of real statements. In other words, he viewed ideal statement as "instruments" (Zach, §3) that served to derive only true real statements. Hence, it remained for him to show, by finitary means, that the instruments at hand were indeed capable of serving such a purpose – that they were, that is, epistemically secure.
So construed, epistemic security could only mean one thing, reliability. If an ideal theory, henceforth denoted by "T", were to be reliable, it should never allow for the derivation of a false real statement. This requirement is taken to be tantamount to a requirement for the consistency of T. That is, that T could never prove a real statement whose negation would be derivable from a finitary theory F (Raatikeinen, p. 160), because, given that F is a member of T (to be specified further below), that would imply that there is a derivation in T of a sentence and its negation Hence, Hilbert's program, from seemingly semantic, i.e. one about reliability, thus about the truth or falsity of the theorems of finitary mathematics, is in fact merely syntactic, i.e. one about the derivation of a certain pair of sentences. In short, reliability of T may be identified with consistency thereof.
I believe that Gödel's incompleteness theorems refute Hilbert's program. To show this, I will provide a sketch of both his first and second theorems, with a special focus on the first, from which the second can be shown to follow more easily.
The first incompleteness theorem states that for certain formal systems, if they are assumed to be consistent, there are sentences of the language of that system for which there is no derivation thereof or of their negation. These formal systems are ones that include a certain arithmetical theory. As I hope to have rendered obvious by now, this arithmetical theory is nothing but finitary mathematics, which, as noted, will be identified with PRA. As a matter of fact, Gödel proved his first theorem for a theory "P" which stood for the one devised in Russell and Whitehead's Principia, which is equivalent to PRA. However, his result can be extended to any theory which contains PRA or, more precisely, in which PRA is interpretable. And a theory T1 is interpretable in another theory T2 just in case the primitive functions and the range of variables of the former are such that they allow that they can be defined in T2 and hence allow for the translation of all the theorems of T1 into theorems of T2 (Raatikainen, 2013, §1.2). The crucial feature of interpretability, so construed, is that it entails conservativity – i.e. if T1 is consistent, then its interpretability into T2 should guarantee that T2 is also consistent.
A sketch of the proof may be presented by the following steps. Firstly, it is assumed that the formal system in question, say T, is consistent at least such that the set of purely existential sentences of the form x1… xnΦ is consistent. Secondly, strong and weak representability are distinguished as follows: suppose there is a finite set of natural numbers; if for any natural number n there is some sentence with only one unbounded variable Φ(x) such that T entails Φ(n) if n is in that set and T entails ~(Φ(n)) if n is not in that set, then it is strongly representable. More formally: a set of numbers S is strongly representable iff n S T Φ(n) & n S T ~Φ(n). It is weakly representable iff n S T Φ(n). From the aforementioned it follows that, for any n, T provides an effective procedure to decide whether it belongs to S or not, if it is strongly representable, or only whether it belongs to S, if it is weakly representable. The set in question, then is said to be decidable or semi-decidable, respectively. Thirdly, an arithmetization of T is performed – that is, a bijection between the set of natural numbers and T such that it 'codes with' some natural number any possible expression of T, from its simplest symbols that comprise the vocabulary of its language to sentences and even derivations of sentences. For any expression E of T its coded version is written as E . Fourthly, it follows that any derivation d of a sentence φ can be coded and, therefore, strongly represented in T. However, the property of being derivable in T is only weakly represented by the purely existential sentence xDerT(d, φ), or just DerT(d), such that T Φ T DerT( Φ ). Fifthly, the famous Diagonalization Lemma: if Φ(x) is any sentence of the language of T with just one unbounded variable, then it is possible to formulate a sentence Ψ such that T Ψ Φ( Ψ ). Sixthly, we apply the Diagonalization lemma to ~DerT(d) so that we get a sentence Ψ' such that T Ψ' ~DerT( Ψ' ). Finally, we show that Ψ' is neither derivable nor non-derivable in T, if T is consistent, so that T Ψ' and T ~Ψ'. T is incomplete.
The second incompleteness theorem may be seen as a more special case of the more general fist theorem, where one can use the formalized version of any false real statement Π, such as 1 1, to stand for d, in DerT(d). The consistency of T may then be formalized by the sentence ~DerT( Π ) or, as it is more common in the literature, Con(T). But it should be immediately obvious that if T is consistent, then one can derive from it, as it was shown above, the special sentence Ψ'. Therefore, if we can derive Con(T) from T, then we can also derive Ψ' from T, which is expressly precluded by the first theorem. Hence, Con(T) is a sentence that cannot be derived from T, i.e. F Cons(F).
This result provides, in my view, in a straightforward way, a negative answer to Hilbert's question of whether one can derive the consistency of an infinitary theory T from its finitary part F. From no finitary theory, or even a finitary-conservative theory, can a statement of its own consistency be derived, let alone that of other theories, such as the infinitary (but finitary-conservative) theories of set theory, analysis, PA, etc. To make this clearer, let T be such a theory, i.e. an infinitary theory formalizing, say PA, but which includes, as defined, a finitary part F, PRA. Moreover, let's assume, for reductio, Hilbert's aim, namely that it can be derived, in F, that T is consistent. Let C be a sentence of the language of T that states the consistency of T thus: it is not the case that there is a derivation, in T, of any arbitrary sentence Φ and another derivation, in T, of its negation, ~Φ. But C entails by finitary means alone that C': it is not the case that there is a derivation of, in T, of a false real statement (for then T would not be reliable, and hence inconsistent) (Giaquinto p. 150). C' is exactly what its syntactic counterpart, Con(T) above, is supposed to express. Thus, if we could derive C from F alone, then we could also derive Con(T) from F alone, and therefore from T. But this very last step is exactly what the second incompleteness theorem expressly precludes. Hence, the second incompleteness theorem precludes the derivation of C from F.
The most powerful objection against this line of argument is Detlefsen's (1989). In effect, his main premise is that Con(T) above need not be the only formalization possible of the requirement that T is a consistent theory. The upshot of such a premise is that if there exist alternative formalizations of the aforesaid requirement, then they could possibly be derivable from T, unlike Con(T). As it was shown, the sentence Con(T) crucially depends on the binary relation DerT(d, φ) which, in turn, depend on three derivability conditions (Smith, 2007, p. 224) , in order to express the (intended) notion of derivability. Detlefsen's view is that such conditions are not necessary and, thus, one can devise non-standard formalized theories in which the derivability relation does not obey some of the conditions, especially the the following: T DerT( Φ ) DerT( DerT( Φ ) ). (Ibid.). Indeed, Detlefsen proceeds to show that there exists such a relation which can then result to consistency statement in code which is derivable from the corresponding non-standard theory.
There are two replies to Detlefsen. Firstly, there is no argument for why one should think that the non-standard theories formalize the intended conception of derivability, the one that Hilbert's program presupposes (Raatikainen, 2003). As already argued, Hilbert's overarching aim was epistemic security of the sort that guarantees that rules of inference of traditional logic may be applied for infinite domains without the danger of such applications leading to false real statements. This aim by no means implies the further aim to "devise some ad hoc logic (i.e. notion of provability) which allows a consistency proof of the axioms of ideal mathematics" (Raatikainen, Ibid. p. 165). Raatikainen (Ibid., p. 166) provides good textual evidence that Hilbert intended his program to guarantee a finitary derivation of the consistency of any consistent theory, which includes PRA; i.e. standard as well as non-standard.
Secondly, one can derive consistency statements from such non-standard theories because of the particular way in which they are developed (Giaquinto, p. 189): every such theory is developed 'parasitically' from a standard theory, so that it can be ensured that the two theories contain all the same theorems and, thus, that the derivability relation is extensionally correct, i.e. co-extensional with the standard derivability relation DerT(x). However, this has the unfortunate result that a derivation of the consistency of the non-standard theory could be complemented with a derivation of the statement that it is co-extensional with its standard counterpart. This would mean that we have obtained a finitary derivation of Con(T), which is precluded by the second incompleteness theorem.


BIBLIOGRAPHY
Giaquinto, Marcus. The Search for Certainty. Oxford: Oxford University Press, 2002
Hilbert, David. Über das Unendliche. Mathematische Annalen 95. English translation in J. van Heijenoort (ed.), 1967
Raatikaeinen, Panu. Hilbert's Program Revisited. Synthese, 137, 2003
Raatikainen, Panu. Gödel's Incompleteness Theorems. The Stanford Encyclopedia of Philosophy [Online]. Available at: http://plato.stanford.edu/entries/hilbert-program/
(Accessed: 15 Feb 2015)
Rosser, J. B. Extensions of Some Theorems of Gödel and Church. The Journal of Symbolic Logic, 1936
Zach, Richard. Hilbert's Program. The Stanford Encyclopedia of Philosophy [Online]. Available at: http://plato.stanford.edu/entries/hilbert-program/
(Accessed: 15 Feb 2015)


6



Here used in its syntactic sense, only.
To be used absolutely interchangeably with "sentences".
More fully: "Extra-logical discrete objects, which exist intuitively as immediate experience before all thought. If logical inference is to be certain, then these objects must be capable of being completely surveyed in all their parts, and their presentation, their difference, their succession (like the objects themselves) must exist for us immediately, intuitively, as something which cannot be reduced to something else." (Hilbert, 1922b, p. 202)
Real statements can be further distinguished into proper and general ones, such as 1 + c = c + 1. The latter may seems suspicious for the purposes of finitism. I will follow grant Giaquinto's defense (Giaquinto, p. 149) of general real statements and assume them to be unproblematic.
Raatikainen (2003, p. 161) agrees with (Tait 1981) that this identification is granted. He provides two further reasons:
a. PRA is a logic-free equational calculus, so choice of logic doesn't matter. All sides of the debate can agree at this point, thus.
b. The induction scheme of PRA is equivalent, neither weaker nor stronger that is, to that of the finitary part, i.e. over Π01-statements.
Moreover, I quote from (Zach, §2.3): "Hilbert and Bernays give the only general account of finitary contentual number theory; according to it, operations defined by primitive recursion and proofs using induction are finitarily acceptable. All of these methods can be formalized in a system known as primitive recursive arithmetic (PRA), which allows definitions of functions by primitive recursion and induction on quantifier-free formulas."

"[A]s a condition for the use of logical inferences and the performance of logical operations, something must already be given to our faculty of representation, certain extra-logical concrete objects that are intuitively present as immediate experience prior to all thought. If logical inference is to be reliable, it must be possible to survey these objects completely in all their parts, and the fact that they occur, that they differ from one another, and that they follow each other, or are concatenated, is immediately given intuitively, together with the objects, as something that can neither be reduced to anything else nor requires reduction. This is the basic philosophical position that I consider requisite for mathematics and, in general, for all scientific thinking, understanding, and communication." (Hilbert, 1926, p. 376)
Gödel proved the Incompleteness theorem for P, Russell's system of the Principia Mathematica. To show that his result could be extended more generally to any theory containing elementary arithmetic something like Church's thesis was necessary – unavailable at the time – that related computable functions and decidability as equivalent, a result arrived at later by Gödel (1934), Alonzo Church (1936a, b) and Alan Turing (1936–7).
I will assume Rosser's result (1936) and not get into the details of ω-consistency, or 1-consistency.
Importantly, the bijection must be decidable. Even more importantly, arithmetization of F ensures that it is strongly representable in any theory T that contains PRA.
The presentation is due, in large part, to Raatikainen (2003, §2).
Those rules of inference that "man has always used since he began to think" (Hilbert, 1926, p. 379).