[FOM] 820: Sugared ZFC Formalization/2

[Tennant, Neil]

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