[FOM] 820: Sugared ZFC Formalization/2

[Harvey Friedman]

PRINCIPLES
summarized from
[1] https://cs.nyu.edu/pipermail/fom/2018-June/021056.html

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.

2,3. THE BEST WAY TO PROCEED WITH ACTUAL
FORMALIZATION IS TO START OVER WITH THE FUNDAMENTAL PRINCIPLE THAT
ORDINARY MATHEMATICAL THINKING MUST RULE.

4. [MAKE INEVITABLE DEVIATIONS FROM MATHEMATICAL PRACTICE] 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.

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

*ROUGH INFORMAL DISCUSSION AIMING AT:
POLISHED INFORMAL DISCUSSION*

There has to be a lot of fits and starts rough informal discussion
concerning Sugared ZFC design, even before test driving with the
actual mathematics. That is what I want to start in this posting.

The outcome of this rough discussion of Sugared ZFC design is to
ultimately achieve some polished informal discussion which will allow
us to sensibly start delving into some actual mathematics, to see what
arises.

So what does this Elementary Set Theory text look like?

As you may recall from [1], we first aim for a text with

*axioms, definitions, conventions, propositions*

which is SEMANTICALLY VALID. We are going to call this a

VALID INFO TEXT

indicating that there are no proofs, and it is semantically valid. We
will know that it is semantically valid because we are going to use
our abilities as working mathematicians to "check" that.

After this is under great control, including fully reflecting normal
mathematical thinking, we take up proofs, with the aim of the "final"
product which is a

VALID PROOF TEXT

indicating that this is the full blown thing, with axioms,
definitions, conventions, propositions, and proofs - and it is both
semantically valid and the proofs have the appropriate "validity".

Our mathematical and computer scientific abilities will then see that
this Valid Proof Text is clearly machine verifiable by clear informal
algorithms.

After that, of course, there is the project of ACTUAL IMPLEMENTATION
of these informal algorithms. Under the current state of software
development, this Actual Implementation will demand RESOURCES, and I
am fully confident that if this comes out as attractive AS I WANT IT
TO BE (a tall order) then there will be no trouble getting RESOURCES
for it, at least by the year 2100. In that case, I don't mind smiling
from my grave.

We have to begin the rough discussion of Sugared ZFC with a discussion
of Sugared Logic. A lot of the sugar is of a logical nature, and not
specific to set theory. However, some of the sugared logic is best
focused on set theory. Why? Decades ago I did play around with a
Sugared Logic not focused on set theory, with generalized variable
binding operators, and the like, and IT JUST GOT TOO COMPLICATED TO BE
WORTH IT. I have no doubt that it is worth it in principle, but it
should be done as a separate big project.

Let's start with something easy. The logical connectives. Of course we
want the usual five connectives not, and, or, implies, iff, with their
good symbols. English is always a good idea as well. We want the well
studied precedence rules which even support chains like A implies B
implies C implies D. I like the idea of conjuncting in pairs when we
have a chain of implications and iff's: A implies B iff C implies D
means A implies B and B iff C and C implies D. You get the idea. Of
course, multiple disjunctions and multiple conjunctions don't need
parentheses, as is standard.

It would also be a nice touch to have a good symbol for "nor" as well
as English "nor".

Unique parsing supports the optional use of very few parentheses.
Parentheses for this context are ( ).

We now discuss quantifiers. Here we want the three quantifier symbols
"there exists", "for all", "there exists unique", the latter with its
famous !.

But to make quantifiers really useful by the appropriate standards,
there are a number of issues that need to be addressed. We want of
course

(there exists v)(phi)
(for all v)(phi)
(there exists unique v)(phi)

Here v is a variable. (We must discuss below what a variable is going
to be, as it must be something much more flexible than a mere letter).
But we need elaborations of these constructs. First of all, there are
the obvious multiple forms:

(there exists v_1,...,v_k)(phi)
(for all v_1,...,v_k)(phi)
(there exists unique v_1,...,v_k)(phi)

where k >= 1 and the v's are distinct "variables", whatever they are
(discussed in detail later).

But there is another important construct that makes for friendly reading:

(there exists v_1,...,v_k|phi)(psi)
(for all v_1,...,v_k|phi)(psi)
(there exists unique v_1,...,v_k|phi)(psi)

A strong case can be made for going much further than this, but
certain complexities arise as to free/bound variables that don't arise
here. I leave it open whether to go further, later.

Now there is one further thing that is somewhat special to set theory.
In it's most rudimentary form, it is

(there exists v epsilon t)(phi)
(for all v epsilon t)(phi)
(there exists unique v epsilon t)(phi)

where t is a "term", discussed at great length below. The v's can be
multiple (but distinct variables), and the t's can also be multiple.
Everything is interpreted here conjunctively. Also this can be put in
front of the |phi.

We won't go further with quantifiers at this point.

In the next posting in this series, we take up these syntactic categories:

variables
terms
atomic formulas
formulas

************************************************************************
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 820th 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  Jun 13 01:08:40
818: Beyond Perfectly Natural/17  6/13/18  4:16PM
819: Sugared ZFC Formalization/1  6/13/18  6:42PM

Harvey Friedman