Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.

Dismiss

55 views

Skip to first unread message

Feb 24, 2006, 10:30:10 AM2/24/06

to

Hi,

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/ )

Feb 24, 2006, 12:30:17 PM2/24/06

to

David Madore in litteris <dtn8q2$fea$1...@news.ks.uiuc.edu> scripsit:

> Is the set of Pi_1 theorems of Peano arithmetic nonrecursive?

> 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.

Mar 4, 2006, 10:50:51 PM3/4/06

to

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?

[...]|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

Mar 5, 2006, 6:36:59 PM3/5/06

to

"Keith Ramsay" in litteris

<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?

> [...]

<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?

> [...]

> |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.

> |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.

0 new messages

Search

Clear search

Close search

Google apps

Main menu