[FOM] 820: Sugared ZFC Formalization/2

[Harvey Friedman]

On Wed, Jun 20, 2018 at 10:18 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
> I apparently wasn't very clear, because I wasn't claiming that 1/0 is the one issue that dooms the approach, but rather the most obvious such issue, if one insists on formalising "ordinary mathematical thinking". Formalising mathematics is difficult enough without trying to duplicate "ordinary mathematical thinking".
>
> I'm aware of many of the approaches to the problem of definedness, all of which involve some compromise, such as complicated formal systems, longer proofs, quirky properties. But even if this issue is fully addressed, there is the next one and the one after that, et cetera.

I remain idealistic, but with a footnote. The example of 1/0 and free
logic is being used by you as a signal of something a little bit bad
with much worse to come. I am looking at the semantics of free logic
as something completely great and convincing (not due to me, of
course), something that a strong majority of mathematicians with the
slightest interest in formalization find or would find very
attractive, very clarifying, and very welcome - and a signal that the
situation is much better than people realize. The room for creative
ideas I believe is very significant.

FOOTNOTE. Recall that I am much more interested in discovering
revelations about the nature of mathematical thought through
formalization research, than I am in the quantity and depth of what
gets formalized. I don't think that you share my obsession. THEREFORE,
even cutting through such difficulties even in comparatively
elementary mathematics like undergrad set theory, can be enough for MY
main purposes - obviously not enough for YOUR main purposes.

> Another is the huge ambiguity found in mathematical notation and mathematical texts. The link below is to a proof I happen to be looking at just now:
>
> https://www.dropbox.com/s/v4mgvh2td2fmy9x/Bak-Newman-CA.pdf?dl=0
>
> (From Complex Analysis by Bak and Newman.) It's completely ordinary material and yet there's nothing resembling a formal proof here. Mathematical notation in its full glory will require disambiguation and I don't think the result will ever be beautiful.

I want to create my own PERFECT exposition of say undergrad set
theory. I am less concerned with published, horribly imperfect by
these standards, expositions. OF COURSE, I recognize that the goal

GETTING PROOF ASSISTANTS TO BE USABLE AND USED BY THE GENERAL
MATHEMATICS COMMUNITY

is much harder than me creating PERFECT EXPOSITIONS of undergrad math.

But in general, I believe that if I succeed with creating some perfect
expositions of undergrad math, we will have learned a lot about the
harder problems that you are focused on. ALSO, I think that my way of
dealing with formalization is MORE LIKELY to lead to revelations about
the nature of mathematical thought. WE WILL also see how receptive the
math community is to certain powerful formalization devices.

> A third problem might be our tendency to sweep aside foundational issues. So when we say "every finite group of odd order is solvable", this includes a group given by three measurable cardinals, which possibly isn't what we want. One could say that quantification over groups always means "up to isomorphism", but what that should mean it isn't clear for "every finite group is a subset of the natural numbers", and anyway, isomorphism classes are proper classes, so the foundational issues just take another form. And let's not mention category theory.

Groups really are (X,+,-), X can be any nonempty set. The isomorphism
relation is defined and is important. Every finite group is isomorphic
to a group with domain included in N. The fact that isomorphism
classes are proper classes doesn't drive me into using proper classes,
as that causes more problems than it solves. I am happy to form the
set of all groups whose domain is a subset of X.

> What I am trying to say is that once you adopt a formal system, you will be working with code. It may be a fairly decent form of code, and people have already done remarkable things using a variety of proof assistants. It is possible to transform ordinary mathematical thinking into this sort of code. But then you will be working at the level of code.

But I am hoping for totally readable totally friendly mathematics that
is obviously formally checkable. At first, just obviously semantically
valid.
>
> Maybe it's appropriate to quote Heyting: "The intuitionistic mathematician... uses language, both natural and formalised, only for communicating thoughts, i.e., to get others or himself to follow his own mathematical ideas. Such a linguistic accompaniment is not a representation of mathematics; still less is it mathematics itself."

You might consider elaborating on this specifically in the context of
our discussion.

Harvey