[FOM] 186:Grand Unification I

Harvey Friedman friedman at math.ohio-state.edu
Wed Jul 2 10:39:24 EDT 2003

NOTE: My FOM activity will necessarily be slowed down for the Summer 
to make time for some formal writing.

NOTE: The Grand Unification discussed here transcends the focused 
goals of interactive proof checking discussed in the last few 
numbered postings.


As stated earlier, in the plan I envisage for proof checking, the 
context strongly encourages the user to adopt LEMMA ENRICHMENT, which 
is intended to have the effect that the complexity of any proof is 
sharply minimized. Nontrivial proof ideas normally generate the 
friendly construction of additional enriching Lemmas.

Nevertheless, the user/computer interaction required even under LEMMA 
ENRICHMENT will from time to time get involved, and hence the need 
for a detailed powerful design of this interaction. We have been 
discussing this, together with supporting user interface ideas, in 
several postings on "Ideas in Proof Checking 1-4", at least for some 
simplified warmup languages.

{In the background, I have been talking to users of Isabelle, a 
highly developed interactive proof checker, to see what difficulties 
users run into, and what Isabelle does about them. At some point, it 
would be particularly valuable if a user of Isabelle, or related 
system, could talk about their experiences.}

I have been aware for quite some time of an important component in 
handling trivialities. This is the use of PACKAGES.

The idea here is that powerful special purpose theorem provers are to 
be created that handle trivialities well, in selected contexts that 

The creation of these powerful special purpose PACKAGES forms an open 
ended project lending itself to deep THEORETICAL work, tempered with 
practical considerations.

Examples of the most OBVIOUS kind of packages would be
i) packages for Presburger arithmetic;
ii) packages for real closed fields;
iii) packages for algebraically closed fields;
iv) packages for special purpose methods in predicate calculus, such 
as resolution;
v) computer algebra systems.

The problem with v) is that there is no appropriately rigorous 
support. An expression may be simplified, but under what exact 
conditions is the simplification valid?

Items i)  - iii) represent infinite recursive sets. There are 
theoretical results that show that no efficient algorithms exist, 
asymptotically. However, there may well be algorithms that perform 
generally well on the SMALL instances that normally come up.

Item iv) is quite different - at least on the face of it - than i) - 
iii) because one is not looking at a sentence, but rather valid 
forms. However, right after the capital letter statement enclosed in 
#'s below, you will see that in our context, there is way of unifying 
these two, so that they are NOT different.

Valid forms and outright sentences of mathematics are to be combined 
into a single package. One should NOT do this with any heavy handed, 
less than mathematically familiar/friendly, use of higher order 
logic. Everything is to stay naturally in mathematically 
familiar/friendly contexts with a set theoretic foundation underlying 

We are now coming to the critical proper ATTITUDE to PACKAGES that I 
am promoting. That is,

a) there is NO reason to consider any infinite class of statements to 
be analyzed;
b) issues of decidability, in the usual sense of the word, are 
completely irrelevant;
c) one should concentrate on SMALL problem instances.

What does it mean to say that a large finite collection of small 
problems is DECIDABLE? Under the usual definition, it always is 
decidable. Instead, it means that there is a small efficient 
algorithm that correctly handles them.

In pondering this, and other ideas I have had about PARADIGM SHIFTS 
for mathematical logic, I see a GRAND UNIFICATION.


I see a grand unifying theme which merges all of the following into 
one giant enterprise.

1. The idea in model theory that one should study structures which 
are WELL BEHAVED, or TAME, rather than ones which exhibit hopeless 
PATHOLOGY, about which very little can be said that relates to 
anything else. The paradigm cases pushed here are where there is QE = 
QUANTIFIER ELIMINATION, which "tame" certain important mathematical 
structures, showing either outright decidability, or decidability 
relative to conjectures, or at least where the definable relations 
are very manageable. The specific paradigm cases include the ordered 
ring of integers (Presburger arithmetic), the field of real numbers 
(real closed fields), the field of complex numbers (algebraically 
closed fields), the p-adics, the field of real numbers with 
exponentiation, and some others.

2. Decision procedures generally, including computational aspects, 
implementational issues, and resource bounds, etc.

3. Proof theoretic formalisms, especially for equational reasoning, 
and quantifier reasoning.

4. Set theoretic reasoning of various kinds, including the possible 
use of large cardinals for concrete statements.

5. Potentially every relatively clean, uncluttered situation in the 
whole of mathematics.

So what is this project?


I am interpreting "assertion" rather broadly here. It might be 
presented in implicational form:

Let A1,...,An. Then B.

Normally, there are free variables used in A1,...,An,B. These are, of 
course, interpreted universally.

But suppose A1,...,An,B are thought of as formulas in predicate 
calculus? I just handle the relation symbols and functions in a 
friendly way as free variables, also. If R is a ternary relation 
symbol, then

R is a ternary relation

is going to be among the A's, with R a free variable - interpreted 
universally within the underlying set theory.

Some further remarks.

a. The scope of applicability of the algorithms should remain 
flexible. If one knows that one has handled all short assertions of a 
certain kind, that should not stop one from expanding the class of 
short assertions with short assertions of a more inclusive kind 
(e.g., less short, or more primitives). Also, if one cannot yet 
handle all short assertions of a certain kind, one can still use what 
one has in the interactive proof checker. Or it may sometimes blow 
up, and one can still use it, as it may not blow up in practice. Or 
one may wish to strengthen the implementation.

b. The model theorists ALSO look to identify mathematically relevant 
families of assertions in various fundamental mathematical situations 
and develop tools to analyze them - especially quantifier 
elimination, and the analysis of definability (in the context). E.g., 
various kinds of minimality, including o-minimality. Decidability is 
usually, but not always, a byproduct.

c. However, the model theorists are looking for CLEAN generality, and 
will not investigate WILD classes of statements, where for classic 
GODELIAN reasons, things are very badly undecidable, and also where 
the definable sets are very pathological.

d. Note that b and c PREVENT model theorists from looking at hardly 
ANYTHING! They can only look at some tiny tiny tiny number of 
contexts with this ATTITUDE - compared to the number of INTERESTING 

e. The key aspect of this paradigm shift for model theorists - and 
for ALL mathematical logicians for that matter - is to WELCOME THE 
BRAINS (as long as it is mathematically natural), for the following 

f. EVERYTHING, no matter how logically horrible, is TAME for a while, 
before it turns UGLY. Intensively investigate from the BOTTOM UP. You 
might get SURPRISINGLY far.

g. But WHY? Lots of interesting tameness uncovered, etc. But there is 
an additional major FOUNDATIONAL reason. My OLD additional 
foundational reason was already sufficiently DRAMATIC. But see the 
additionally DRAMATIC and UNIFYING reason m below.

h. I CONJECTURED that WHENEVER you climbed up the ladder in a 
logically horrible context, you would get to a BOUNDARY, where things 
start to get dicey, BEFORE they plunge into UTTER GODELIAN CHAOS. And 
what is the nature of this BOUNDARY? It is conjectured to be LARGE 

i. The principal example of this was in BOOLEAN RELATION THEORY. See

Harvey Friedman, Equational Boolean Relation Theory, 

A very short statement in equational BRT involving two functions and 
three sets, is tied up with Mahlo Cardinals.

j. So I proposed a GRAND development of BRT. Look at various of the 
trillions of totally natural BRT contexts (families of multivariate 
functions and associated sets), and CLIMB THE LADDER, until maybe you 
reach LARGE CARDINALS - as I did in the context discussed in that 
reference above.

k. Then I proposed an even GRANDER vision. BRT is just one aspect of 
setting up little languages surrounding mathematical contexts and 
theorems. There one varies the parameter BOOLEAN RELATION.

l. So generally, we identify little languages associated with 
mathematical theorems, based on a PARAMETER to vary. And then look at 
what statements you get when you do the VARIATION OF INTELLECTUAL 
PARAMETERS. The conjecture is that

1) virtually everywhere you do VARIATION OF INTELLECTUAL PARAMETERS, 
it is very productive and very much connected naturally with lots of 
existing mathematics;

2) frequently, you climb the ladder, and then get into a region where 

m. Coming back to DRAMA and UNIFICATION and g above. We now have an 
ADDITIONAL reason for this study.



for the purposes of developing PACAKAGES for INTERACTIVE PROOF CHECKING,


into one GRAND UNIFYING subject!!!!!

The next numbered posting #187 discusses some powerful reasons to 
have this GRAND UNIFICATION in place, because of its role in another 
venture whose great importance is obvious to virtually anyone 


I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 186th 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-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM
182:Ideas in Proof Checking 1  6/21/03 10:50PM
183:Ideas in Proof Checking 2  6/22/03  5:48PM
184:Ideas in Proof Checking 3  6/23/03  5:58PM
185:Ideas in Proof Checking 4  6/25/03  3:25AM

Harvey Friedman

More information about the FOM mailing list