[FOM] 302: PA Completeness

Sun Oct 29 02:38:04 EST 2006

We consider PA as formulated with the primitives

0,S,+,dot.

QUESTION: All of the axioms of PA are of a special fundamental character
that comes from "logical reflection" or "prescribing the setup" rather than
"detailed understanding of facts about the ring of natural numbers of a
standard mathematical character". Does PA leave out something of such a
special fundamental character? I do not believe so.

A more specific question is this:

QUESTION: Does PA prove all sentences in its language which are of no
greater "complexity" than its axioms (schemes)? I am very confident that
this is true.

This leads to a number of novel formal investigations into PA. I hope to
find time to pursue these.

PA

not(Sx = 0).
Sx = Sy implies x = y.
x+0 = 0.
x+Sy = S(x+y).
x dot 0 = 0.
x dot Sy = (x dot y) + x.
(forall x)(R(x) implies R(S(x))) implies (R(0) implies R(x)).

The last axiom is an axiom scheme using the unary schematic relation symbol
R. Under the appropriate theory of scheme presentations, this indicates all
legal substitution instances. I.e., R is to be replaced using any formula
phi none of whose variables appear in the scheme, paired with a variable y
that does not appear in the scheme, and which does not appear bound in phi.
Then any R(t) shown in the scheme is to be replaced by phi[y/t].

In looking at these axioms, we are struck by their simplicity in that

i. There are at most two variables in each axiom (scheme).
ii. The complexity of all of the terms that appear in each axiom (scheme) is
very low. 

Let us measure the complexity of terms by

c(variable) = c(constant) = 0.
c(op(-,...,-)) = 1+max(c(-),...,c(-)).

The complexity of the terms appearing in this axiomatization are at most 2.

The term complexity of a formula or scheme is the maximum of the
complexities of the terms that appear.

CONJECTURE. Every true sentence in 0,S,+,dot with at most two variables and
term complexity at most 2, is provable in PA (and even in EFA). Every
instance of every universally true scheme in 0,S,+,dot and the unary
schematic letter R, with at most two variables and term complexity at most
2, is provable in PA.

Why 2,2? Because 2,2 is sufficient to axiomatize PA.

It looks like the numbers 2,2 have to be raised somewhat before we bump up
into sentences (schemes) in the language of PA whose truth value is not
known. The numbers 2,2 have to be considerably raised in order to
accommodate any sentences (schemes) that are known to be independent of PA.

Once we establish the Conjecture, we can seek to strengthen it considerably
- in many ways. E.g., allow more schematic letters (even binary and higher),
more variables, more term complexity, etc.

**********************************

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 302nd 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM
276: Higman/Kruskal/impredicativity  4/4/06  6:31AM
277: Strict Predicativity  4/5/06  1:58PM
278: Ultra/Strict/Predicativity/Higman  4/8/06  1:33AM
279: Subcubic graph numbers/restated  4/8/06  3:14AN
280: Generating large caridnals/self embedding axioms  5/2/06  4:55AM
281: Linear Self Embedding Axioms  5/5/06  2:32AM
282: Adventures in Pi01 Independence  5/7/06
283: A theory of indiscernibles  5/7/06  6:42PM
284: Godel's Second  5/9/06  10:02AM
285: Godel's Second/more  5/10/06  5:55PM
286: Godel's Second/still more  5/11/06  2:05PM
287: More Pi01 adventures  5/18/06  9:19AM
288: Discrete ordered rings and large cardinals  6/1/06  11:28AM
289: Integer Thresholds in FFF  6/6/06  10:23PM
290: Independently Free Minds/Collectively Random Agents  6/12/06  11:01AM
291: Independently Free Minds/Collectively Random Agents (more)  6/13/06
5:01PM
292: Concept Calculus 1  6/17/06  5:26PM
293: Concept Calculus 2  6/20/06  6:27PM
294: Concept Calculus 3  6/25/06  5:15PM
295: Concept Calculus 4  7/3/06  2:34AM
296: Order Calculus  7/7/06  12:13PM
297: Order Calculus/restatement  7/11/06  12:16PM
298: Concept Calculus 5  7/14/06  5:40AM
299: Order Calculus/simplification  7/23/06  7:38PM
300: Exotic Prefix Theory   9/14/06   7:11AM
301: Exotic Prefix Theory (correction)  9/14/06  6:09PM

Harvey Friedman 