[FOM] free logic

[William Farmer]

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.