[FOM] Truth and natural numbers

[Arne Hole]

I have a problem which I would very much like to receive comments on
from this group.

First some words on the background thinking. This does not really
reflect the way I arrived at the problem in question, but still it gives
some perspective. What happened, is that I started doubting that
the (informal) definition of the standard model of natural numbers
(henceforth N) is sufficiently precise for it to naturally determine the
truth value of all closed formulas in, say, the language L of PA. Note
that I am not talking about undecidability in any given axiomatized
L-theory, but about the much stronger notion of being "generally
undecidable" in the non-formal mathematics of natural numbers.
As we all know, the basic definition of N is, in all known variants,
essentially circular. Thus there is an opening for the possibility that
the lack of precision in the definition of "natural number" renders some
L-formulas impossible to prove or disprove in any meaningful way. If
this was the case, the situation would in a sense be analogous to the
case of CH and AC relative to the notion of "set". The structure based
semantics defining the N-truth value of L-formulas with unbounded
existential quantifiers, only works if all questions of the type "There
is a natural number such that..." can really be answered on basis of our
informal, intuitive definition of N. Note that although ZF proves that
every L-formula is either true or false in N, the "underdetermination
hypothesis" for N-truth described above does not imply that ZF contains
a contradiction.

Based on these ideas, I have tried finding candidates for "generally
undecidable" L-formulas. What I want is a formula which cannot be proved
from principles which are presently "generally accepted" as true for
natural numbers (such as the axioms of PA), while at the same time it
can be argued (informally) that its N-truth value may, in some way, be
"naturally undefined". However, I am not an expert in this field. Thus
to avoid spending time rediscovering things which are well known, I
would like to have your response to the little construction below. This
is a simplified version of a more general development which I find
interesting. As you can see, I have two questions (i) and (ii).

First some notation. If T is an axiomatized L-theory, let CMT(T) be the
L-statement

(Forall x)(Prf_T^2(x) -> Prf_T(x)),

where Prf_T is an L-formula with one free variable x expressing
provability in T (via a suitable choice of Godel numbering, in the
usual fashion), and where the iteration Prf_T^2(x) expresses
T-provability of the statement Prf_T(x). Interpreted in N, CMT(T) thus
says that for all x, if T proves that T proves x, then T actually proves
x. Here we employ an obvious convention for free variables under the
provability sign. I have chosen CMT to rhyme with "correct meta theory".
(I assume there is standard notation for this, sorry that I do not know it.)

Now for the actual construction. Let T_1=PA, and then inductively
T_(j+1)=T_j+Consistent(T_j) for j=1,2,... We may explicitly construct
(leaving out details here) an infinite sequence of L-formulas
S_1,S_2,... so that for all j, PA proves

S_j <-> CMT(T_j+S_(j+1))

Then we may prove the following little result:

Theorem: Assume that N is a model of PA. Then at least one of the
statements S_1 and S_2 is undecidable in PA.

Proof sketch: First note that PA cannot disprove neither S_1 nor S_2,
since this would imply that PA proves its own consistence. Assume that
PA proves S_1. Then the theory T_1+S_2 also proves S_1, or in other
words, T_1+S_2 proves CMT(T_1+S_2). This implies that N is not a
model of T_1+S_2. (Probably this is a standard result? I can supply a
proof if nescessary.) It follows that S_2 is not true in N. By
assumption, PA does not prove S_2. Hence S_2 is undecidable in PA. End
of proof.

Note that the above simple proof uses very little of the information
avaliable, in particular the structure of the infinite sequence for j>2.
By altering things a little, I believe it is possible to obtain stronger
results. For example, the above theorem does not rule out the
possibility that for both j=1 and j=2, PA could prove a statement of the
form

A -> S_j

or of the form

A -> not S_j,

where A is known (or generally assumed) to be true in N. A candidate for
A in the second statement (A -> not S_j) could be "PA is consistent".
(It will not be a candidate in the first statement, since PA trivially
proves (not A)-> S_j with this choice.) This brings me to my first
question for the group:

(i) Does anyone know a choice of A which solves this problem, ie. a
statement A which is known (or generally assumed) to be true in N, while
at the same time PA proves A -> S_j or A -> not S_j for j=1 and/or j=2?

I have some ideas for refining the above construction so that, roughly
speaking, letting A state the consistency of the theories T_i involved
in the infinite sequence, will not solve the problem. My second question
for the group is then

(ii) Does anyone know where this leads to? Is there any known work
covering these ideas?

Many thanks,

Arne H.