[FOM] 819: Sugared ZFC Formalization/1

Wed Jun 13 18:42:17 EDT 2018

Decades ago, I spent some effort designing a Sugared ZFC for friendly
formalization of mathematics, including the design of some specific
practical projects.

I didn't receive any encouragement from people in Theorem Proving, and
in some cases was assured that nobody would pay any attention to such
things unless one actually had a prototype running.

So I moved on to other things, but remained uncomfortable with this
conventional wisdom of: no implementation implies worthless, and also
the conventional wisdom of heaving typing. These two pieces of CW are
totally incompatible with anything like my approach.

Recent FOM postings concerning Theorem Proving now convince me that I
probably made a serious error in listening to CW decades ago.

I am thinking about Formalization some, again, and this time I am
going to be much more bull headed.

PRINCIPLES

1. My primary aim for the development of real, genuine, actual,
practical, readable Formalization (of mathematics) is TO GENERATE
MAJOR FINDINGS CONCERNING THE NATURE OF MATHEMATICAL DEFINITIONS,
MATHEMATICAL PROPOSITIONS, AND MATHEMATICAL PROOFS. A secondary
objective is to support the production of formalized proofs. Present
Formalization has been impressive concerning this secondary aim (with
a long way to go in many respects), but particularly unimpressive
concerning this primary aim. One reason for this may be that the tools
created have a lot of not well controlled (intellectually)
combinations of procedures, experimentally tweaked for optimization,
with the generally forced abandonment of theoretically well understood
principles powerful enough to be really relevant. In this kind of
situation, accompanying theory is very hard to initiate - WITHOUT
ESSENTIALLY COMPLEtELY STARTING OVER with the full intention of
developing theory.

2. ORDINARY MATHEMATICAL THINKING MUST RULE. I can imagine a time
where maybe this becomes a silly old fashioned idea sort of like what
we have seen with Chess and Go - trying to imitate humans is
incomparably less powerful than letting computers loose with Deep
Learning. However, we are not nearly at that point, if we ever get
there. I made an FOM posting some time ago asking for the prospects of
Deep Learning coming up with a formal proof of no p^2 = 2 from the
mere relevant formal system. Subsequently, there have been some recent
FOM postings addressing this kind of issue.

3. Until such time as there is a Deep Learning type revolution,
whereby machines become effective general purpose mathematicians, I am
going with the working idea that THE BEST WAY TO PROCEED WITH ACTUAL
FORMALIZATION IS TO START OVER WITH THE FUNDAMENTAL PRINCIPLE THAT
ORDINARY MATHEMATICAL THINKING MUST RULE.

4. Now having said this, we all know that almost all mathematicians
are at the very best  - let me put it very gently - amateur logicians.
A slavish adherence to 2) is going to lead to disaster. When we run
into problems - most commonly unclear semantics - with something
mathematicians are actually doing, like the absolutely horrendous
notation from Calculus, we adjust it IN SUCH A WAY THAT WE ARE
CONFIDENT THAT THE MATHEMATICIANS CAN BE CONVINCED THAT WE ARE MAKING
THE RIGHT DECISION WITH THEIR INPUT AND INTERESTS FULLY TAKEN INTO
ACCOUNT.

5. For example, I am convinced that I could get the math community
(with a passing interest in Formalization) to be entirely happy with a
proper alternative to the disgusting logical atrocity that is Calculus
notation. THEY WOULD BE HAPPY for the purpose of FORMALIZATION,
understand why it is SUPERIOR for that purpose, but OF COURSE would
never dream of adopting it in their own papers. At least not until
Formalization really gets to an advanced practical stage.

PLAN OF ACTION
DELIVERABLES

1. A sketch of some principal features of Sugared ZFC, along with
crystal clear semantics. All of this is done at a semiformal level
typical of a mathematical paper. The full expectation is that many
more features will be added, that things may get seriously modified,
as we dig deeply into the actual mathematics

1. Start with an undergraduate math area. First undergraduate set
theory. Second undergraduate combinatorics. Third undergraduate number
theory. That's enough for a while.

2. Write a text covering the main material, with Definitions and
Statements only. Postpone proof issues. Adjust and refine Sugared ZFC
in order to make this very readable and completely rigorous. By
completely rigorous, I mean that all of the propositions follow
logically from the axioms and rules, at this point purely as a matter
of ORDINARY MATHEMATICAL THINKING, and without FORMAL PROOFS, at this
first stage.

3. Already, even at this point, come up with some interesting theory
and interesting findings and interesting questions about what is
happening.

4. After this is very much in control in the first undergrad subject,
set theory, we venture into proofs. The MAIN IDEA HERE, is to, after
serious experimentation, come up with a fairly robust notion of
OBVIOUS, and OBVIOUS VIA HINTS, that can be used uniformly throughout
a full treatment with proofs, so that what is left is totally
readable, and reads like an ordinary undergrad math text. Hints are to
become a certain kind of formal object. This challenge is drenched
with various prospective theory. We dig in deep to investigate robust
forms of OBVIOUSNESS. But NOT with the conventional aim of making
machines take greater leaps. RATHER, understanding just what it is
that makes US see something as obvious, and just what it takes in the
form of HINTS that makes the not quite obvious, obvious.

5. After serious experimentation and theory converging on at least one
really robust notion of OBVIOUS, we now write the text. We write it in
such a way that it is CLEARLY FORMALLY VERIFIED by SKETCHED
ALGORITHMS. Yet totally readable, with plenty of English like: Let A,B
be blahs, where f(A,B) is constant.

************************************************************************
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 819th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

800: Beyond Perfectly Natural/6  4/3/18  8:37PM
801: Big Foundational Issues/1  4/4/18  12:15AM
802: Systematic f.o.m./1  4/4/18  1:06AM
803: Perfectly Natural/7  4/11/18  1:02AM
804: Beyond Perfectly Natural/8  4/12/18  11:23PM
805: Beyond Perfectly Natural/9  4/20/18  10:47PM
806: Beyond Perfectly Natural/10  4/22/18  9:06PM
807: Beyond Perfectly Natural/11  4/29/18  9:19PM
808: Big Foundational Issues/2  5/1/18  12:24AM
809: Goedel's Second Reworked/1  5/20/18  3:47PM
810: Goedel's Second Reworked/2  5/23/18  10:59AM
811: Big Foundational Issues/3  5/23/18  10:06PM
812: Goedel's Second Reworked/3  5/24/18  9:57AM
813: Beyond Perfectly Natural/12  05/29/18  6:22AM
814: Beyond Perfectly Natural/13  6/3/18  2:05PM
815: Beyond Perfectly Natural/14  6/5/18  9:41PM
816: Beyond Perfectly Natural/15  6/8/18  1:20AM
817: Beyond Perfectly Natural/16
818: Beyond Perfectly Natural/17

Harvey Friedman