# [FOM] 747: PA Incompleteness/2

Harvey Friedman hmflogic at gmail.com
Fri Feb 3 12:07:18 EST 2017

```NOTES FOR A RECENT TALK AT STANFORD HAS BEEN PLACED AT
#67.

######################################################

This continues the prior PA Incompleteness/1,
http://www.cs.nyu.edu/pipermail/fom/2016-September/020083.html In
particular, his improves on
http://www.cs.nyu.edu/pipermail/fom/2013-August/017469.html.

This development, because of the smooth entrance of polynomials and
the particularly compelling Templates and Strategic Theme, takes PA
Incompleteness to a new strategic level in terms of professional
mathematical culture.

DEFINITION 1. N^k< is the set of all strictly increasing k-tuples from
the set N of nonnegative integers. For x,y in N^k, x <adj y if and
only if x,y in N^k< and (x_2,...,x_k) = (y_1,...,y_k-1). Note that
this proscribes a single order type for the 2k-tuple (x,y). x <=c y
means that each x_i <= y_i. Here <=c is read "<= coordinstewise".

ADJACENT LIFTING. Every f:N^k into N^k has some x <adj y with f(x) <=c f(y).

RECURSIVE ADJACENT LIFTING. Every recursive f:N^k into N^k has some x
<adj y with f(x) <=c f(y).

ELEMENTARY RECURSIVE ADJACENT LIFTING. Every elementary recursive
f:N^k into N^k has some x <adj y with f(x) <=c f(y).

POLYNOMIAL ADJACENT LIFTING. Every surjective polynomial P:N^k into
N^k has some x <=c y with P(x) <adj P(y).

Polynomial Adjacent Lifting is new, and improves on
http://www.cs.nyu.edu/pipermail/fom/2013-August/017469.html.

We moved to surjections in order to support the use of polynomials. We
can also use surjections for the first three above:

ADJACENT LIFTING'. Every surjective f:N^k into N^k has some x <=c y

RECURSIVE ADJACENT LIFTING'. Every recursive surjection f:N^k into N^k
has some x <=c y with f(x) <adj f(y).

ELEMENTARY RECURSIVE ADJACENT LIFTING'. Every elementary recursive
surjection f:N^k into N^k has some x <=c y with f(x) adj f(y).

to epsilon_0 is well ordered over RCA_0. Recursive Adjacent Lifting,
Recursive Adjacent Lifting' are provably equivalent to 2-Con(PA) over
EFA. Elementary Recursive Adjacent Lifting is provably equivalent to
1-Con(PA) over EFA. Elementary Recursive Adjacent Lifting' is provably
equivalent to 2-Con(PA) over EFA.

Proof: See http://cage.ugent.be/~pelupessy/ARPH.pdf Reference 
there has the wrong URL. It should be
http://u.osu.edu/friedman.8/files/2014/01/PA-incomp082910-2lgh5wm.pdf
QED

http://cage.ugent.be/~pelupessy/ARPH.pdf also discusses finite forms
of Adjacent Lifting with "for all k there exists n such that ...".

We will give a proof of the following here:

THEOREM 2. Polynomial Adjacent Lifting is provably equivalent to
2-Con(PA) over EFA. In particular, it is provable in ACA but not in
PA.

Instead of using Elementary Recursive above, we can use very low
complexity classes of f:N^k into N^k. Pushing this to the extreme will
require some research. I.e., we think it can probably be pushed nicely
into rather restrictive forms of real time complexity classes.

The above suggests the following fundamental Templates:

TEMPLATE A. Let R containedin N^2k+2r be order invariant. Every
(surjective) F:N^k into N^r has some x,y with R(x,y,F(x),F(y)).

TEMPLATE B. Let R containedin N^2k+2r be order invariant. Every
(surjective) recursive F:N^k into N^r has some x,y with
R(x,y,F(x),F(y)).

TEMPLATE C. Let R containedin N^2k+2r be order invariant. Every
(surjective) elementary recursive F:N^k into N^r has some x,y with
R(x,y,F(x),F(y)).

TEMPLATE D. Let R containedin N^2k+2r be order invariant. Every
(surjective) polynomial P:N^k into N^r has some x,y with
R(x,y,P(x),P(y)).

QUESTIONS. What are the relationships between these 8 Templates? Same
question for small k,r? Is every instance of these 8 Templates
provable or refutable in PA (ACA_0 for Template A)? Even provable in
PA or refutable in EFA (RCA_0 for Templates A)? At least for small
k,r?

STRATEGIC THEME. What are the purely order theoretic relations that
must be present between two arguments and their values in functions of
various kinds? This naturally throws you out of the PA realm.

LEMMA 3. EFA proves that Recursive Adjacent Lifting implies Polynomial

Proof: Assume Recursive Adjacent Lifting. Let P:N^k into N^k be a
surjective polynomial. Let f:N^k into N^k be recursive, where for all
x in N^k, P(f(x)) = x. Let x <adj y and f(x) <=c f(y). Then f(x) <=c
f(y) and P(f(x)) <adj P(f(y)). QED

LEMMA 4. Let f:N^k into N^k be recursive, k sufficiently large. There
is a polynomial P:N^3k into Z where for all x,y in N^k, f(x) = y if
and only if there exists z in N^k such that P(x,y,z) = 0. There exists
a surjective polynomial P*:N^3k into N^k such that the following
holds. If P*(x,y,z) in N^k< then P*(x,y,z) = x and y = f(x).

Proof: The first claim is a familiar positive form of the negative
solution to Hilbert's 10th Problem, since the graph of f is r.e. Now
define P*:N^3k into N^k by P*(x,y,z) = (x_1 +
((P(x,y,z)^2)x_2,x_2,...,x_k). Let P(x,F(x),z) = 0. Then P*(x,F(x),z)
= x, and so P* is surjective. Let P*(x,y,z) in N^k<. Then (x_1 +
((P(x,y,z)^2)x_2,x_2,...,x_k) is strictly increasing, and so P(x,y,z)
= 0 and P*(x,y,z) = x. Also f(x) = y if and only if there exists z
such that P(x,y,z) = 0. Hence f(x) = y. QED

LEMMA 5. (EFA) Suppose that for all sufficiently large k, every
recursive surjection f:N^3k into N^k has some x <=c y with f(x) <adj
f(y). Then Recursive Adjacent Lifting holds.

Proof: Let f:N^k into N^k be recursive. Let k < k', where k' is
sufficiently large according to the hypothesis. Define g:N^3k' into
N^k' by g(x,y,z) = f(x_1,...,x_k). Let (x,y,z) <=c (u,v,w), g(x,y,z)
<adj g(u,v,w). Then (x_1,...,x_k) <=c (u_1,...,u_k) and f(x_1,...,x_k)

LEMMA 6. EFA proves that Polynomial Adjacent Lifting implies Recursive

Proof: Assume Polynomial Adjacent Lifting. By Lemma 5, it suffices to
verify Recursive Adjacent Lifting for any recursive f:N^3k into N^k, k
sufficiently large. Let P* be given by Lemma 4. Let (x,y,z) <=c
(u,v,w) with P*(x,y,z) <adj P*(u,v,w). Then P*(x,y,z),P*(u,v,w) in
N^k<. Hence P*(x,y,z) = x, P*(u,v,w) = u, y = f(x), v = f(u). Hence x
<adj u and f(x) <=c f(u). QED

THEOREM 2. Polynomial Adjacent Lifting is provably equivalent to
2-Con(PA) over EFA. In particular, it is provable in ACA but not in
PA.

Proof: By Lemmas 3,6. QED

************************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
This is the 747th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-699 can be found at

700: Large Cardinals and Continuations/14  8/1/16  11:01AM
701: Extending Functions/1  8/10/16  10:02AM
702: Large Cardinals and Continuations/15  8/22/16  9:22PM
703: Large Cardinals and Continuations/16  8/26/16  12:03AM
704: Large Cardinals and Continuations/17  8/31/16  12:55AM
705: Large Cardinals and Continuations/18  8/31/16  11:47PM
706: Second Incompleteness/1  7/5/16  2:03AM
707: Second Incompleteness/2  9/8/16  3:37PM
708: Second Incompleteness/3  9/11/16  10:33PM
709: Large Cardinals and Continuations/19  9/13/16 4:17AM
710: Large Cardinals and Continuations/20  9/14/16  1:27AM
700: Large Cardinals and Continuations/14  8/1/16  11:01AM
701: Extending Functions/1  8/10/16  10:02AM
702: Large Cardinals and Continuations/15  8/22/16  9:22PM
703: Large Cardinals and Continuations/16  8/26/16  12:03AM
704: Large Cardinals and Continuations/17  8/31/16  12:55AM
705: Large Cardinals and Continuations/18  8/31/16  11:47PM
706: Second Incompleteness/1  7/5/16  2:03AM
707: Second Incompleteness/2  9/8/16  3:37PM
708: Second Incompleteness/3  9/11/16  10:33PM
709: Large Cardinals and Continuations/19  9/13/16 4:17AM
710: Large Cardinals and Continuations/20  9/14/16  1:27AM
711: Large Cardinals and Continuations/21  9/18/16 10:42AM
712: PA Incompleteness/1  9/23/16  1:20AM
713: Foundations of Geometry/1  9/24/16  2:09PM
714: Foundations of Geometry/2  9/25/16  10:26PM
715: Foundations of Geometry/3  9/27/16  1:08AM
716: Foundations of Geometry/4  9/27/16  10:25PM
717: Foundations of Geometry/5  9/30/16  12:16AM
718: Foundations of Geometry/6  101/16  12:19PM
719: Large Cardinals and Emulations/22
720: Foundations of Geometry/7  10/2/16  1:59PM
721: Large Cardinals and Emulations//23  10/4/16  2:35AM
722: Large Cardinals and Emulations/24  10/616  1:59AM
723: Philosophical Geometry/8  10/816  1:47AM
724: Philosophical Geometry/9  10/10/16  9:36AM
725: Philosophical Geometry/10  10/14/16  10:16PM
726: Philosophical Geometry/11  Oct 17 16:04:26 EDT 2016
727: Large Cardinals and Emulations/25  10/20/16  1:37PM
728: Philosophical Geometry/12  10/24/16  3:35PM
729: Consistency of Mathematics/1  10/25/16  1:25PM
730: Consistency of Mathematics/2  11/17/16  9:50PM
731: Large Cardinals and Emulations/26  11/21/16  5:40PM
732: Large Cardinals and Emulations/27  11/28/16  1:31AM
733: Large Cardinals and Emulations/28  12/6/16  1AM
734: Large Cardinals and Emulations/29  12/8/16  2:53PM
735: Philosophical Geometry/13  12/19/16  4:24PM
736: Philosophical Geometry/14  12/20/16  12:43PM
737: Philosophical Geometry/15  12/22/16  3:24PM
738: Philosophical Geometry/16  12/27/16  6:54PM
739: Philosophical Geometry/17  1/2/17  11:50PM
740: Philosophy of Incompleteness/2  1/7/16  8:33AM
741: Philosophy of Incompleteness/3  1/7/16  1:18PM
742: Philosophy of Incompleteness/4  1/8/16 3:45AM
743: Philosophy of Incompleteness/5  1/9/16  2:32PM
744: Philosophy of Incompleteness/6  1/10/16  1/10/16  12:15AM
745: Philosophy of Incompleteness/7  1/11/16  12:40AM
746: Philosophy of Incompleteness/8  1/12/17  3:54PM

Harvey Friedman
```