[FOM] 820: Sugared ZFC Formalization/2

[Harvey Friedman]

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