[FOM] 820: Sugared ZFC Formalization/2

[Lawrence Paulson]

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.

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.

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.

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.

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."

Larry Paulson



> On 19 Jun 2018, at 00:52, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> I respectfully have a different take on this, and the example you gave
> of 1/0 = 10 and 1/0 not= 1/0 and not 1/0 = 1/0 being meaningless is a
> perfect example for my approach.
> 
> I know how to convince mathematicians of the proper attitude towards this.
> 
> An atomic statement is automatically false if any sub term is
> undefined. So 1/0 = 1/0 is meaningful and false, 1/0 not= 1/0 is
> meaningful and false, and also not 1/0 = 1/0 is meaningful is true. I
> will argue until the cows come home with them, and I claim that I have
> done this sort of thing on occasion with some success - although if
> you are interested, I will try to document this with them.
> 
> And I will convince them that this is fully consistent with any
> intelligible mathematical thinking, if that thinking is meant to be
> fully rigorous.
> 
> Of course, I am trying to do this sort of thing with everything needed
> in Sugared ZFC, and that is of course a tall order (especially for
> this short person) (smile).
> 
> Harvey Friedman
> 
> On Mon, Jun 18, 2018 at 11:42 AM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>> There is a tension between logical formality and ordinary mathematical thinking. And because formality cannot be compromised (for then it would cease to be formal), ordinary mathematical thinking will need to give way. For example, ordinary mathematical thinking surely rejects both 1/0 = 1/0 and 1/0 ≠ 1/0 as meaningless. Most formal proof assistants will make the first one true and the second one false, though with free logic I believe it to be the other way around. There are other approaches to this particular difficulty, but doubt whether any of them are fully consistent with ordinary mathematical thinking. It is a vague concept so we can never be sure. We would be better off accepting a formal system whose workings can be understood with the help of ordinary mathematical thinking even when they are not strictly orthodox.
>> 
>> Larry Paulson
>> 
>> 
>> 
>>> On 14 Jun 2018, at 23:45, Harvey Friedman <hmflogic at gmail.com> wrote:
>>> 
>>> 2,3. THE BEST WAY TO PROCEED WITH ACTUAL
>>> FORMALIZATION IS TO START OVER WITH THE FUNDAMENTAL PRINCIPLE THAT
>>> ORDINARY MATHEMATICAL THINKING MUST RULE.
>> 
>> _______________________________________________
>> FOM mailing list
>> FOM at cs.nyu.edu
>> https://cs.nyu.edu/mailman/listinfo/fom