[FOM] 820: Sugared ZFC Formalization/2

[Bill Greenberg]

Re: Division by Zero

What might FOM'ers reaction be to Rolf Schock's "Division by Zero" (
virthost.vub.ac.be/lnaweb/ojs//index.php/LogiqueEtAnalyse/article/view/957/792).
Or to NaN's in Python?

William J. Greenberg

On Mon, Jun 18, 2018 at 4:52 PM, 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180621/8d2cadf0/attachment.html>