[FOM] 618: Adventures in Formalization 4

[Harvey Friedman]

REVERSE PROVER DESIGN

We begin our REVERSE PROVER DESIGN with the elementary number theory
environment. This will be based on a friendly version of PA for the
rationals, which we refer to as PA(Q).

In this exploratory study, we are at the outset committed to a few principles.

1. ABOVE ALL, beauty. All statements and proofs must be beautiful.
2. We will be using the HAVE/WANT calculus. This needs to of course be
formally defined - in due course - but illustrative examples have
already been given previously.
3. We will automatically assume that the Proof Assistant will
recognize ALL of the mathematically straightforward quantifier free
assertions that arise, that involve ONLY the PRIMITIVES of PA(Q). This
DOES include any use defined notions given by a quantifier free
definition. This DOES NOT INCLUDE user defined notions that are
defined using quantifiers. E.g., n|m is going to be user defined
rather early in the development, and it hides an existential
quantifier. This DOES NOT INCLUDE the non routine, such as a^3 + b^3 =
c^3 --> a = b = c = 0, or n^2 = 2m^2 --> n = m = 0. CLAIM: A very
strong phase transition exist here.
4. I HAVE INQUIRED SOME, and have found out that the state of the art
in computer packages for the quantifier free part of PA(Q) is NOT ALL
THAT WELL DEVELOPED at this point, and there are research projects
ongoing to make the packages stronger. I have not seen any details on
this, but I hope to be able to contribute something to these efforts.
I have the sense that this is a PERFECT PLACE to REVERSE. I.e., we are
going to see what DREAM PACKAGE should look like as we go.
5. We are aiming at the efficient creation of BEAUTIFUL FORMALLY
CORRECT, ELEMENTARY MATHEMATICS. We want to CREATE A GOLD STANDARD for
such items.

FREE LOGIC (SINGLE SORTED)

In free logic, we have undefined terms, =, and ~. s = t as usual means
that s,t are defined and identical. s ~ t means that either s = t or
s,t are both undefined.  With the latter, we mean that both sides are
either defined and equal (=), or both sides are undefined. We have the
downarrow for being defined, and the uparrow for being undefined. In
order for a term to be defined, all of its soubrettes must be defined.
The usual axioms and rules for classical logic are adjusted to reflect
that i) variables and constants are always defined, and ii)
instantiation of quantifiers must be be conditional on the term being
defined.

A term being defined is not a syntactic matter. However, we will want
to have facilities for dealing with compound terms being obviously
defined, just as mathematicians do. E.g., in an environment with the
field operations, we have undefined terms. However, we know that if we
avoid division, the terms are always defined. We need a way of dealing
with this formally. I haven't quite decided how I want to deal with
this.

I know that the Proving community handles this by having a lot of
typing, and default values. E.g., 1/0 = 0. I have NEVER met a
mathematician who is not disgusted with the idea that 1/0 might just
be 0. I am reasonably convinced that this seductive approach is bad,
and the badness exponentially proliferates. Of course, the burden of
proof is on ME.

There is an obvious completeness theorem for this free logic, or free FOL.

PA(Q)

This is meant to be the analog of PA for the rationals. A very nice
playground for the toys we are going to carefully analyze.

PRIMITIVE NOTIONS. <,<=,>,>=,not=. +,-,*,0,1,2,3,4,5,6,7,8,9,|
|,division. Being an integer. Floor,ceiling. Exponentiation,
factorial.

NOTE: We really want full base 2 and base 10 notation in this context.
This has been worked out well many times, although it does raise some
general purpose issues. I know nobody cares, but I do. So I will
revisit it later. But I include the ten digits just to support some
things I want to deal with like 2^(1/2). We will of course prove that
2^(1/2)uparrow. I.e., that 2^(1/2) is undefined.

L(PA(Q)) is the following language.

i. From logic, and, or, not, absurdity, implies, iff, therexists,
forall, =, not=, ~, uparrow, downarrow. Here x not= y is atomic, and
therefore means both sides are defined and not equal.
ii. Relations. <,<=,>,>=,not=,INT. INT means "being an integer". OK, I
confess, INT is NOT BEAUTIFUL. But we fill fix this of course by
supporting the use of "is an integer" in English.
iii. Constants. 0,1,2,3,4,5,6,7,8,9. There is the matter of supporting
say 10398.257. This has long been considered a solved problem. We
would like to handle this in a way that is part of a general theory of
BEAUTIFUL term constructions. But we have more urgent business to
attend to. I.e., strings-as-terms theory.
iv. Functions. +,-,*,/,^,!. The ! is quite useful to use as part of
the logic, right after an existential quantifier. So this is to be
distinguished from the factorial function, which is what I mean here.
Of course, unique parsing says that there is no problem. Also there is
the usual double meaning of -, as a unary function or a binary
function. There are also various well understood and well supported
conventions concerning the avoidance of parentheses, etc. We will
assume that all of this is done as usual, although again I would like
to revisit it as part of a general theory - and maybe that has also
been done properly. I am using * here for multiplication, as this is
plain text. Also I use / for division, also because this is plain
text. ^ for exponentiation, ! for factorial.

It is an essential point that we are going to have plenty of terms
that are provably not defined. E.g., 1/0uparrow is going to be a
theorem. 2^(1/2)uparrow is going to also be a theorem. Yes, the square
root sign is arguably more beautiful, and we can fix this in due
course.

PROPER AXIOMS.

1. Declaration. We let p,q,r,s,t range over everything, and
a,b,c,d,e,n,m range over integers (INT), unless otherwise specified.
WE NEED to support this kind of declaration. When this kind of
declaration is made, in order not to run out of variables, it is
understood that, e.g., p0,p1,p2,... are treated just like p.
2. Quantifier Free Axioms. Since we assume a software package for the
entire straightforward part of the qf fragment, we won't be too
detailed,
2.1. Ordered ring axioms. As usual.
2.2. Division axioms. "is defined" will normally use the uparrows.
p/q = r iff p = q*r and q not= 0.
p/q is defined iff q not= 0.
2.3. Integer axioms. Will present them informally.
0,1,a-b,a*b are integers if a,b are integers.
No integer strictly between 0,1.
Induction scheme for all formulas on integers >= 0.
(forall p)(therexists a,b)(p = a/b).
2.4. Exponentiation.
Suppose p,m not= 0. p^(n/m) = q iff p^n = q^m.
 0^p = 0 if p >= 0; undefined otherwise.
Suppose p not= 0. p^0 = 1 and p^(n+1) = p^n * p.
2.5. Factorial.
p! is defined if and only if INT(p) and p >= 0.
0! = 1.
n >= 0 implies (n+1)! = n! * (n+1).
2.6. Numerical.
2 = 1+1, 3 = 2+1, 4 = 3+1, 5 = 4+1, 6 = 5+1, 7 = 6+1, 8 = 7+1, 9 = 8+1.
Extension to full base 10 and base 2 notation.

The Package for the quantifier free part will undoubtedly contain
stuff about very elementary number theoretic basics, like p|q, gcd,
lcm, and the like. HOWEVER, we will not assume this, as we want to use
this material to examine slowly and carefully how to do REVERSE PROVER
DESIGN.

**********************************************************
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 618th 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  Sep 14 13:43:28 EDT 2015
615: Adventures in Formalization 2  Sep 14 13:44:13 EDT 2015
616: Adventures in Formalization 3  Sep 14 13:45:01 EDT 2015
617: Removing Connectives 1

Harvey Friedman