What sort of sentence is the Goedel Sentence (for the First Incompleteness Theorem)?

As everyone knows who have studied Hilbert's writings, he divides sentences and terms (well-formed formulas) into at least (the 'at least' in deference to Smorynski) two classes: finitary, and ideal. (In what follows I shall be quoting heavily from Stephan Bauer-Mengelberg's translation of Hilbert's paper "On the Infinite, found in van Heijenoorts book From Frege to Goedel . My comments will be enclosed in brackets.)

Regarding finitary well-formed formulas (wffs for short) (of a formal language and theory, of course) he states:

"It ["finitary number theory"--this term from the preceding sentence in the paragraph] can be certainly developed through the construction of numbers by means solely of of intuitive contentual considerations. But the science of mathematics is by no means exhausted by numerical equations and cannot be reduced to these alone. One can claim, however, that it is an apparatus that must always yield correct numerical equations when applied to integers. But then we are obliged to investigate the structure of the apparatus sufficiently to make this fact apparent. And the only tool at our disposal in this investigation is the same as that used for the derivation of numerical equations in the construction of number theory itself, namely, a concern for concrete content, the finitist frame of mind. This scientific requirement can in fact be satisfied; that is, it is possible to obtain in a purely intuitive and finitary way , just like truths of number theory, those insights that guarantee the reliability of the mathematical apparatus . Let us now consider number theory in more detail."

He then proceeds to construct the numerals

|, ||, |||, ||||,... [by a process of concatenating by |, i.e. __$^\frown$|--my comment ]

and states, "...These numerals, which are the object of our consideration, have no meaning at all in themselves." He continues:

"In elementary number theory, however, we already require, besides these signs, others that mean something and serve to convey information, for example, the sign 2 as an abbreviation for the numeral ||, , or the numeral 3 as a sign for the numeral |||; further, we use the signs +,=,>, and others , which serve to communicate assertions. So 2+3 [i.e. ||$^{\frown}$|||--my comment] = 3+2 [i.e. |||$^{\frown}$||] serves to communicate the fact that 2+3 and 3+2, when the abbreviations used are taken into account, are in fact the same numeral, namely, the numeral |||||. Likewise, then, 3>2 serves to communicate the fact that the sign 3 (that is, |||) extends beyond the sign 2 (that is, ||) , or that the latter sign is a proper segment of the former."

He also states the use of letters for numerals (i.e. $\mathfrak a$, $\mathfrak b$, $\mathfrak c$,..., $\mathfrak b$>$\mathfrak a$,'$\mathfrak b$+$\mathfrak a$=$\mathfrak a$+$\mathfrak a$', and instances of bounded existential quantification are acceptable finitary wffs. However, he states that ordinary existential and universal quantification (leading to infinite disjunctions and conjunctions of finitary terms and sentences) are not acceptable from a finitary point of view. Regarding the logical manipulation of finitary ["contentual communications"] propositions he states:

"In mathematics, we found, first, finitary propositions that contain only numerals, like

3>2, 2+3=3+2, 2=3, and 1$\ne$1,...

...These are capable of being negated, and the result will be true or false; one can manipulate them at will, without any qualms, in all the ways that Aristotlean logic allows." This suggests (to me, at least) that these propositions can also be manipulated by propositional logic. I hope by now the reader has a somewhat clear picture of what Hilbert meant by finitary wffs.

What then of ideals wffs? Well, Hilbert says that infinitary conjunctions and disjunctions of finitary propositions are 'ideal' and one can also form ideal wffs by means of abstraction [my term] as follows. Consider the finitary proposition

2+1=1+2

one can substitute letters for numerals and form the wff

$\mathfrak a$+1=1=$\mathfrak a$.

So far, Hilbert would deem such a wff as finitary since $\mathfrak a$ is just a sign for an arbitrary numeral [a type of schema?]. However, by abstracting further and replacing the letter a for the numeral-schema $\mathfrak a$, one has

a+1=1+a

which has no meaning in itself, but can be used to derive finitary propositions of the form

3+1=1+3, etc.

Hilbert summarizes all of this in the following manner:

"...mathematics becomes an inventory of formulas--first, formulas to which contentual communications of finitary propositions [hence, in the main, numerical equations and inequalities [Hilbert's comment]] correspond, and, second, further formulas that mean nothing in themselves and are the ideal objects of our theory."

I will now consider the Goedel sentence

$\lnot$Bew(n),

where n is the Goedel-number of $\lnot$Bew(n) (where Bew(x) denotes [following Rosser in his paper "An Informal Exposition of Proofs of Goedel's Theorem and Church's Theorem", found in Martin Davis' book The Undecidable] "the formula (wff) with the number n is provable in $T$", where $T$ is a first-order theory containing enough arithmetic to adequately allow for Goedel-numbering).

Since, by the definition of Goedel-numbering, 'n' of $\lnot$Bew(n) is a specific number, one can replace the sign 'n' with its associated numeral $\mathfrak n$, so one now has the proposition

$\lnot$Bew($\mathfrak n$), where $\mathfrak n$ is the numeral associated with the Goedel-number for $\lnot$Bew($\mathfrak n$).

Question: Is $\lnot$Bew($\mathfrak n$) a finitary proposition in Hilbert's sense? If not, then is it an ideal proposition? If it is a finitary proposition in Hilbert's sense, then its unprovability seems to be irrelevant, since such finitary propositions are intuitively true or false, as $\lnot$Bew($\mathfrak n$) is. If ideal, then the impact of Goedel's first incompleteness on Hilbert's program seems to be that there are ideal propositions that cannot be abstractions of finitary propositions, in which case Hilbert can restrict his attention to only those ideal propositions which are abstractions of finitary propositions. Does the Paris-Harrington incompleteness theorem apply to such ideal propositions as these?

Neither $Bew(\mathfrak{n})$ nor $\neg Bew(\mathfrak{n})$ is finitary: they quantify over all proofs. Verifying the first formula requires an unbounded search for a proof, stopping once one is found. Verifying the latter requires examination of all proofs, examining each one, and stopping only if a counterexample is found. In the latter case, its falsity might be established in finite time, but not its truth. The examination of each case (potential proof) is an effective operation, a finitary procedure. The former sentence is an infinite disjunction of finitary formulas; the latter, an infinite conjunction. So, yes, they are "ideal" propositions.
• Note that in fact $Bew(x)$ is a maximally complicated existential formula, in a precise sense: for any other existential formula $\varphi(x)$, we can find a primitive recursive function $f$ such that, for all $n$, $\varphi(n)$ is true iff $Bew(f(n))$ is true. (This is closely related to the recursion-theoretic notion of a complete c.e. set.) Note that this isn't fully internal to PA (I'm assuming PA is the theory Bew refers to, here): it is consistent with PA that $\forall xBew(x)$. Nov 17, 2015 at 22:34
• @NoahSchweber Your last line gave me pause for a moment, but yes sure: PA + $\neg$Con(PA) is consistent if PA is, although it has few adherents. Nov 17, 2015 at 22:48