Tutorial at CADE-22

Logics with Undefinedness

How to Modify a Traditional Logic so that It Handles
Undefinedness in Accordance with Mathematical Practice

McGill University
Montreal, Quebec, Canada
2 August 2009

William M. Farmer



Overview

Undefined terms arise naturally in mathematics and computing. There is, more or less, a traditional approach to dealing with undefinedness in mathematical practice [5,7]. The benefits of the approach are (1) undefinedness can be handled directly and (2) statements involving definedness can be written very concisely since many definedness conditions can be expressed implicitly. Unfortunately, this approach to undefinedness is not supported by traditional logics and reasoning systems — such as first-order logic, simple type theory, and ZF set theory — since terms must always be defined in these systems. Several logicians, computer scientists, and software engineers have independently noticed that the traditional approach to undefinedness can be formalized in a traditional logic if the logic is modified slightly [1,2,13,15,16], yielding what we call a logic with undefinedness. Moreover, one such logic with undefinedness, a version of Church's type theory [3,4], is the logical basis for IMPS [11], a successful higher-order theorem proving system first released in 1993. Although a logic with undefinedness is clearly closer to mathematical practice than a traditional logic, except for a few exceptions like IMPS, the reasoning systems produced by the automated reasoning community are based on logics that do not handle undefinedness according to the traditional approach.

The goals of this tutorial are to:

  1. Describe the traditional approach to undefinedness used in mathematical practice.
  2. Demonstrate the benefits that are gained by employing a logic with undefinedness.
  3. Show what modifications are needed to transform a traditional logic into a logic with undefinedness.
  4. Present the techniques needed to implement a logic with undefinedness.

Target Audience

Students and researchers who are interested in approaches to undefinedness or the design and implementation of logics for practical use. No special background is needed for the tutorial except a basic understanding of first-order logic.

Outline

  1. The nature of undefinedness
  2. How to create a version of first-order logic that admits undefinedness
  3. Other examples of logics with undefinedness
  4. How to implement a logic with undefinedness [11]

Suggested Reading Before the Tutorial

  1. W. M. Farmer, "Formalizing undefinedness arising in calculus", in: D. Basin and M. Rusinowitch, eds., Automated Reasoning, Lecture Notes in Computer Science (LNCS), 3097:475–489, 2004. Online
  2. O. Müller and K. Slind, "Treating partiality in a logic of total functions", in: The Computer Journal, 40:640–652, 1997. Online

Warm up Exercise

Formalize in your favorite logic the following theorem from calculus:

  For all real-valued functions f : R -> R and real numbers a : R,

    lim f(x) = lim f(x) implies lim f(x) exists.
    x->a-      x->a+            x->a
See [17, p. 110, Problem 29] for details.

References

  1. M. Beeson, "Formalizing constructive mathematics: Why and how?", in: F. Richman, ed., Constructive Mathematics: Proceedings, New Mexico, 1980, LNM 873:146–190, 1981. Online
  2. T. Burge, Truth and Some Referential Devices, Ph.D. Thesis, Princeton University 1971.
  3. W. M. Farmer, "A partial functions version of Church's simple theory of types", Journal of Symbolic Logic, 55:1269–91, 1990.
  4. W. M. Farmer, "A simple type theory with partial functions and subtypes", Annals of Pure and Applied Logic, 64:211–240, 1993.
  5. W. M. Farmer, "Reasoning about partial functions with the aid of a computer", Erkenntnis, 43:279–294, 1995.
  6. W. M. Farmer, "STMM: A Set Theory for Mechanized Mathematics", Journal of Automated Reasoning, 26:269–289, 2001. Online
  7. W. M. Farmer, "Formalizing undefinedness arising in calculus", in D. Basin and M. Rusinowitch, eds., Automated Reasoning, Lecture Notes in Computer Science (LNCS), 3097:475–489, 2004. Online
  8. W. M. Farmer, "Chiron: A multi-paradigm logic", in: R. Matuszewski and A. Zalewska, eds, From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar and Rhetoric, 10(23):1–19, 2007. Online
  9. W. M. Farmer, "Andrews' type system with undefinedness", in: C. Benzmüller, 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. Online
  10. W. M. Farmer and J. D. Guttman, "A set theory with support for partial functions", Partiality and Modality, special issue of Studia Logica, 66:59–78, 2000. Online
  11. W. M. Farmer, J. D. Guttman, and F. J. Thayer, "IMPS: An Interactive Mathematical Proof System", Journal of Automated Reasoning, 11:213–248, 1993. Online
  12. C. B. Jones, "References relating to reasoning about partial functions", Newcastle University, UK, 2007. Online
  13. L. G. Monk, "PDLM: A Proof Development Language for Mathematics", Technical Report M86-37, The MITRE Corporation, Bedford, MA, USA, 1986.
  14. O. Müller and K. Slind, "Treating partiality in a logic of total functions", The Computer Journal, 40:640–652, 1997. Online
  15. D. L. Parnas, "Predicate logic for software engineering", IEEE Transactions on Software Engineering, 19: 856–861, 1993. Online
  16. R. Schock, Logics without Existence Assumptions, Almqvist & Wiksells, 1968
  17. M. Spivak, Calculus, Third Edition, Publish or Perish, 1994.

Presenter

William M. Farmer is a Professor in the Department of Computing and Software at McMaster University in Hamilton, Ontario, Canada. He received a B.A. in mathematics from the University of Notre Dame (Notre Dame, Indiana, USA) in 1978. He attended graduate school at the University of Wisconsin-Madison (Madison, Wisconsin, USA), where he received an M.A. in mathematics in 1980, an M.S. in computer sciences in 1983, and a Ph.D. in mathematics in 1984. Before joining McMaster in 1999, he conducted research in various areas of computer science for twelve years at The MITRE Corporation (Bedford, Massachusetts, USA). Dr. Farmer also taught computer programming and networking courses for two years at St. Cloud State University (St. Cloud, Minnesota, USA).

Dr. Farmer's primary research interests are applied logic, computer support for mathematical reasoning, mathematical knowledge management, and formal methods in software development. In partnership with Dr. Joshua Guttman and Dr. Javier Thayer at MITRE in the early 1990s, he designed and implemented the IMPS Interactive Mathematical Proof System. In 2001, he started the MathScheme project whose goal is to develop a new approach to mechanized mathematics that integrates and generalizes computer theorem proving and computer algebra.