[FOM] 304: PA Completeness/strategy
Harvey Friedman
friedman at math.ohio-state.edu
Sat Nov 4 10:57:10 EST 2006
We begin with some general remarks concerning the paradigm shift represented
by investigations in the style of the PA Completeness investigation. (This
is not to say that there is anything illegitimate about traditional and
ongoing PA Incompleteness investigations).
We begin with the observation that many of our usual formal systems for
f.o.m. are obtained by first specifying a language and then formulating as
many "obvious natural fundamental axioms" as one can come with up within the
specified language.
F.o.m. is generally speaking absorbed by the various incompleteness
phenomena. Of course, an exception is where one has completeness in the
strong sense - e.g., the theory of real closed fields. But even here, there
is substantial incompleteness phenomena of a more subtle nature connected
with lengths of proof and computational complexity.
In this paradigm shift, we concentrate instead on the various senses in
which PA (and other systems) are complete.
At the outset, we can expect to establish completeness in an important but
special sense:
*That any true fact in the language of 0,S,+,dot that is no more complicated
than the usual axioms and axiom schemes for PA, is already provable in PA.*
This is well within reach for a variety of very reasonable notions of "no
more complicated".
What is harder to obtain in a truly convincing way is
**That any serious axiom or axiom (scheme) candidate in the language of
0,S,+,dot is already provable in PA.**
Complexity measures on schemes are entirely natural and appropriate and fit
in well with basic mathematical logic. For example, the axiom scheme
A implies A
is very simple, and is appropriately measured by the complexity of what is
written.
The latter will be obtained incrementally over long periods of time with
results that are more and more compelling. But I don't want to rule out the
stunning discovery of a truly convincing notion of "axiom (scheme)
candidate" for which one can prove that any such is already provable in PA.
Let me mention a fundamental point that is easily missed. Suppose that at
some stage we consider a natural (finite) family of sentences in 0,S,+,dot
that is sufficiently rich to contain well known open number theoretic
conjectures. E.g., the twin prime conjecture.
Of course, this will prevent us from actually showing that every true
element of that family is already provable in PA (at least for a long time).
HOWEVER, this is not really an obstacle to **. For it is completely obvious
that
***The twin prime conjecture is not a serious axiom candidate***.
Let me illustrate this point as follows. Suppose we can show that all true
sentences in this rich family are provable in PA with a list of possible
exceptions that we don't know the truth value of.
We can then hope to argue in some convincing way that none of these
exceptions are axiom candidates. If the only exception is the twin prime
conjecture, then of course we are done. More realistically, we might show
that these exceptions are all equivalent to well known open number theoretic
problems and variants thereof. We would then want to argue that none of them
are axiom candidates - and various arguments will be given, including "it it
obvious that...".
The above discussion lays the groundwork for the importance and potential
importance of such completeness investigations for f.o.m. in a SUFFICIENTLY
CONVINCING way.
SUFFICIENTLY CONVINCING for what?
Every such foundational program immediately leads to incremental formal
investigations of great depth,
****THAT TAKE ON A LIFE OF THEIR OWN.****
E.g., Reverse Mathematics, Concrete Independence Results, Concept Calculus,
and several others that have set up over the years.
SUFFICIENTLY CONVINCING to appropriately motivate the pursuit of the
associated formal investigations on the part of those with sufficient
interest in f.o.m. and sufficient abilities.
1. A NEW FORMULATION.
It is a challenge to come up with a complexity measure for sentences and
sentence schemes in 0,S,+,dot which lead to powerful results of the kind we
want than can actually be obtained.
Currently we are most optimistic about the following complexity measure.
*The number of occurrences of general operations*.
In the case of sentences, the general operations are
not, and, or, implies, iff, S,+,dot,=, forall, therexists.
In the case of axiom schemes, we add the schematic symbols to this list.
Let us look at the counts for the various axioms of PA.
1. (forall x)(not Sx = 0). 4.
2. (forall x)(forall y)(Sx = Sy implies x = y). 7.
3. (forall x)(x + 0 = x). 3.
4. (forall x)(forall y)(x+Sy = S(x+y)). 7.
5. (forall x)(x dot 0 = 0). 3.
6. (forall x)(forall y)(x dot Sy = (x dot y) + x). 7.
7. (forall x)(R(x) implies R(Sx)) implies (forall x)(R(x)). 8.
Also
(forall x)(forall y)(forall z)(x+(y+z) = (x+y)+z). 8.
(forall x)(forall y)(forall z)(x dot y+z = x dot y + x dot z). 9.
CONJECTURE. Every true sentence in 0,S,+,dot with general operation
complexity at most 7 is provable in PA. This is also true for 8. This is
also true for 9,10,11.
The Twin Prime Conjecture appears to be the smallest under general operation
complexity of the open problems, coming in at 12. For reasons given earlier
we should not be automatically frightened of 12.
There is another closely related complexity measure. Count the number of
symbols, except for parentheses. This is the same as general operation
complexity except that we add the number occurrences of variables and 0.
Under this measure you get penalized 2 for each quantifier. The shape of the
results ought to be the same, but the numbers are higher.
CONJECTURE. Every instance of every true sentence scheme in 0,S,+,dot with
general operation complexity at most 8 is provable in PA. This is also true
for 9,10,11.
2. SOME PA COMPLETENESS.
THEOREM 2.1. Any universal sentence in 0,S,+,dot that is true in the reals
is provable in PA. Any scheme in 0,S and unary schematic letters is true for
all set interpretations of those letters if and only if every substitution
by formulas in 0,S,+,dot is true in the natural numbers if and only if every
substitution by formulas in 0,S,+,dot is provable in PA.
THEOREM 2.2. PA can be axiomatized as follows.
1. All universal sentences in 0,S,+,dot true in the reals.
2. All schemes using only 0,S and unary schematic letters all of whose
substitution instances in 0,S,+,dot are true.
Note that these results do not treat sentences and schemes the same way. In
terms of the original motivation, this is not good.
THEOREM 2.3. Let A be a sentence in 0,S,+,dot, with two quantifiers, in
which all terms use at most two operation symbols. Then A is true iff A is
provable in (a weak fragment of) PA.
This class of sentences contains the axioms of PA except for the axiom
scheme of induction.
CONJECTURE. Let A be a sentence in 0,S,+,dot, with three quantifiers, in
which all terms use at most two operation symbols. Then A is true iff A is
provable in (a weak fragment of) PA.
This class of sentences also includes the associative law of addition.
To include the distributive law, we make the following conjecture.
CONJECTURE. Let A be a sentence in 0,S,+,dot, with three quantifiers, in
which all terms use at most three operation symbols. Then A is true iff A is
provable in (a weak fragment of) PA.
**********************************
I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 304th 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
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
Harvey Friedman
More information about the FOM
mailing list