FOM: 65:Simplicity of Axioms/Conjectures
Harvey Friedman
friedman at math.ohio-state.edu
Tue Oct 19 09:54:20 EDT 1999
This is the 65th in a series of self contained postings to FOM covering a
wide range of topics in f.o.m. Previous ones are:
1:Foundational Completeness 11/3/97, 10:13AM, 10:26AM.
2:Axioms 11/6/97.
3:Simplicity 11/14/97 10:10AM.
4:Simplicity 11/14/97 4:25PM
5:Constructions 11/15/97 5:24PM
6:Undefinability/Nonstandard Models 11/16/97 12:04AM
7.Undefinability/Nonstandard Models 11/17/97 12:31AM
8.Schemes 11/17/97 12:30AM
9:Nonstandard Arithmetic 11/18/97 11:53AM
10:Pathology 12/8/97 12:37AM
11:F.O.M. & Math Logic 12/14/97 5:47AM
12:Finite trees/large cardinals 3/11/98 11:36AM
13:Min recursion/Provably recursive functions 3/20/98 4:45AM
14:New characterizations of the provable ordinals 4/8/98 2:09AM
14':Errata 4/8/98 9:48AM
15:Structural Independence results and provable ordinals 4/16/98
10:53PM
16:Logical Equations, etc. 4/17/98 1:25PM
16':Errata 4/28/98 10:28AM
17:Very Strong Borel statements 4/26/98 8:06PM
18:Binary Functions and Large Cardinals 4/30/98 12:03PM
19:Long Sequences 7/31/98 9:42AM
20:Proof Theoretic Degrees 8/2/98 9:37PM
21:Long Sequences/Update 10/13/98 3:18AM
22:Finite Trees/Impredicativity 10/20/98 10:13AM
23:Q-Systems and Proof Theoretic Ordinals 11/6/98 3:01AM
24:Predicatively Unfeasible Integers 11/10/98 10:44PM
25:Long Walks 11/16/98 7:05AM
26:Optimized functions/Large Cardinals 1/13/99 12:53PM
27:Finite Trees/Impredicativity:Sketches 1/13/99 12:54PM
28:Optimized Functions/Large Cardinals:more 1/27/99 4:37AM
28':Restatement 1/28/99 5:49AM
29:Large Cardinals/where are we? I 2/22/99 6:11AM
30:Large Cardinals/where are we? II 2/23/99 6:15AM
31:First Free Sets/Large Cardinals 2/27/99 1:43AM
32:Greedy Constructions/Large Cardinals 3/2/99 11:21PM
33:A Variant 3/4/99 1:52PM
34:Walks in N^k 3/7/99 1:43PM
35:Special AE Sentences 3/18/99 4:56AM
35':Restatement 3/21/99 2:20PM
36:Adjacent Ramsey Theory 3/23/99 1:00AM
37:Adjacent Ramsey Theory/more 5:45AM 3/25/99
38:Existential Properties of Numerical Functions 3/26/99 2:21PM
39:Large Cardinals/synthesis 4/7/99 11:43AM
40:Enormous Integers in Algebraic Geometry 5/17/99 11:07AM
41:Strong Philosophical Indiscernibles
42:Mythical Trees 5/25/99 5:11PM
43:More Enormous Integers/AlgGeom 5/25/99 6:00PM
44:Indiscernible Primes 5/27/99 12:53 PM
45:Result #1/Program A 7/14/99 11:07AM
46:Tamism 7/14/99 11:25AM
47:Subalgebras/Reverse Math 7/14/99 11:36AM
48:Continuous Embeddings/Reverse Mathematics 7/15/99 12:24PM
49:Ulm Theory/Reverse Mathematics 7/17/99 3:21PM
50:Enormous Integers/Number Theory 7/17/99 11:39PN
51:Enormous Integers/Plane Geometry 7/18/99 3:16PM
52:Cardinals and Cones 7/18/99 3:33PM
53:Free Sets/Reverse Math 7/19/99 2:11PM
54:Recursion Theory/Dynamics 7/22/99 9:28PM
55:Term Rewriting/Proof Theory 8/27/99 3:00PM
56:Consistency of Algebra/Geometry 8/27/99 3:01PM
57:Fixpoints/Summation/Large Cardinals 9/10/99 3:47AM
57':Restatement 9/11/99 7:06AM
58:Program A/Conjectures 9/12/99 1:03AM
59:Restricted summation:Pi-0-1 sentences 9/17/99 10:41AM
60:Program A/Results 9/17/99 1:32PM
61:Finitist proofs of conservation 9/29/99 11:52AM
62:Approximate fixed points revisited 10/11/99 1:35AM
63:Disjoint Covers/Large Cardinals 10/11/99 1:36AM
64:Finite Posets/Large Cardinals 10/11/99 1:37AM
In this installment, we only consider PA.
INTRODUCTION
We start with the crucial question:
*Where do the usual axioms for mathematics come from?*
We can focus on the axioms of set theory, which form the standard
presentation of the axioms for mathematics.
*Where do the usual axioms for set theory come from?*
And we can also focus on axioms for parts of mathematics as, e.g.,
designated by their primitives. Thus
*Where do the usual axioms for finite set theory come from?*
*Where do the usual axioms for arithmetic come from?*
*Where do the usual axioms for second order arithmetic come from?*
*Where do the usual axioms for n-th order arithmetic come from?*
*Where do the usual axioms for type theory come from?*
There are a number of different views towards these issues. Here are some.
1. They come from our intuition. We see that these axioms are clearly true.
In the future, we expect to find additional axioms that are clearly true.
2. They come from our intuition. We see that these axioms are clearly true.
But they are complete in the sense that we do not expect to find additional
axioms that are clearly true. However, we will accept additional axioms on
the basis of "evidence."
3. They come from our intuition. We see that these axioms are clearly true.
But they are complete in the sense that we do not expect to find additional
axioms that are clearly true. And we will never accept additional axioms on
the basis of "evidence" because the notion of "evidence" does not apply to
this context.
In this posting, I don't want to pursue the line of thought represented by
1-3, but instead a quite different line of thought.
4. The axioms are forced on us merely by the choice of primitives, and the
requirement that the axioms be simple.
And what if we pick other primitives?
5. Statement 4 holds for any reasonable choice of primitives. The same
axiom systems arise - up to Tarski interpretation - regardless of the
choice of primitives, including category theoretic primitives.
We conjecture that the usual formal systems used to formalize mathematics
are uniquely determined - up to provable equivalence - as the simplest
formalizations that are sufficient to formalize mathematics. Simpler
formalizations will not be adequate.
We also have a number of conjectures about formal systems that are
successively more complicated than the simplest ones.
1. PROVABLE FORMULAS OF PA
PA is Peano Arithmetic, which we will take to be as follows. The language
is =,0,S,+,x. We have the usual axioms and rules of inference for predicate
calculus with equality in this language. We use forall, therexists, not,
and, or, implies.
The nonlogical axioms are as follows.
1. Quantifier free axioms. These consist of the equational axioms a+0 = a,
a+(S(b)) = S(a+b), ax0 = 0, ax(S(b)) = axb + a, and the two axioms S(a) not=
0, S(a) = S(b) implies a = b.
2. Induction axioms. (A[x/0] & (forall x)(A implies A[x/S(x)])) implies A,
where A is any formula in the language of PA.
A symbol in a formula is a variable, a constant symbol, a relation symbol
(including =), a function symbol, a connective, and a quantifier. We take
(forall x) and (therexists x) to each have two symbols - the quantifier and
the variable. We do not count parentheses and commas as symbols.
When we count the number of symbols in a formula, we count duplications.
Note that there are finitely many formulas with a given number of symbols
up to change of symbols.
CONJECTURE 1.1. Let phi be a formula in the language of PA with at most 20
symbols. The universal closure of phi is provable or refutable in PA.
CONJECTURE 1.2. There is a formula phi in the language of PA with at most
50 symbols such that the universal closure of phi is neither provable nor
refutable in PA.
2. PROVABLE SCHEMES OF PA
As we shall see, there is added significance when we state such conjectures
for schemes. We first need a general framework for discussing schemes.
For this purpose, we introduce special "schematic" letters A_1, A_2,... to
predicate calculus
with equality. A scheme is a formula in predicate calculus with equality
which mentions zero or more of the schematic letters in the syntactic role
of an ordinary relation symbol of definite arity. In other words, i.e., any
two occurrences of the same schematic letter must be used with the same
arity - as is the case with relation symbols. Formulas in predicate
calculus with equality are vacuously considered schemes.
Let phi be a scheme. A substitution map for phi is a function h whose
domain is the set of schematic letters in phi, such that
*h(A_i) is a tuple (psi,y_1,...,y_k), where psi is a formula whose free
variables do not include any bound variables of phi, and the y's are
distinct variables not appearing in phi, and not bound in psi, where A_i
appears in phi with arity k.*
We implement h on phi as follows. Take h[phi] to be the result of replacing
each atomic formula A_i(t_1,...,t_k) in phi by h(A_i)(y_1/t_1,...,y_k/t_k).
For example, the induction scheme in section 1 is presented as (A(0) &
(forall x)(A(x) implies A(S(x))) implies A(x). Note that this has 14
symbols.
What does it mean for a scheme to be provable in a theory T? The crudest
notion is as follows. Let h be a subsitution map for phi whose values are
in the language of T. Then the formula h[phi] is provable in T. Note that
this is a Pi-0-2 condition, and therefore it may hold but not demonstrably
hold. We would prefer a notion of uniformly provable. We take this matter
up in section 3.
A scheme is said to be refutable in T if and only if there is some
substitution map h for phi whose values are in the language of T, such that
the universal closure of h[phi] is refutable in T.
CONJECTURE 2.1. Let phi be a scheme in the language of PA with at most 20
symbols. The universal closure of phi is provable or refutable in PA.
CONJECTURE 2.2. There is a scheme in the language of PA with at most 50
symbols such that the universal closure of phi is neither provable nor
refutable in PA.
So far, our conjectures do not single out PA as having special status. Let
EFA be the weak fragment of PA known as exponential function arithmetic.
There are many equivalent formulations of EFA. For our purposes, we take
EFA to have the same language as PA, with the following axioms:
i) the quantifier free axioms of PA;
ii) for all n there exists m such that every 1 <= i <= n divides m;
iii) induction for all formulas in the language with bounded quantifiers.
EFA is finitely axiomatizable.
CONJECTURE 2.3. Every scheme in the language of PA with at most 13 symbols
is provable or refutable in EFA. This is false for 14 symbols, since the
induction scheme has 14 symbols and is known to be not provable in EFA.
We conjecture that we can reaxiomatize PA as follows.
CONJECTURE 2.4. PA is reaxiomatized by taking the union of all schemes with
at most 14 symbols which are consistent with EFA, and also by taking the
union of all schemes with at most 20 symbols which are consistent with EFA.
The special status that PA occupies can be more clearly stated by the
following conjecture. For each i >= 1, let W[i] be the set of all schemes
with at most i symbols that are consistent with EFA.
CONJECTURE 2.5. Let i be least such that not all elements of W[i] are
provable in EFA. Then the union of W[i] forms a reaxiomatization of PA.
Some element of W[i] is a reaxiomatization of PA. For any two elements of
W[i], one is provable from the other over EFA. We also conjecture that i =
14.
We also have conjectures for the higher W[i].
CONJECTURE 2.6. Let j be least such that there are two elements of W[j],
neither of which is provable from the other over EFA. Then there exists phi
in W[j-1] such that phi has consistency strength that of ZF + "there exists
a nontrivial elementary embedding from V into V." Furthermore, W[j-1] has
representatives of all of the usual levels of set theory and large
cardinals considered by logicians.
We also conjecture that in the above conjectures, we can replace EFA with a
small number of simple mathematically natural consequences of EFA.
3. UNIFORMLY PROVABLE SCHEMES
It is more appropriate to use the sharper notion of uniformly provable
schemes rather than just provable schemes. Let phi, psi be two schemes in
the language of T. We can view phi as a formula in the language of T
extended by the schematic letters as new relation symbols. And we can make
substitutions of psi where the schematic letters are allowed in the range
of the substitution map. We say that phi is uniformly provable from psi
over T if and only if phi is provable from finitely many such substitutions
of psi over T.
We make the conjectures in section also for "provable" replaced by
"uniformly provable." In fact, we conjecture that in the W[j-1] of
Conjecture 2.6, provability and uniform provability are the same.
We also conjecture that as in section 2, we can replace EFA with a small
number of simple mathematically natural consequences of EFA.
4. COMPUTER INVESTIGATIONS
It would be very useful to list all of the short formulas - say up through
14 symbols - and run an automated theorem prover on them that is reasonably
good at proving things from PA. Then see how many cases remain that have to
be eyeballed by a human. This should also be done with schemes. One could
then take a random sample of what remains for two purposes:
1) to get an estimate as to how many man hours is involved in going through
the remaining cases;
2) to perhaps find a few key theorems of EFA that might help the automated
theorem prover dispense with many more cases.
As the theorem prover dispenses with more cases, the remaining cases can
again be sampled by a human.
5. PRIOR POSTING
The following is from posting #4. Note the alternative complexity measure.
If you formulate PA in the standard way in the language 0,S,+,x, with a
free monadic letter R used as a place marker in the induction scheme, one
sees that every axiom (scheme) has at most 5 occurrences of variables. In
fact, they all have at most 5 occurrences of variables/constants. I.e., we
count the total number of occurrences of variables and constants (in this
case the only constant is 0).
Here are some conjectures.
1. The set of all universally true formulas without R with at most 5
occurrences of variables/constants is decidable. There is a simple
axiomatization.
2. The set of all universally true formulas with (or without) the free
monadic letter R with at most 5 occurrences of variables/constants is
decidable in two senses. Firstly, that all arithmetic interpretations of R
are used. Secondly, that all interpretations of R (i.e., using all monadic
relations on N) are used. And one gets the same universally true formulas
in either case. Furthermore, if one considers the set of all such
universally true formulas, and interprets this as an axiomatization of
arithmetic with schemes, then one gets a system that is logically
equivalent to PA.
Now don't get me wrong: I am not asserrting that this count is the right
way to do complexity here. We are just trying to get our feet wet with some
new brands of f.o.m. research. F.o.m. has a nice red-blooded experimental
nature to it, which flows rather freely. If one's intuition is sufficiently
good to ask a more or less right question, then this is bound to lead to
even better right questions, and then to discoveries of obviously permanent
value.
More information about the FOM
mailing list