# FOM: Leo credit/n^n(p)/sequences

Harvey Friedman friedman at math.ohio-state.edu
Tue Sep 15 19:44:58 EDT 1998

```This is a short note on three unrelated topics.

1. About my posting 20:Proof Theoretic Degrees, 9:37PM 8/2/98. I found an
old manuscript dated **Februrary 1977** (am I that old?) which clarifies
some credit issues.

In that manuscript, I start by giving proofs of two results:

I). Suppose PA proves "A implies Con(PA)". Then there exists a sigma-0-1
sentence B such that PA proves "A if and only if Con(PA + B)."

II). Suppose PA proves "A implies Con(PA)". Then there exists a pi-0-1
sentence B such that PA proves "A if and only if Con(PA + B)."

There I attribute result I) to Leo Harrington (on the FOM!). Then I go on
to say that of course B must in general be false, and so what if we want B
to be true (assuming A is true)? Then I answer this strongly in the
affirmative by proving II), which I took credit for. (In fact, if A is
consistent with PA then B will be a true pi-0-1 sentence).

I also credit Solovay for the existence of two sentences A,B of PA such
that PA does not prove "Con(PA + A) implies Con(PA + B)," and PA does not
prove "Con(PA + B) implies Con(PA + A)." I don't give any more details
about Solovay's result, such as what kind of sentences A,B are. Of course,
this result can be obtained as a consequence of a or b.

I also answered a question of Steel and Smorynski: is there a recursive
sequence of true sentences A1,A2,..., such that for all i, PA proves Ai
implies Con(PA + Ai)? I give an explicit example of such true pi-0-1
sentences without resorting to self reference.

2. Tennant has pointed out a possible confusion with the use of my notation
k^k(p) in posting 7:29PM 9/15/98. k^k(p) is the result of multiplying k^k
with p.

3. In my posting "length of proofs" of 9/16/98, I neglected to mention the
obvious advantage of the n(k) approach: one simply is writing down a
succession of integers - as opposed to other approaches, where one is, say,
writing down a succession of finite sequences of integers.

```