Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows how the traditional approach to partial functions (...) can be formalized in a range of formalisms that includes first-order logic, simple type theory, and Von-Neumann—Bernays—Gödel set theory. It argues that these new formalisms allow one to directly reason about partial functions; are based on natural, well-understood, familiar principles; and can be effectively implemented in mechanized mathematics systems. (shrink)

LetCbe an axiom system formalized within the first order functional calculus, and letC′ be related toCas the Bernays-Gödel set theory is related to the Zermelo-Fraenkel set theory. Ilse Novak [5] and Mostowski [8] have shown that, ifCis consistent, thenC′ is consistent. Mostowski has also proved the stronger result that any theorem ofC′ which can be formalized inCis a theorem ofC.The proofs of Novak and Mostowski do not provide a direct method for obtaining a contradiction inCfrom a contradiction inC′. We could, (...) of course, obtain such a contradiction by proving the theorems ofCone by one; the above result assures us that we must eventually obtain a contradiction. A similar process is necessary to obtain the proof of a theorem inCfrom its proof inC′. The purpose of this paper is to give a new proof of these theorems which provides a direct method of obtaining the desired contradiction or proof.The advantage of the proof may be stated more specifically by arithmetizing the syntax ofCandC′. (shrink)

Questions of definedness are ubiquitous in mathematics. Informally, these involve reasoning about expressions which may or may not have a value. This paper surveys work on logics in which such reasoning can be carried out directly, especially in computational contexts. It begins with a general logic of partial terms, continues with partial combinatory and lambda calculi, and concludes with an expressively rich theory of partial functions and polymorphic types, where termination of functional programs can be established in a natural way.

In his doctor's thesis [1], Henkin has shown that if a formal logic is consistent, and sufficiently complex, then it must admit a non-standard model. In particular, he showed that there must be a model in which that portion of the model which is supposed to represent the positive integers of the formal logic is not in fact isomorphic to the positive integers; indeed it is not even well ordered by what is supposed to be the relation of ≦.For the (...) purposes of the present paper, we do not need a precise definition of what is meant by a standard model of a formal logic. The non-standard models which we shall discuss will be flagrantly non-standard, as for instance a model of the sort whose existence is proved by Henkin. It will suffice if we and our readers are in agreement that a model of a formal logic is not a standard model if either: The relation in the model which represents the equality relation in the formal logic is not the equality relation for objects of the model. That portion of the model which is supposed to represent the positive integers of the formal logic is not well ordered by the relation ≦. That portion of the model which is supposed to represent the ordinal numbers of the formal logic is not well ordered by the relation ≦. (shrink)

Simple type theory is a higher-order predicate logic for reasoning about truth values, individuals, and simply typed total functions. We present in this paper a version of simple type theory, called PF*, in which functions may be partial and types may have subtypes. We define both a Henkin-style general models semantics and an axiomatic system for PF*, and we prove that the axiomatic system is complete with respect to the general models semantics. We also define a notion of an interpretation (...) of one PF* theory in another. PF* is intended as a foundation for mechanized mathematics. It is the basis for the logic of, an Interactive Mathematical Proof System developed at The MITRE Corporation. (shrink)