[FOM] free logic

[William Farmer]

I have some experience with both formalizing and implementing the
approach to undefinedness that Harvey Friedman advocates.  I would
like to add a few points to the overview he gave (which I have
included below).

1. When mathematicians are being careful, they generally use the
approach Harvey described.  I like to call this approach the
"traditional approach to undefinedness".  Mathematicians use this
approach because it provides big benefits:

  a. Undefinedness is handled in a very simple way.  Undefined terms
     do not denote anything at all.  There is no need for a term like
     1/0 to denote an unspecified value, an error value, a
     "nonexistence" value, or some other kind of value.  Formulas
     involving undefined terms are always either true or false.  The
     is no need to say that these formulas are ill-formed or denote
     some nonstandard truth value.

  b. Most definedness conditions can be expressed implicitly so ideas
     involving partial functions and other sources of undefinedness
     can be expressed very succinctly.  For example, in a formula like

       f(a) = f(b) implies A

     the local context for A includes the following implicit
     definedness conditions: a, b, f, and g are defined; f is
     defined at a; and g is defined at b.

  c. There is no need to separate partial functions from total
     functions.  By default, function spaces include partial as well
     as total functions.  This yields pleasant results such as, if an
     integer is considered a real number, then a function that maps
     integers to integers is also considered a function that maps real
     numbers to real numbers.

  d. Definite description can be freely utilized because an improper
     definite description, like "the (unique) x such that x != x", is
     undefined.  Definite description is extensively employed in
     mathematical practice.  For example, any one of the definitions
     of a limit is expressed using definite description as in

       the limit of f(x) as x goes to a is the real number y such
       that, for every epsilon > 0, ...

     By this use of definite description, the limit is undefined
     whenever the condition "for every epsilon > 0, ..." does not
     hold.

2. Michael Spivak's well-known textbook Calculus is celebrated for its
careful presentation of calculus to university students.  In this book
he handles undefinedness according to the traditional approach (see
the discussion in [1]).  It is interesting to note that he represents
the two equalities that Harvey mentioned, = and ~, both by the symbol
=.  This is bothersome since there are many cases in which using the
wrong equality yields the wrong result.  However, Spivak comments in
the book that an equation a = b can mean either a = b (a and b are
both defined and have the same value) or a ~ b (a and b both have the
same value or are both undefined), depending on the context.
Apparently, he thought the confusion to students caused by
distinguishing a = b and a ~ b with syntax would be greater than the
confusion caused by being imprecise.

3. As Harvey noted, the traditional approach to undefinedness can be
formalized relatively easily.  As far as I know, this was first shown
by Rolf Schock in 1968.  Several other people have independently
proposed the same kind of formalization as Schock's including Michael
Beeson, Tyler Burge, Leonard Monk, and David Parnas.  The
formalization works for many logics including first-order logic and
simple type theory.  In [2], I carefully show what changes need to be
made to Peter Andrews' version of Church's type theory to formalize
the traditional approach.

4. My colleagues, Joshua Guttman and Javier Thayer, and I built a
proof assistant named IMPS [3,4] in the early 1990s that was based on
a version of Church's type theory that formalizes the traditional
approach to undefinedness.  Using IMPS, we developed a theory library
containing a great deal of basic mathematics including an abstract
development of mathematical analysis.  The IMPS system, and its theory
library, demonstrate (I think convincingly) that a logic admitting
undefined terms can be effectively implemented and can successfully
capture the benefits of the traditional approach mentioned above.

5. One criticism of basing a proof assistant on a logic that admits
undefined terms is that (1) proofs then necessarily include a plethora
of subgoals of the form "a is defined" and (2) the proof process
becomes overwhelmed by the sheer number of these pesky subgoals. (1)
is true, but (2) need not be true if the proof assistant comes with
adequate facilities for automatically resolving definedness subgoals.
The definedness subgoals that arise in IMPS are not a problem at all
because the IMPS simplifier can automatically verify the vast majority
of them.  Those that it cannot verify are almost always subgoals that
say something nontrivial concerning undefinedness and require some
insight to be proved.

6. The three most salient characteristics of IMPS are (1) its logic
that admits undefined terms, (2) its use of the "little theories"
method to represent mathematical knowledge as a network of
interconnected axiomatic theories, and (3) its proofs that are a blend
of computation and deduction. (2) and (3) have been widely accepted by
the theorem proving community as good ideas.  However, (1) has been
much less accepted.  Moreover, some researchers have been openly
hostile to (1).  I have long been puzzled why there is not stronger
support for basing proof assistants on logics that deal with
undefinedness according to how mathematicians deal with undefinedness.

[1] 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

[2] W. M. Farmer.
    "Andrews' type system with undefinedness".      
    In: C. Benzmueller, C. Brown J. Siekmann, and R. Statman, eds.,
    Reasoning in Simple Type Theory: Festschrift in Honor of Peter
    B. Andrews on his 70th Birthday, Studies in Logic, pp. 223–242,
    College Publications, 2008.
    http://imps.mcmaster.ca/doc/andrews.pdf

[3] W. M. Farmer, J. D. Guttman, and F. J. Thayer.
    "IMPS: An Interactive Mathematical Proof System".
    Journal of Automated Reasoning 11:213-248, 1993.
    http://imps.mcmaster.ca/doc/imps-overview.pdf

[4] W. M. Farmer, J. D. Guttman, and F. J. Thayer Fabrega.
    "IMPS: An updated system description". 
    In: M. McRobbie and J. Slaney, eds,
    Automated Deduction -- CADE-13, LNCS 1104: 298-302, 1996.
    http://imps.mcmaster.ca/doc/cade-13-sys-desc.pdf

Bill Farmer
McMaster University


> From: Harvey Friedman <hmflogic at gmail.com>
> Date: Sat, 24 Oct 2015 01:20:05 +0000
> 
> There has been discussion of how to handle undefined terms in the
> formalization of mathematics.
> 
> I have stated my views in one form or another perhaps half a dozen
> times on the FOM and a few times recently.
> 
> Now that there is a focus on this, let me elaborate a bit on it again.
> 
> 1. Mathematicians have good instincts about this, but are not normally
> interested in being systematic and entirely consistent. They just want
> to make sure that there is no practical ambiguity in what they write.
> 
> 2. I have practiced a particular way of dealing with undefined terms
> for many decades and am totally convinced that from the formalization
> of mathematics point of view, which does not include any
> considerations about Provers, that there is an optimally simple
> systematic way of handling this. Furthermore, that this would also be
> the easiest and most friendly *systematic* solution for the general
> mathematical community, and that they would easily accept it as the
> Gold Standard if they were compelled to endorse a Gold Standard.
> 
> 3. This way of handling undefined terms is not due to me. I don't know
> what credit should be assigned to it. It comes also with the entirely
> appropriate and obvious Completeness Theorem. It can be done first in
> one sorted predicate calculus with equality, and then extended to many
> sorted predicate calculus with or without equality in obvious ways.
> 
> 4. So I will only talk about one sorted predicate calculus with
> equality. I will proceed semiformally. There is no problem being fully
> formal.
> 
> 5. In addition to =, there is ~ and uparrow and downarrow. There is no
> such thing as "the undefined element".
> 
> 6. We have constants, relation symbols, function symbols.
> 
> 7. s = t means that the terms s,t are defined and have the same value.
> 
> 8. s ~ t means that the terms s,t are either both undefined or both
> defined with the same value.
> 
> 9. s uparrow means s is undefined. s downarrow means s is defined.
> 
> 10. Variables are always defined. I.e., we have x downarrows.
> Constants are always defined. I.e., we have c downarrows.
> 
> 11. All atomic formulas are true or false. There is no such thing as
> an undefined atomic formula, or an undefined truth value. In fact,
> there is no explicit notion of truth value other than what is
> represented if we are using the absurdity symbol. (absurdity indicates
> false, and absurdity --> indicates true). However, that is a
> propositional calculus matter, and is optional.
> 
> 12. A term other than a variable or a constant, is defined if and only
> if all of its subterms are defined. E.g., 1/0 - 1/0 is not defined for
> x = 0.
> 
> 13. There is the usual implicit assumption that there is at least one
> thing in the domain.
> 
> 14. forall x  blah blah blah, means, of course, that for all actual
> existing elements of the domain, x, such that blah blah blah.
> 
> 15. therexists x blah blah blah, means, of course, that there is an
> actual existing element of the domain, x, such that blah blah blah.
> 
> 16. Examples. 1/0 - 1/0 <= 1/0 - 1/0 is false. 1/0 - 1/0 = 1/0 - 1/0 is false.
> 
> Harvey Friedman
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>