[FOM] free logic

[Joe Shipman]

Has inadequate attention to these issues ever resulted in failure to prove a mathematical theorem that was proved after more care had been taken?

Has inadequate attention to these issues ever resulted in a proof of a false mathematical proposition being published?

I think not, and that these issues are important only for mechanizing proof assistants (which is indeed valuable), but I'd be interested to be shown to be mistaken about this.

-- JS

Sent from my iPhone

> On Oct 27, 2015, at 9:40 AM, William Farmer <wmfarmer at mcmaster.ca> wrote:
> 
> 
> I have a few more comments about logics that formalize the traditional
> approach to undefinedness.
> 
> 1. In a logic that admits undefined terms as sketched by Harvey
> Friedman, a common mistake is to think of an undefined term as
> denoting a value that can have properties.  To the contrary, an
> undefined term does not denote any value whatsoever and hence the
> application of a predicate to a list of terms that includes at least
> one undefined term is not a meaningful assertion and is considered
> false by convention.  This means that undefined terms, like 1/0 and
> lim x->0 sin 1/x, are semantically indistinguishable.  This also means
> that statements like
> 
>  1/0 = 1/0, 
>  1/0 < 1/0, 
>  1/0 >= 1/0, 
>  1/0 = 2, 
>  "1/0 is an integer", and
>  lim x->0 sin 1/x = 0
> 
> are semantically indistinguishable.  These statements look like they
> say something, but they actually say nothing at all.
> 
> 2. Anthony Coulter said:
> 
>> 1. When I took calculus in school we had only one equal sign to
>>   worry about. I'm looking through my 3rd edition Spivak and I
>>   don't see any discussion about there being a second equality
>>   relation. So I'm skeptical that "the traditional approach to
>>   undefinedness" really involves two distinct notions of equality.
> 
> Spivak doesn't discuss the ~ equality, but he mentions (after Exercise
> 28 on p. 92 of Edition 1 and after Exercise 30 on p. 110 of Edition 3)
> that there are several different ways to interpret an expression a = b
> where a or b might be undefined.  The first way he mentions is the ~
> notion of equality.  He suggests that the reader has to decide what
> interpretation of a = b is suitable in a particular context.
> 
> Spivak does use = to represent both the = and ~ equalities.  For
> example, he defines the quotient of two functions (on p. 41 of Edition
> 1 and on p. 43 of Edition 3) by
> 
>  (f/g)(x) = f(x)/g(x)
> 
> but by this he really means
> 
>  (f/g)(x) ~ f(x)/g(x)
> 
> which says (f/g)(x) = f(x)/g(x) whenever f(x)/g(x) is defined and is
> undefined whenever f(x)/g(x) is undefined.  (See his comment in
> italics on p. 39 of Edition 1 and on p. 41 of Edition 3.)
> 
> It is not uncommon for calculus textbook writers to define a partial
> function as
> 
>  f(x) = t
> 
> but mean
> 
>  f(x) ~ t.
> 
> When f is defined in this way using ~, the domain of f is implicitly
> defined.  This kind of definition is especially useful when the domain
> of the function is burdensome to define and there is no need to
> understand its full definition.  In proof assistants that do not admit
> undefined terms it is usually necessary to explicitly define the
> domain of a partial function.  It is not necessary in IMPS.
> 
> 3. In the early 1990s my colleagues and I gave some tutorials on IMPS
> to engineers.  We found that if we said nothing about the IMPS logic
> the engineers picked up on how IMPS worked with no difficulty.  The
> way undefinedness is handled in IMPS seemed to match their intuition
> about undefinedness quite well.  However, if we started a tutorial out
> by explaining the logic, it led to a lot of confusion.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom