It is a misconception that an arithmetical statement—such as the one constructed by Kurt Gödel (1931. On formally undecidable propositions of Principia Mathematica and related systems I. In M. Davis. 1965. The Undecidable. p25)—can be intuitively true, and yet not follow formally from the axioms and rules of inference of a first-order Peano Arithmetic, .
The misconception arises because actually admits two logical entailments, only one of which—Gödelian provability—has, so far, been formally acknowledged.
However, the other—familiar only in its avatar as the intuitive truth of a proposition under ‘s standard interpretation—does, also, follow formally from the axioms and rules of inference of .
Even when this issue is sought to be addressed, the argument is indirect, and this point remains implicit.
For instance, in a critical review of Roger Penrose’s Gödelian argument, Martin Davis (1990. Is Mathematical Insight Algorithmic? Behavioural and Brain Sciences, vol. 13 (1990), pp. 659–660) argues that:
“… There is an algorithm which, given any consistent set of axioms, will output a polynomial equation which in fact has no integer solutions, but such that this fact can not be deduced from the given axioms. Here then is the true but unprovable Gödel sentence on which Penrose relies and in a particularly simple form at that. Note that the sentence is provided by an algorithm. If insight is involved, it must be in convincing oneself that the given axioms are indeed consistent, since otherwise we will have no reason to believe that the Gödel sentence is true”.
Note that the first part of Gödel’s argument in Theorem VI of his 1931 paper is that, if is consistent, then we can mechanically construct a formula—which, syntactically, is of the form —such that:
(i) The formula , when viewed as a string of ‘meaningless’ symbols, does not follow mechanically from the axioms of as the last of any finite sequence of -formulas, each of which is either a -axiom, or a consequence of one or more of the formulas preceding it in the sequence, by the mechanical application of the rules of inference of ;
(ii) For any given numeral —which ‘represents’ the natural number in —the formula , when viewed as a string of ‘meaningless’ symbols, does follow mechanically from the axioms of as the last of some finite sequence of -formulas, each of which is either a -axiom, or a consequence of one or more of the formulas preceding it in the sequence, by the mechanical application of the rules of inference of .
Now, (i) is the standard definition (due to Gödel) of the meta-assertion:
(iii) The -formula is formally unprovable in .
However, under standard interpretations of Alfred Tarski’s definitions of the satisfiability and truth of the formulas of a language under an interpretation , the -formula is true in the interpretation if, and only if, the interpreted relation is instantiationally satisfied in (i. e. for any given element of the interpreted relation can be ‘seen’ to hold in the interpretation).
If we take both and as (as detailed in ‘Evidence-Based Interpretations of PA‘), and take satisfiability in to mean instantiational provability in , we arrive at the formal definition of the truth of the -formula in as:
The -formula is formally true in if, and only if, the formula is provable in whenever we substitute a numeral for the variable in .
Hence (ii) is the standard definition (due to Tarski) of the meta-assertion:
(iv) The -formula is formally true in .
So, by definition, the appropriate interpretation of Gödel’s reasoning (i) and (ii) ought to be:
(v) The -formula is formally unprovable in , but formally true in .
This interpretation also meets Ludwig Wittgenstein’s (Remarks on the Foundations of Mathematics. 1978 edition. MIT Press) requirement that the concept of ‘truth’ in a language must be formally definable, and effectively verifiable, within the language.
As noted by Reuben L. Goodstein (1972. Wittgenstein’s Philosophy of Mathematics. In Ambrose, Alice, and Morris Lazerowitz (eds.), Ludwig Wittgenstein: Philosophy and Language. George Allen and Unwin. pp. 271–86):
“In the realist-formalist controversy in the philosophy of mathematics Wittgenstein’s Remarks offers a solution that is crystal clear and satisfyingly uncompromising. The true propositions of mathematics are true because they are provable in a calculus; they are deductions from axioms by formal rules and are true in virtue of valid applications of the rules of inference and owe nothing to the world outside mathematics.”
However, standard expositions of Gödel’s formal reasoning assert only that:
(vi) The -formula is formally unprovable in , but intuitively true in the standard interpretation of .
They fail to highlight that, actually, (i) and (ii) are both logically entailed by the axioms and rules of inference of , and that, classically, the meta-assertion:
(vii) The -formula is intuitively true in the standard interpretation of .
is both ambiguous and stronger than the meta-assertion:
(viii) The -formula is formally true in .
The ambiguity surfaces in the presence of the Church-Turing Thesis, for (vii), then, implicitly implies that the arithmetical relation is algorithmically decidable as always true in the standard interpretation of , whereas (viii) does not.