[FOM] 654: Theory Inspired by Automated Proving 1

[Harvey Friedman]

I want to present some new or essentially new or at least undeveloped
subjects that come naturally out of stepping back and thinking
generally about automated theorem proving. I put the number '1' in the
subject header expecting to be able to start giving some initial toy
results.

I am going to take ZFC as the basic setup for these investigations. A
good alternative is to just use ZC, dropping Replacement. However,
there is some limited amount of very interesting mathematics, even at
the level of Borel measurable functions, that can be done in ZFC but
not in ZC. So that is a reason to use ZFC here instead of ZC. But
using ZC instead of ZFC is also perfectly reasonable.

Since I am talking about logical investigations inspired in some way
from contemplating automated theorem proving, this presentation does
not depend on accepting the use of ZFC or ZC as the core setup for
automated theorem proving. In fact, using set theory with its soft
typing is not at the moment very fashionable in most of the automated
theorem proving community.

However, many of you know that I am not shy of my deep skepticism
about elaborate and over complicated foundational setups.

Recently, I had some extensive discussions with John Harrison  at a
meeting, where I gave a talk:
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
An Approach to the Formal Representation of Mathematical Propositions,
February 3, 2016, Semantic Representation of mathematical Knowledge
Workshop, Fields Institute, Toronto, Canada, 14 pages.
DigialLibrary020716

John set up and extensively uses HOL Light with great success.
http://www.cl.cam.ac.uk/~jrh13/papers/hollight.pdf

In HOL Light there is very light typing, although the types are hard,
and not soft as in ZC. It is entirely clear that HOL Light can easily
be replaced - and I say improved - by simply using ZC. You just don't
gain much by using even the type structure in HOL Light. I will grant
that a case can be made that you DO GAIN SOMETHING with these types in
HOL Light if you are concerned with constructive mathematics issues.
But even here, it seems that ZC can be ready adapted for this purpose
as well, although there are some issues to be addressed.

Well, as I said, this posting is not really about automated theorem
proving. To get to the main points, we distinguish three realms.

REALM 1. Here we consider only axioms and definitions. No theorems, no
proofs. Already here there are a lot of challenging issues if one is
seriously aiming at beautiful readability and ease of writing. And
there is already some theory perhaps?? more challenging than any
perfectly precise and reasonably attractive mathematical theory that
has ever been precisely articulated. It would be interesting to see
what other theories can be precisely articulated.

REALM 2. Here we consider only axioms and definitions and theorems,
but not proof structure.

REALM 3. Here we consider axioms and definitions and theorems and
proof structure. Here I am not ready to articulate a precise
mathematical theory. I am hoping to be able to do this later.

1. PRIMITIVE FORMULAS AND COMPLEXITY

ZFC, in its raw form, uses these symbols:

not, and, or, implies, iff
forall, therexists
variables v1,v2,...
epsilon, equality
(   )

We need a complexity measure on formulas of ZFC. There are some basic
alternatives, with advantages and disadvantages, according to various
purposes.

a. Count the number of occurrences of variables.
b. Count the number of occurrences of quantifiers.
c. Compute the quantifier alternation complexity.

With a,b, we see that the number of formulas with a given count or
less, up to change of variables and logical equivalence, is finite.
Not so with c, which is defined by recursion on formulas in the well
known way, giving the Pin and SIGMAn classes of formulas, n >= 0.

2. QUANTITATIVE DEFINITIONAL THEORY

Let R be a k-ary relation on the set theoretic universe V. Compute or
estimate the least complexity of a primitive formula with at most the
free variables v1,...,vk, which defines R. Investigate this for
fundamental and familiar and simple R across mathematics. Use any of
the three complexity notions. This does not involve the axioms of ZFC.

3. QUANTITATIVE INSTANCE THEORY

Let phi be a theorem of ZFC. Compute or estimate the least complexity
of a set of formulas so that phi can be proved in ZFC where the two
axiom schemes of separation and replacement that are used are
restricted to that set of formulas. It is of course a bit less awkward
to use ZC instead of ZFC as there is only the separation scheme.

There are two obvious ways to measure the complexity of a finite set
of primitive formulas, all of which are relevant.

Investigate this for fundamental and familiar and simple phi across
mathematics.

i. The sum of the complexities of the elements.
ii. The max of the complexities of the elements.

**********************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 654th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM
622: Adventures in Formalization 6  9/29/15  3:33AM
623: Optimal Function Theory 2  9/22/15  12:02AM
624: Optimal Function Theory 3  9/22/15  11:18AM
625: Optimal Function Theory 4  9/23/15  10:16PM
626: Optimal Function Theory 5  9/2515  10:26PM
627: Optimal Function Theory 6  9/29/15  2:21AM
628: Optimal Function Theory 7  10/2/15  6:23PM
629: Boolean Algebra/Simplicity  10/3/15  9:41AM
630: Optimal Function Theory 8  10/3/15  6PM
631: Order Theoretic Optimization 1  10/1215  12:16AM
632: Rigorous Formalization of Mathematics 1  10/13/15  8:12PM
633: Constrained Function Theory 1  10/18/15 1AM
634: Fixed Point Minimization 1  10/20/15  11:47PM
635: Fixed Point Minimization 2  10/21/15  11:52PM
636: Fixed Point Minimization 3  10/22/15  5:49PM
637: Progress in Pi01 Incompleteness 1  10/25/15  8:45PM
638: Rigorous Formalization of Mathematics 2  10/25/15 10:47PM
639: Progress in Pi01 Incompleteness 2  10/27/15  10:38PM
640: Progress in Pi01 Incompleteness 3  10/30/15  2:30PM
641: Progress in Pi01 Incompleteness 4  10/31/15  8:12PM
642: Rigorous Formalization of Mathematics 3
643: Constrained Subsets of N, #1  11/3/15  11:57PM
644: Fixed Point Selectors 1  11/16/15  8:38AM
645: Fixed Point Minimizers #1  11/22/15  7:46PM
646: Philosophy of Incompleteness 1  Nov 24 17:19:46 EST 2015
647: General Incompleteness almost everywhere 1  11/30/15  6:52PM
648: Necessary Irrelevance 1  12/21/15  4:01AM
649: Necessary Irrelevance 2  12/21/15  8:53PM
650: Necessary Irrelevance 3  12/24/15  2:42AM
651: Pi01 Incompleteness Update  2/2/16  7:58AM
652: Pi01 Incompleteness Update/2  2/7/16  10:06PM
653: Pi01 Incompleteness/SRP,HUGE  2/8/16  3:20PM

Harvey Friedman