[FOM] free logic

[Lawrence Paulson]

[Perhaps there is some prospect of inviting Mike Fourman into this discussion. He is well familiar with such issues through his work on what is sometimes called the Scott-Fourman logic. I believe that he was also involved with an implementation of such a formalism. Obviously, William Farmer is also very experienced with this topic.]

There is no doubt that a free logic is more expressive and precise than higher-order logic as typically used in proof assistants, where every term is defined but doesn’t necessarily denote anything sensible. The question is whether the additional expressiveness justifies the additional complications involved in implementing and using a free logic. It’s unfortunate that IMPS, which incorporated a lot of novel ideas, failed to catch on with the research community. Instead, many researchers (particularly in the USA) adopted PVS, which combined the “everything is defined” basis of higher-order logic with a well-definedness check, which returned a list of assertions that the user had to prove in order to guarantee that every function was applied within its domain. This latter approach was possibly easier to use, but as it turned out, very difficult to implement the soundly. PVS was plagued by critical bugs for some time.

Partial functions and definedness don’t seem to come up as issues in discussions with colleagues about the limitations of our systems. Nor are they discussed as topics that need addressing in papers that I read, unless they are specifically on this topic to begin with. We seem to cope with definedness perfectly well within our formalisms. We have used descriptions, both definite and indefinite, for 30 years. I have personal experience of formalising a wide range of mathematical material, including elementary number theory and group theory, Gödel’s incompleteness theorem, Gödel’s constructible universe and the relative consistency of the axiom of choice, and more recently a lot of results in complex analysis, such as Cauchy’s integral formula and the Weierstraß approximation theorem. In analysis, there are many situations where limits or integrals are undefined; these are easily dealt with using relations, for example, <x_i> converges to y. A relational assertion tells us that the limit exists as well as telling us what it is. Advocates of free logics really have to prove that they can deliver useful additional expressiveness without imposing unreasonable costs.

Larry Paulson


> On 25 Oct 2015, at 18:39, William Farmer <wmfarmer at mcmaster.ca> wrote:
> 
> 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
>> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom