# Goedelizability and decidability of a property of Peano formulas

Sorry for not knowing the answers to these elementary questions:

Is the property of formulas of the first-order language of Peano arithmetic of "defining a finite set of natural numbers" goedelizable?

If so: Is the set of formulas with this property decidable, semidecidable or non-decidable?

-
By finite do you mean provably bounded, i.e. $PA \vdash \exists b\forall x(\phi(x) \to x \leq b)$? Or do you mean something stronger? –  François G. Dorais Feb 4 '10 at 23:46
By looking at your formula I am quite sure that I mean "provably bounded". But what might be stronger? –  Hans Stricker Feb 5 '10 at 0:03
"If this property was goedelizable and if there was a constructive proof that this property is decidable: one would not have to look for a specific proof for - e.g. - that there are infinitely many primes." Is this a correct line of reasoning? –  Hans Stricker Feb 5 '10 at 0:09
@Francois: Please forget about my last comment: you just showed that the property is NOT decidable, so what about infinite primes? –  Hans Stricker Feb 5 '10 at 0:50
Hans, this is the kind of focused and precise question that is good to make on MO. –  Joel David Hamkins Feb 5 '10 at 2:50

The set of (Gödel codes for) PA provably bounded formulas $\phi(x)$ is computably enumerable (c.e.). By provably bounded, I mean PA $\vdash \exists b\forall x(\phi(x)\to x \leq b)$. Indeed, you can enumerate all consequences of PA and when you find one of the shape $\exists b\forall x(\phi(x)\to x \leq b)$ then enumerate $\phi(x)$.

You can't do better than that since you can easily reduce the halting problem to the decision problem for the set of PA provably bounded formulas. Consider the formula $\phi_T(x)$ which says "the Turing machine $T$ (with blank input) has not halted after $x$ steps," with the usual arithmetic coding of Turing machines. Then PA proves that $\phi_T(x)$ is bounded if and only if $T$ truly halts in finite time.

Thus, the set of PA provably bounded formulas is a complete c.e. set.

-
Sorry, I do not understand the second part of your answer: on which input didn't the Turing machine T halt after x steps? –  Hans Stricker Feb 5 '10 at 0:16
It doesn't really matter, but I was assuming blank input. (If you prefer, you could also enumerate all possible combinations of machines and inputs.) –  François G. Dorais Feb 5 '10 at 0:22
While trying to understand your answer (second half of), I truly admire your ease of thinking this way! –  Hans Stricker Feb 5 '10 at 0:23
Do I understand correctly: The property of "defining a provably bounded set of natural numbers" is NOT decidable, but the set of such formulas is - almost trivially - enumerable? –  Hans Stricker Feb 5 '10 at 0:37
Yes, you understand correctly. In fact, I proved a stronger statement that the set of provably bounded formulas is a complete c.e. set, just like the halting set. –  François G. Dorais Feb 5 '10 at 0:40

Francois has fully answered the question about the formulas phi(x) that PA proves to define a finite set, and I agree completely with what he said.

It is also natural, however, to consider which formulas phi(x) define a finite set in the standard model of arithmetic.

Here, the situation is even worse. The set of (codes for) formulas phi(x) that define a finite set in the standard model is not decidable, not enumerable, not co-enumerable, not computable from the halting problem nor computable even from finitely many iterations of the halting problem. This set is not definable by any arithmetic formula. To see this, suppose that it were. Suppose there were a formula F, such that F('phi(x)') was true iff phi(x) defined a finite set. Note that as a special case, when phi(x) is a sentence whose truth does not depend on x, then the set { n | phi(n) is true in N } is either everything or empty, depending on whether the sentence is true or false in N, the standard model. Thus, for a sentence phi, the formula ¬F('phi') is true if and only if phi is true. Thus, F provides a definable truth predicate, but this is exactly ruled out by Tarski's theorem on the non-definability of truth. The proof of this is to use the fixed-point lemma to find a sentence psi such that PA proves (F('psi') iff psi). Thus, psi asserts "I am not true", and this easily gives a contradiction.

-
I am VERY interested in what you say, so let me please ask early: what's the main difference between your "standard model" and Francois' obviously "non-standard model" (or no model at all?) What does Francois' answer refer to? Only syntax? –  Hans Stricker Feb 5 '10 at 1:30
Tough answer, anyway. –  Hans Stricker Feb 5 '10 at 1:33
The issue is the PA is not a complete theory. The Incompleteness Theorem says that it is not possible to present a complete axiomatization of what is true in the standard model, that is, in the natural numbers. So, when you consider whether phi(x) defines a finite set or not, you could say that you want PA to prove this, or just that you want it to be true in the standard model. This difference of course affects which formulas you are speaking of, since some formulas actually define a finite set, but PA doesn't prove it. –  Joel David Hamkins Feb 5 '10 at 1:36
In principle, I am aware of the distinction between axiomatization and standard model, but eventually I have to refresh it (= make it concrete)! –  Hans Stricker Feb 5 '10 at 1:59