FOM: 94:Relative Completeness
Harvey Friedman
friedman at math.ohio-state.edu
Tue Sep 19 04:20:49 EDT 2000
In posting #93, 3:46AM 9/18/00, I defined
phi<_K psi if and only if
*phi,psi are formulas L(<,F) with at most the free variable x, such that in
every (A,<,F) lying in K, there exists a solution to phi which is greater
than all solutions to psi.*
That should be
phi >_K psi if and only if
*phi,psi are formulas L(<,F) with at most the free variable x, such that in
every (A,<,F) lying in K, there exists a solution to phi which is greater
than all solutions to psi.*
*****
This posting presents my ideas about the conjectured completeness of
various standard systems such as Peano Arithmetic, Z_2, Zermelo set theory
with bounded separation, ZF, and ZFC, in a clearer form than in earlier
postings. This matter, either directly or indirectly, was taken up
previously in postings 1,2,3,4,8,65,66,68,70.
1. RELATIVE COMPLETENESS OF FINITELY AXIOMATIZED THEORIES.
We want to be careful about the version of predicate calculus with equality
that we are using. In particular, we use constant, relation, and function
symbols. We use the connectives not, and, or, if then. We use the
quantiifers forall, therexists.
We define the complexity of a formula as the number of occurrences of
symbols, where each of the following counts as an occurrence:
i) a constant symbol
ii) a relation symbol
iii) a function symbol
iv) the equality symbol
v) a quantifier (without the variable)
vi) a variable
vii) a connective.
The only items that we do not count are parentheses and commas.
A theory T is a set of formulas. These formulas are interpreted
universally. We say that a formula A is a logical consequence of a theory T
if and only if every model of T (where the formulas in T are interpreted
universally) is a model of A (again where A is interpreted universally). An
axiomatization of T is a set of formulas K in first order predicate
calculus with equality which is semantically equivalent to T - i.e., has
the same models as T.
There is an important integer #(T) associated with any theory T. #(T) is
the least integer n such that T has an axiomatization consisting entirely
of formulas of complexity at most n.
Note that if a theory T uses only finitely many constant, relation, and
function symbols, then T is finitely axiomatizable if and only if #(T)
exists.
PROBLEM. Compute #(T) for various interesting theories T.
We now come to the definition of the concept of relative completeness.
DEFINITION. Let T be a finitely axiomatized theory. We say that T is
relatively complete if and only if for all formulas A of complexity at most
#(T), either A is a logical consequence of T or the negation of the
universal closure of A is a logical consequence of T.
We now come to the main conjecture about relative completeness of finitely
axiomatized theories.
CONJECTURE. All of the main systems of f.o.m. that are finitely
axiomatizable, and are inteneded to fully formalize a kind or level of
mathematical reasoning, are relatively complete. For example, Zermelo set
theory with bounded separation is relatively complete. Zermelo set theory
with bounded separation and the axiom of choice is relatively complete. The
fragment of Peano Arithmetic known as Sigma-0-1 induction is relatively
complete. The base theory for reverse mathematics, RCA_0, is relatively
complete.
2. RELATIVE COMPLETENESS OF THEORIES AXIOMATIZED BY FINITELY MANY SCHEMES.
We have to be careful about schemes in predicate calculus with equality.
We introduce schematic letters into predicate calculus with equality. Each
is of a definite arity >= 1. These are used just like relation symbols in
order to create a wider class of formulas called the schemes. A formula is
just a scheme with no schematic letters.
Let phi be a scheme. A substitution for phi is a function f from the set of
schematic letters occurring in phi into formulas subject to certain
conditions. Let R be a schematic letter occurring in phi of arity n >= 1.
Then f(R) is a formula such that
i) all constant, relation, and function symbols in f(R) are in phi;
ii) no variable occurs both free and bound in f(R);
iii) phi and f(R) have no variables in common;
iv) f(R) has at least n free variables.
The result of the substitution is as follows. Let w_1,...,w_n be the first
n free variables of f(R) in numerically ordered subscripts. Suppose
R(t_1,...,t_n) is an occurrence of R in phi. Then R(t_1,...,t_n) is
replaced by the result of replacing the variables w_1,...,w_n in f(R) by
t_1,...,t_n, respectively.
Let T be a set of schemes. Then T* is the set of all formulas that result
from all substitutions for all elements of T.
It is obvious that theories like PA, Z_2, ZF, and ZFC fall under this
setup. (Z_2 is many sorted; one can either use an obvious single sorted
version, or extend the above definition in a striaghtforward way to many
sorted predicate calculus).
A model of T is just a model of the associated theory T*.
We define the complexity of a scheme in the same way that we defined the
complexity of formulas. So we again define #(T) is the least integer n such
that T has an axiomatization by schemes consisting entirely of schemes of
complexity at most n.
PROBLEM. Compute #(T) for various interesting theories T finitely
axiomatized by schemes.
We now come to the definition of the concept of relative completeness.
DEFINITION. Let T be a theory finitely axiomatized by schemes. We say that
T is strongly relatively complete if and only if for all formulas A of
complexity at most #(T), either A is a logical consequence of T* or the
negation of the univeresal closure of A is a logical consequence of T*.
There is a stronger notion that is perhaps more natural.
DEFINITION. Let T be a theory finitely axiomatized by schemes. We say that
T is strongly relatively complete if and only if for all schemes psi of
complexity at most #(T), either every element of psi* is a logical
consequence of T* or the negation of the conjunction of the universal
closures of finitely many elements of psi* is a logical consequence of T*.
We now come to the main conjecture about relative completeness of theories
axiomatized by finitely many schemes.
CONJECTURE. All of the main systems of f.o.m. that are axiomatized by
finitely many schemes (virtually all of them), that are inteneded to fully
formalize a kind or level of mathematical reasoning, are (strongly)
relatively complete. For example, ZF is (strongly) relatively complete. ZFC
is (strongly) relatively complete. Zermelo set theory is (strongly)
relatively complete. Zermelo set theory with the axiom of choice is
(strongly) relatively complete. Peano Arithmetic is (strongly) relatively
complete. Z_2 is (strongly) relatively complete.
****************************
This is the 94th 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
65:Simplicity of Axioms/Conjectures 10/19/99 9:54AM
66:PA/an approach 10/21/99 8:02PM
67:Nested Min Recursion/Large Cardinals 10/25/99 8:00AM
68:Bad to Worse/Conjectures 10/28/99 10:00PM
69:Baby Real Analysis 11/1/99 6:59AM
70:Efficient Formulas and Schemes 11/1/99 1:46PM
71:Ackerman/Algebraic Geometry/1 12/10/99 1:52PM
72:New finite forms/large cardinals 12/12/99 6:11AM
73:Hilbert's program wide open? 12/20/99 8:28PM
74:Reverse arithmetic beginnings 12/22/99 8:33AM
75:Finite Reverse Mathematics 12/28/99 1:21PM
76: Finite set theories 12/28/99 1:28PM
77:Missing axiom/atonement 1/4/00 3:51PM
78:Qadratic Axioms/Literature Conjectures 1/7/00 11:51AM
79:Axioms for geometry 1/10/00 12:08PM
80.Boolean Relation Theory 3/10/00 9:41AM
81:Finite Distribution 3/13/00 1:44AM
82:Simplified Boolean Relation Theory 3/15/00 9:23AM
83:Tame Boolean Relation Theory 3/20/00 2:19AM
84:BRT/First Major Classification 3/27/00 4:04AM
85:General Framework/BRT 3/29/00 12:58AM
86:Invariant Subspace Problem/fA not= U 3/29/00 9:37AM
87:Programs in Naturalism 5/15/00 2:57AM
88:Boolean Relation Theory 6/8/00 10:40AM
89:Model Theoretic Interpretations of Set Theory 6/14/00 10:28AM
90:Two Universes 6/23/00 1:34PM
91:Counting Theorems 6/24/00 8:22PM
92:Thin Set Theorem 6/25/00 5:42AM
93:Orderings on Formulas 9/18/00 3:46AM
More information about the FOM
mailing list