FOM: 70:Efficient Formulas and Schemes

Harvey Friedman friedman at
Mon Nov 1 13:46:44 EST 1999


We fix predicate calculus as the usual predicate calculus with equality and
countably infinitely many constant, relation, and function symbols, where
we use the connectives not, and, or, implies, the quantifiers forall,
therexists, and infinitely many variables. There are infinitely many
relation and function symbols of any arities >= 1.

We count the number of symbols by counting the total number of occurrences
of the following:

i) connectives;
ii) constant, relation, function symbols;
iii) variables;
iv) forall, therexists;
v) =.

As in postings #65, #66, and #68, (forall x) and (therexists x) each get
counted as two symbols. Note that parentheses and commas are not counted.

A single formula phi is said to be efficient if and only if there is no
formula psi with fewer symbols such that {phi} and {psi} are logically
equivalent. The latter is the same as saying that the universal closures of
phi and of psi are logically equivalent.

We introduce two notions of efficiency for finite sets of formulas.

A finite set of formulas S is said to be alpha efficient if and only if
there is no finite set of formulas T such that

i) S and T are logically equivalent;
ii) some element of S has more symbols than every element of T.

A finite set of formulas S is said to be beta efficient if and only if
there is no finite set of formulas T such that

i) S and T are logically equivalent;
ii) the total number of symbols of elements of S is greater than the total
number of symbols of elements of T.

GENERAL PROBLEM. Investigate efficiency, alpha efficiency, and beta
efficiency in predicate calculus. Take standard theories in predicate
calculus and give alpha and beta efficient axiomatizations.

There should be some general theory; e.g., in connection with sufficient
and necessary conditions for efficiency, relationships between the three
notions of efficiency, and the relationship between the efficiency of a
formula and that of its negation, etcetera.

More specifically, start with giving efficient axiomatizations of the
following famous theories in the binary relation symbol R:

1. R holds everywhere.
2. R holds somewhere.
3. R is reflexive.
4. R is irreflexive.
5. R is symmetric.
6. R is antisymmetric.
7. R is transitive.
8. R is a strict ordering.
9. R is a quasi ordering.
10. R is a partial ordering.
11. R is a linear ordering.
12. R is an equivalence relation.
13. R is a dense linear ordering.
14. R is a linear ordering with a right endpoint (or no right endpoint).
15. R is a linear ordering with endpoints (or without endpoints).
16. The negation of any of the above.

One can even start with more elementary things such as:

17. There are at least two objects.
18. There are at least three objects.
19. There is exactly one object.
20. There are exactly two objects.
21. There are exactly three objects.
22. There are at most two objects.
23. There are at most three objects.

Also, one can consider algebraic theories in one binary operation symbol F,
with/without unit:

24. F is commutative.
25. F is associative.
26. F is commutative and associative.
27. F is a group.

And, with two binary operation symbols +,*, with/without unit:

28. They form a ring (with or without unit).
29. They form a commutative ring. (with or without unit).
30. They form a field.

In posting #65, I gave a treatment of schemes using schematic letters, and
the appropriate notion of substitution, which handled free/bound variables
and clashes appropriately.

The above setup is straightforwardly carried over to single schemes, and
also finite sets of schemes.

In addition, it is also carried over straightforwardly to many sorted
predicate calculus.


a. The results don't change much under minor changes in the way symbols are
b. A reasonably complete understanding of the above requires substantive
interaction between computer algorithms and various kinds of combinatorics.
This will result in new combinatorics and computer science of independent
interest; especially in the area of efficient heuristics.
c. The natural problems range from trivial to completely out of range.
d. People will hesitate before accepting this way of counting symbols, but
will then plow in to an intensive investigation for the forseeable future.
e. There will be striking relationships between people's intuition when
they write "nice" axioms down in predicate calculus and their efficiency in
these formal senses.
f. Unexpected insights will eventually emerge into the nature of


PROBLEM. Give efficient, alpha efficient, and beta efficient
axiomatizations of PA. Do this also for the standard fragments of PA.


PROBLEM: Give efficient, alpha efficient, and beta efficient
axiomatizations of Z_2, which is the two sorted axiomatization of second
order arithmetic with natural numbers and sets of natural numbers, using
=,S,+,*,0 on integers only, and epsilon between integer terms and set
variables. Optionallly, = between sets should be present, with


PROBLEM: Give efficient, alpha efficient, and beta efficient
axiomatizations of ZFC and its standard fragments such as ZF, Z, ZC.


Way into the future, also give efficient axiomatizations of ZFC with large


This is the 70th 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
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

More information about the FOM mailing list