[FOM] free logic
Joe Shipman
joeshipman at aol.com
Tue Oct 27 18:11:59 EDT 2015
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
More information about the FOM
mailing list