Saunders Mac Lane has drawn attention many times, particularly in his book Mathematics: Form and Function, to the system of set theory of which the axioms are Extensionality, Null Set, Pairing, Union, Infinity, Power Set, Restricted Separation, Foundation, and Choice, to which system, afforced by the principle, , of Transitive Containment, we shall refer as . His system is naturally related to systems derived from topos-theoretic notions concerning the category of sets, and is, as Mac Lane emphasises, one that is (...) adequate for much of mathematics. In this paper we show that the consistency strength of Mac Lane's system is not increased by adding the axioms of Kripke–Platek set theory and even the Axiom of Constructibility to Mac Lane's axioms; our method requires a close study of Axiom H, which was proposed by Mitchell; we digress to apply these methods to subsystems of Zermelo set theory , and obtain an apparently new proof that is not finitely axiomatisable; we study Friedman's strengthening of , and the Forster–Kaye subsystem of , and use forcing over ill-founded models and forcing to establish independence results concerning and ; we show, again using ill-founded models, that proves the consistency of ; turning to systems that are type-theoretic in spirit or in fact, we show by arguments of Coret and Boffa that proves a weak form of Stratified Collection, and that is a conservative extension of for stratified sentences, from which we deduce that proves a strong stratified version of ; we analyse the known equiconsistency of with the simple theory of types and give Lake's proof that an instance of Mathematical Induction is unprovable in Mac Lane's system; we study a simple set theoretic assertion—namely that there exists an infinite set of infinite sets, no two of which have the same cardinal—and use it to establish the failure of the full schema of Stratified Collection in ; and we determine the point of failure of various other schemata in . The paper closes with some philosophical remarks. (shrink)

§1. Introduction. This paper deals with aspects of my doctoral dissertation which contributed to the early development of model theory. What was of use to later workers was less the results of my thesis, than the method by which I proved the completeness of first-order logic—a result established by Kurt Gödel in his doctoral thesis 18 years before.The ideas that fed my discovery of this proof were mostly those I found in the teachings and writings of Alonzo Church. This may (...) seem curious, as his work in logic, and his teaching, gave great emphasis to the constructive character of mathematical logic, while the model theory to which I contributed is filled with theorems about very large classes of mathematical structures, whose proofs often by-pass constructive methods.Another curious thing about my discovery of a new proof of Gödel's completeness theorem, is that it arrived in the midst of my efforts to prove an entirely different result. Such “accidental” discoveries arise in many parts of scientific work. Perhaps there are regularities in the conditions under which such “accidents” occur which would interest some historians, so I shall try to describe in some detail the accident which befell me.A mathematical discovery is an idea, or a complex of ideas, which have been found and set forth under certain circumstances. The process of discovery consists in selecting certain input ideas and somehow combining and transforming them to produce the new output ideas. The process that produces a particular discovery may thus be represented by a diagram such as one sees in many parts of science; a “black box” with lines coming in from the left to represent the input ideas, and lines going out to the right representing the output. To describe that discovery one must explain what occurs inside the box, i.e., how the outputs were obtained from the inputs. (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)

Church's simple theory of types is a system of higher-order logic in which functions are assumed to be total. We present in this paper a version of Church's system called PF in which functions may be partial. The semantics of PF, which is based on Henkin's general-models semantics, allows terms to be nondenoting but requires formulas to always denote a standard truth value. We prove that PF is complete with respect to its semantics. The reasoning mechanism in PF for partial (...) functions corresponds closely to mathematical practice, and the formulation of PF adheres tightly to the framework of Church's system. (shrink)

This influential 1888 publication explained the real numbers, and their construction and properties, from first principles.

Higher-Order Logic (HOL) is a proof development system intended for applications to both hardware and software. It is principally used in two ways: for directly proving theorems, and as theorem-proving support for application-specific verification systems. HOL is currently being applied to a wide variety of problems, including the specification and verification of critical systems. Introduction to HOL provides a coherent and self-contained description of HOL containing both a tutorial introduction and most of the material that is needed for day-to-day work (...) with the system. After a quick overview that gives a "hands-on feel" for the way HOL is used, there follows a detailed description of the ML language. The logic that HOL supports and how this logic is embedded in ML, are then described in detail. This is followed by an explanation of the theorem-proving infrastructure provided by HOL. Finally two appendices contain a subset of the reference manual, and an overview of the HOL library, including an example of an actual library documentation. (shrink)

Even though it is not very often admitted, partial functions do play a significant role in many practical applications of deduction systems. Kleene has already given a semantic account of partial functions using three-valued logic decades ago, but there has not been a satisfactory mechanization. Recent years have seen a thorough investigation of the framework of many-valued truth-functional logics. However, strong Kleene logic, where quantification is restricted and therefore not truthfunctional, does not fit the framework directly. We solve this problem (...) by applying recent methods from sorted logics. This paper presents a resolution calculus that combines the proper treatment of partial functions with the efficiency of sorted calculi. (shrink)