is the set of Pi_1 theorems recursive? ("undecidably undecidable" statements)
David Madore
I had always taken the following fact for granted, but I realize now
that I don't know how to prove it, and the question doesn't even seem
mentioned in any of the books I can find (e.g., *Metamathematics of
First-Order Arithmetic* by Hájek and Pudlak):
Is the set of Pi_1 theorems of Peano arithmetic nonrecursive?
Comment: it is well-known that the set of Sigma_1 theorems is
nonrecursive (essentially because Sigma_1 theorems are exactly Sigma_1
true statements). If the above is true then there exists a true Pi_1
statement such that P is not provable in Peano, and _that_ is not
provable in Peano+Consis(Peano) (otherwise we would have a decision
algorithm for Pi_1 theorems and the above says exactly that this does
not exist): i.e., there is an "undecidably undecidable" (but true)
statement.
Is this known? If so, where can I find a proof?
--
David A. Madore
(david....@ens.fr,
http://www.dma.ens.fr/~madore/ )
David Madore
> Is the set of Pi_1 theorems of Peano arithmetic nonrecursive?
Sorry, I think this is another instance of the general rule of "I'll
think about a problem for hours, and find the answer minutes after I
decide to ask the question publicly"... So if I'm not mistaken,
here's a proof of this:
Let T1 and T2 be two Turing machines which enumerate recursively
enumerable sets S1 and S2 of integers which are disjoint but not
recursively separable (that is, there is no recursive set which
contains one and is disjoint from the other). We also need the fact
that Peano arithmetic proves that S1 and S2 are disjoint (or, more
accurately, that there is no integer x which is enumerated by T1 and
by T2): this is harmless. (The existence of T1 and T2 is proved,
e.g., in Roger's *Theory of Recursive Functions and Effective
Computability*, circa §7.7.)
Now given an integer x the statement "T2 never generates x" (that is,
"x does not belong to S2") is Pi_1. Consider the set C of x such that
this is a theorem of Peano: if the set of Pi_1 theorems of Peano
arithmetic were recursive, then C would be recursive. Certainly, C is
disjoint from S2 because Peano is sound. But conversely, if x belongs
to S1 then that fact is a theorem in Peano (because it is a Delta_0
statement), so it is also a theorem in Peano that T2 never generates x
(because by assumption Peano proves disjointness of S1 and S2), i.e.,
x belongs to C. So we have a recursive set C which contains S1 and is
disjoint from S2, a contradiction.
In fact the reasoning above shows that the set of Pi_1 theorems of
Peano and the set of Pi_1 antitheorems (=negation is a theorem) are
recursively inseparable. So it is not possible that for all Pi_1
statements P either Peano+Consis(Peano) proves Consis(Peano+P) or
Peano+Consis(Peano) proves Consis(Peano + not-P): for if this were the
case we would have a recursive separation of the set of Pi_1 theorems
into certain consistent statements (including all Pi_1 theorems) and
certain unprovable statements (including all Pi_1 antitheorems). In
particular, there is a Pi_1 statement P such that Peano+Consis(Peano)
does not prove either Consis(Peano+P) or Consis(Peano + not-P); and of
course, P must be true, because otherwise not-P would be a theorem (so
Peano+Consis(Peano) would prove Consis(Peano + not-P)), but it must
also be unprovable in Peano (otherwise Peano+Consis(Peano) would prove
Consis(Peano+P)). Ergo, I have shown that there is a true Pi_1
statement P which is not provable in Peano (nor refutable) but such
that Peano+Consis(Peano) cannot show that P is unprovable nor can it
show that it is consistent.
And I'm sure P can be made explicit (using effective inseparability).
Also, I'm sure we can go much further (for all integers k, find a true
Pi_1 statement P such that any addition of up to k levels of "is
consistent" or "is unprovable" is true: P is true, P is consistent, P
is unprovable, "P is consistent" is consistent, "P is consistent" is
unprovable, "P is unprovable" is consistent, "P is unprovable" is
unprovable, etc., where each level refers to a formal system which
adds consistency of the previous one to its axioms).
I hope I didn't make any major mistakes here.
I'd still like to find a textbook reference to such questions, because
I'm sure there are more interesting things to be said than my modest
knowledge will let me discover.
Keith Ramsay
|David Madore in litteris <dtn8q2$fea$1...@news.ks.uiuc.edu> scripsit:
|> Is the set of Pi_1 theorems of Peano arithmetic nonrecursive?
|Let T1 and T2 be two Turing machines which enumerate recursively
|enumerable sets S1 and S2 of integers which are disjoint but not
|recursively separable (that is, there is no recursive set which
|contains one and is disjoint from the other). We also need the fact
|that Peano arithmetic proves that S1 and S2 are disjoint (or, more
|accurately, that there is no integer x which is enumerated by T1 and
|by T2): this is harmless. (The existence of T1 and T2 is proved,
|e.g., in Roger's *Theory of Recursive Functions and Effective
|Computability*, circa §7.7.)
Probably my favorite way to construct an example is to take
an enumeration f1, f2, f3,... of the primitive recursive
sequences of bits, so that each fn maps N to {0,1}, and then
let S1 be the set of n such that a 1 occurs in fn, and the
first 1 to occur is at an even position in the sequence,
and S2 be the set of n such that a 1 occurs in fn, and the
first 1 to occur is at an odd position in the sequence.
Using a standard diagonal trick, if we are given two
disjoint recursively enumerable sets U and V, we can cook
up an n such that fn simulates the enumerations of U and V
and looks to see whether n appears in either of them. Then
if n appears in U, fn arranges to put a 1 bit in an odd
position, and if n appears in V, fn arranges to put a 1 bit
in an even position (first). This foils any attempt to
separate S1 and S2 using U and V thus: n is in U iff n is
in S2 and n is in V iff n is in S1. So if U contains S1,
and V contains S2, then n is in neither U nor V.
|Now given an integer x the statement "T2 never generates x" (that is,
|"x does not belong to S2") is Pi_1. Consider the set C of x such that
|this is a theorem of Peano: if the set of Pi_1 theorems of Peano
|arithmetic were recursive, then C would be recursive. Certainly, C is
|disjoint from S2 because Peano is sound. But conversely, if x belongs
|to S1 then that fact is a theorem in Peano (because it is a Delta_0
|statement), so it is also a theorem in Peano that T2 never generates x
|(because by assumption Peano proves disjointness of S1 and S2), i.e.,
|x belongs to C. So we have a recursive set C which contains S1 and is
|disjoint from S2, a contradiction.
Using the above slight generalization of recursive
inseparability, we can avoid having to assume that the pi^0_1
theorems of PA are recursive. Instead we can just use the
(true) fact that they are recursively enumerable. Using the
pair U={x : PA proves that x is not in S2} and V is any
recursively enumerable set disjoint from U, we cook
up an x such that x is in U iff x is in S2 and x is in V
iff x is in S1. But U is disjoint from S2, so x is not in
U or S2. And since x is not in U, as you note x is also not
in S1 (which would allow PA to realize it is not in S2).
Hence x is not in U or V.
|In fact the reasoning above shows that the set of Pi_1 theorems of
|Peano and the set of Pi_1 antitheorems (=negation is a theorem) are
|recursively inseparable.
Yes.
|So it is not possible that for all Pi_1
|statements P either Peano+Consis(Peano) proves Consis(Peano+P) or
|Peano+Consis(Peano) proves Consis(Peano + not-P): for if this were the
|case we would have a recursive separation of the set of Pi_1 theorems
|into certain consistent statements (including all Pi_1 theorems) and
|certain unprovable statements (including all Pi_1 antitheorems).
Well, I would certainly expect this to be true, but it is
a little unclear to me at first glance. The sets of P for
which consis(PA+P) and for which consis(PA+~P) respectively
are provable in PA+consis(PA) are not disjoint. I was going
to try to sketch out a construction like this explicitly,
but only for the failure of some disjoint sets to separate
the theorems from the false sentences.
[...]
|I'd still like to find a textbook reference to such questions, because
|I'm sure there are more interesting things to be said than my modest
|knowledge will let me discover.
I would guess a lot of this would follow as corollaries to
results about "provability logic". The provability of X is
sometimes denoted []X since provability has some properties
in common with other operators like necessity also represented
using the "box". A lot of these questions can be phrased in
terms of []. There are a few fundamental theorems such as
[]([]X->X)->[]X that hold for provability in a formal system
like PA. I'm afraid I'm not all that familiar with it though.
Keith Ramsay
David Madore
<1141530651.2...@e56g2000cwe.googlegroups.com> scripsit:
> David Madore wrote:
> |David Madore in litteris <dtn8q2$fea$1...@news.ks.uiuc.edu> scripsit:
> |> Is the set of Pi_1 theorems of Peano arithmetic nonrecursive?
> [...]
> |Peano and the set of Pi_1 antitheorems (=negation is a theorem) are
> |recursively inseparable.
>
> Yes.
>
> |So it is not possible that for all Pi_1
> |statements P either Peano+Consis(Peano) proves Consis(Peano+P) or
> |Peano+Consis(Peano) proves Consis(Peano + not-P): for if this were the
> |case we would have a recursive separation of the set of Pi_1 theorems
> |into certain consistent statements (including all Pi_1 theorems) and
> |certain unprovable statements (including all Pi_1 antitheorems).
>
> Well, I would certainly expect this to be true, but it is
> a little unclear to me at first glance. The sets of P for
> which consis(PA+P) and for which consis(PA+~P) respectively
> are provable in PA+consis(PA) are not disjoint. I was going
> to try to sketch out a construction like this explicitly,
> but only for the failure of some disjoint sets to separate
> the theorems from the false sentences.
Ah, yes, I should have been clearer about this, since I also noticed
the difficulty. The trick is to do this: assume that for all Pi_1
statements P either Peano+Consis(Peano) proves Consis(Peano+P) or
Peano+Consis(Peano) proves Consis(Peano + ~P); then take a Turing
machine which enumerates proofs in Peano+Consis(Peano) and stops as
soon as it reaches a proof of either Consis(Peano+P) or of
Consis(Peano + ~P): by assumption it always stops, so it classifies
(well-formed) Pi_1 statements in two bins: the first one contains
those for which it stops with a proof of Consis(Peano+P) first, and
the other is the complement. Now every theorem of Peano must be in
the first bin because if P is a theorem then Consis(Peano + ~P) is
certainly not true, let alone provable, and similarly if ~P is a
theorem then P is in the second bin. So we have a recursive
separation of Pi_1 theorems and antitheorems, a contradiction.
(The idea of taking the first proof which shows up is the essential
idea of the Gödel-Rosser theorem, as opposed to the usual Gödel
theorem.)
To tie it all up, we can take the following statement G:
"there exists a proof of Consis(PA+~G) in PA+Consis(PA) such that
there is no earlier (smaller) proof of Consis(PA+G) (still in
PA+Consis(PA))"
(by the usual "Quinean" trick, the fact that the definition of G
involves its own code does not cause any difficulty).
Now there cannot be a proof of Consis(PA+G) or Consis(PA+~G) (or
both!) in PA+Consis(PA), because if there were, the one with the
smaller proof would give a contradiction (for example, if
Consis(PA+~G) had a proof smaller than any of Consis(PA+G), then
_that_ fact would be a theorem of PA, or even Robinson arithmetic, so
G would be a theorem of PA, so Consis(PA+~G) could not be provable in
PA+Consis(PA) - assuming PA+Consis(PA) is consistent). So ~G (which
is Pi_1) is true, but it is neither provable (nor, obviously,
refutable) in PA and its consistency and unprovability are themselves
not provable (nor, obviously, refutable) in PA+Consis(PA).
> [...]
> |I'd still like to find a textbook reference to such questions, because
> |I'm sure there are more interesting things to be said than my modest
> |knowledge will let me discover.
>
> I would guess a lot of this would follow as corollaries to
> results about "provability logic". The provability of X is
> sometimes denoted []X since provability has some properties
> in common with other operators like necessity also represented
> using the "box". A lot of these questions can be phrased in
> terms of []. There are a few fundamental theorems such as
> []([]X->X)->[]X that hold for provability in a formal system
> like PA. I'm afraid I'm not all that familiar with it though.
I'm afraid we can't avoid the use of some form of "earliest proof" as
explained above, and I don't think this can be done using provability
logic as such.