[FOM] 621: Adventures in Formalization 5

[Harvey Friedman]

CORRECTION TO http://www.cs.nyu.edu/pipermail/fom/2015-September/019142.html

I left out floor and ceiling in the axioms of PA(Q). Now I put them in.

PA(Q)

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

i. From logic, and, or, not, absurdity, implies, iff, therexists,
forall, =, not=, ~, uparrow, downarrow.
ii. Relations. <,<=,>,>=,not=,INT. INT means "being an integer".
iii. Constants. 0,1,2,3,4,5,6,7,8,9.
iv. Functions. +,-,*,/,^,!, floor, ceiling. Here * is multiplication,
/ division, ^ exponentiation, ! factorial.

PROPER AXIOMS.

1. Declaration. We let p,q,r,s,t,x,y,z,w,u,v range over everything, and
a,b,c,d,e,n,m  range over integers (unary predicate Z for being an
integer), unless otherwise specified.
2. Quantifier Free Axioms.
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.
floor(x), ceiling(x) are integers.
x-1 < floor(x) <= x, x <= ceiling(x) < x+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.

###############################

I am hoping to directly answer all of those interesting FOM postings
by the experts in Provers, shortly. In the meantime, I want to
continue where I left off using PA(Q).

I want to REINVENT WHEELS using PA(Q). I am expecting that the wheels
I reinvent will have enough new that I can leverage things when I go
to full blown setups, and really maybe stir the pot in an interesting
way. So let's see how far I get.

I understand from Dana that Isabelle, roughly speaking, has a kind of
umbrella that accommodates various particular ways of formalizing
mathematics. That's great if it turns out that Isabelle can be used,
or other tools, to greatly facilitate an implementation of the kind of
approach I want to take here. But it still remains to develop some
particularly clear/beautiful/novel approach first.

With regard to certainty, I am interested in pushing the certainty as
far as it can go, whatever that means. I believe that it can go
farther than anything I have heard about, that probably not many
people care about going much further, and that there is an unknown
limit as to how far certainty can really be pushed. I would love to
see, or have a hand in developing, a theory of just how hard certainty
can be pushed. Under a suitable theory, I think, there may emerge a
very robust notion of "as certain as possible", and then people will
call that something like "essential certainty", or whatever. And then
that will be the gold standard for certainty, something for people to
aim for. E.g., just how tiny can a kernel be? Just how transparent can
a kernel be? Exactly what is a kernel? etcetera. I have even heard
stories about how small kernels were wrong!! What do you do about that
without a Kernel Theory? Maybe there is one tiny indivisible UNIVERSAL
KERNEL, (provably) not capable of simplification, and then everybody
just starts with that universal kernel to justify their certainty??

I know that 1/0 = 0 is very common, going back to the need for
Herbrand universes, and various infrastructures that were built long
ago and kept going with the idea that all terms should denote. Free
logic was apparently not much embraced when people built these
infrastructures. This, together with the typing idea - that there
should be a plethora of types all over the place, and dependent types,
etc, to guarantee that all terms denote. Then if one wants, 1/0 can be
illegal because 0 is not in the appropriate type.

I admit to hating types in the formalization of mathematics, but I
have been told that I am wrong, as type checking and the like is the
bread and butter of Proving, and without it, we are supposed to be
lost. This makes me think I may be right. But of course, in my
naivety, I might be forced to buckle under and support rampant typing.

Well, there is some sort of very weak kinds of typing in ordinary
mathematical proofs, but I don't think its the kind of intense stuff
that the Provers tend to enforce. PA(Q) has no typing to speak of. I
don't consider the predicate "being an integer" really that big a
plunge into typedom. Of course, if you put a serious lid on typing,
you run quickly into things like rampant 1/0, and then you really do
need Free Logic to keeps things beautiful - and faithful to ordinary
mathematical thinking and writing.

So I want Free Logic and essentially no typing. PA(Q) is too
elementary for infinite sets, and so for PA(Q), I will not use x
epsilon Z. So I will use Z(x) for "x is an integer", and also special
variables for integers. We know full well that there is already out
there some support for actually using the phrase "x is an integer"
spelled out in English. So that is ultimately what I have in mind when
I write Z(x) here on the FOM. Of course, this kind of thing is icing
on the cake, and we don't have to worry about it. Much more
fundamental, and controversial, is the free (pun) use of Free Logic.

QUANTIFIER FREE PACKAGES

As I said earlier, qf is the drudgery part of Proving, as far as I am
concerned, and nasty problems come from not having a powerful qf
package. I wholly subscribe to the idea that we build bigger and
better packages all the time, not just surrounding mainly the qf stuff
in PA(Q), the immediate need, but also everywhere.The QFPA(Q) package
development is orthogonal to the Fun Prover stuff.

Originally, I planned a pretty standard kind of QFPA(Q) surrounding
just the primitives of PA(Q). However, I have come to think that their
has to be something more general purpose here.

WE ALSO need The General Purpose QF, GPQF.

GPQF supports purely quantifier free reasoning of the kind that is
really relevant and useful for REAL WORLD mathematical theorem
proving. But GPQF does not take into account special mathematical
facts and ideas. E.g., GPQF does not know that addition is
commutative. However, you can feed it the commutativity of addition,
and it will act on it.

How is the GPQF = general purpose quantifier free package ACtUALLY
USED by Provers?

The GPQF simply digests the whole of what is going on, blackballing
all quantifiers. Anything that starts with a quantifier must be viewed
as atomic.

When the user creates a convention that certain variables range over
entities with certain quantifier free properties, this is digested by
the GPQF. Or when the user defines a new atomic formula by a
quantifier free definition, that is digested by GPQF.

The user can control what the GPQF is going to be allowed to use to
generate anything new. This way, it tries to prevent GPQF from wasting
its time looking at irrelevancies. This shows up in the Beautiful Text
as something like; we easily see that blah blah blah, using this and
this and that.

Then there is the separate Special Purpose QF packages that are the
linked to the GPQF seamlessly.

More specifically, the GPQF has these features:

a. The user can create new atomic formulas at any time. They can
either be introduced in a quantifier free fashion, or they can be
introduced using quantifiers.
b. The GPQF absorbs tsuch new qf stuff
c. GPQF only pays attention TO THE QUANTIFIER FREE PART of what the
user is doing with the Prover. We ban GPQF from taking into account
any quantifiers whatsoever.
d. The user controls what GPQF is considering, making changes at any
time. This may well save a lot of computational space. So that is a
little part of the HINT system.
e. The default is for GFQF is of course to use everything that has
been thrown at it, that is qf. But looking at any quantifiers is
strictly forbidden, under penalty of death.

So the design and implementation of the qf part of the PA(Q) Prover
has two somewhat orthogonal challenges.

i. A logic challenge. What should general purpose quantifier free
reasoning really look like, to support REAL WORLD PROVERS of the kind
I am talking about? I.e., GPQF?
ii. A mathematical challenge. How do we exploit the most fundamental
of mathematical notions leveraging what we have seen to be important
and useful over the centuries in actual quantifier free mathematics?
Specifically, of course, for PA(Q), we need to intensively address its
primitives.  I.e., the SPQF's? special purpose qf packages.

With regard to i, we are really talking about intelligent term
substitutions, sensitive to the goaling structures inherent in the
propositional structure and the Free Logic primitives of uparrow,
downarrow, =, ~. Remember, this is suppose to support the brainless qf
drudgery in actual mathematical proofs.

With regard to ii,  am now going to take a stab at the kind of things
that we really want to crush in the SPQF for PA(Q) = QFPA(Q).

1. Start easy. Look at all quantifier free formulas satisfying the
following conditions.
a. The total number of variables is at most 4.
b. Every term has at most two uses of multiplication and division
combined, and no exponentiation and no factorial. It can use any
constants, +,-,floor,ceiling.
The qf formula itself uses the connectives,
=,~,uparrow,downarrow,<,<=,>,>=,=,not=,Z.
2. Gradually go bigger than 1. How much and in what way depends on
what is involved in getting a good crushing software for 1.

ABOVE ALL, I want the user to have a good conceptual handle on just
what GPQF is doing, and what QFPA(Q) is doing. Only then will the user
have a good handle on what HINTS they have to give to successfully
drive the Prover in the fun and sometimes creative parts. REMEMBER:
The Prover will be linking the QFPA(Q) seamlessly with the GPQF.

**********************************************************
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 621st 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

Harvey Friedman