[FOM] 820: Sugared ZFC Formalization/2

[William M. Farmer]

Please see the paper

  W. M. Farmer.
  "Formalizing Undefinedness Arising in calculus".
  In: D. Basin and M. Rusinowitch, eds., 
  Automated Reasoning, LNCS, 3097:475-489, 2004. 
  http://imps.mcmaster.ca/doc/calculus.pdf

for an argument that free logic in the style advocated by Harvey
Friedman is indeed "fully consistent with ordinary mathematical
thinking".

Bill Farmer

> From: "Tennant, Neil" <tennant.9 at osu.edu>
> Thread-Topic: [FOM] 820: Sugared ZFC Formalization/2
> Date: Tue, 19 Jun 2018 12:22:07 +0000
> 
> 
> Harvey in effect relies on the scope distinctions that can be made fully explicit by the following use of bound variables to indicate term-insertions:
> 
> t_x (x=x)         false if the term t does not denote; true if the term t does denote
> 
> ~ t_x (x=x)      true if the term t does not denote; false if the term t does denote
> 
> t_x ~(x=x)       false if the term t does not denote; false if the term t does denote
> 
> The free logic that captures these intuitions about term-denotations and truth-conditions is set out in my paper
> 
> Natural deduction for first order logic with identity, descriptions and restricted quantification’, in Contributed Papers of the 5th International Congress of Logic, Methodology and Philosophy of Science, London, Ontario, 1975, pp. I 51-2.
> 
> See iterm 123 at https://u.osu.edu/tennant.9/publications/
> 
> Neil
> 
> 
> ________________________________________
> From: fom-bounces at cs.nyu.edu [fom-bounces at cs.nyu.edu] on behalf of Harvey Friedman [hmflogic at gmail.com]
> Sent: Monday, June 18, 2018 7:52 PM
> To: Foundations of Mathematics; Larry Paulson
> Subject: Re: [FOM] 820: Sugared ZFC Formalization/2
> 
> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
>