Undefinedness in Accordance with Mathematical Practice

McGill University

Montreal, Quebec, Canada

2 August 2009

The goals of this tutorial are to:

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

- The nature of undefinedness
- Where undefinedness comes from
- Approaches for dealing with undefinedness in traditional logics [3,12,14]
- The traditional approach to undefinedness used in mathematical practice [5,7]
- Benefits of the traditional approach

- How to create a version of first-order logic that admits
undefinedness
- Changes to syntax
- Changes to semantics
- Definedness concepts
- Changes to the laws of predicate logic

- Other examples of logics with undefinedness
- Church's type theory [3,7,9]
- Church's type theory with subtypes (IMPS logic) [4]
- NBG set theory with types [6,10]
- NBG set theory with types, quotation, and evaluation [8]

- How to implement a logic with undefinedness [11]
- Substitution
- Definedness checking

- 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 - O. Müller and K. Slind, "Treating partiality in a logic
of total functions", in:
*The Computer Journal*, 40:640–652, 1997. Online

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.

- M. Beeson, "Formalizing constructive mathematics: Why and
how?", in: F. Richman, ed.,
*Constructive Mathematics: Proceedings*, New Mexico, 1980, LNM 873:146–190, 1981. Online - T. Burge,
*Truth and Some Referential Devices*, Ph.D. Thesis, Princeton University 1971. - W. M. Farmer, "A partial functions version of Church's simple
theory of types",
*Journal of Symbolic Logic*, 55:1269–91, 1990. - W. M. Farmer, "A simple type theory with partial functions and
subtypes",
*Annals of Pure and Applied Logic*, 64:211–240, 1993. - W. M. Farmer, "Reasoning about partial functions with the aid
of a computer",
*Erkenntnis*, 43:279–294, 1995. - W. M. Farmer, "STMM: A Set Theory for Mechanized Mathematics",
*Journal of Automated Reasoning*, 26:269–289, 2001. Online - 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 - 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 - 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 - 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 - 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 - C. B. Jones, "References relating to reasoning about partial functions", Newcastle University, UK, 2007. Online
- L. G. Monk, "PDLM: A Proof Development Language for Mathematics", Technical Report M86-37, The MITRE Corporation, Bedford, MA, USA, 1986.
- O. Müller and K. Slind, "Treating partiality in a logic of
total functions",
*The Computer Journal*, 40:640–652, 1997. Online - D. L. Parnas, "Predicate logic for software engineering",
*IEEE Transactions on Software Engineering*, 19: 856–861, 1993. Online - R. Schock,
*Logics without Existence Assumptions*, Almqvist & Wiksells, 1968 - M. Spivak,
*Calculus, Third Edition*, Publish or Perish, 1994.

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.