NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF

Natural Formalization proposes a concrete way of expanding proof theory from the meta-mathematical investigation of formal theories to an examination of “the concept of the specifically mathematical proof.” Formal proofs play a role for this examination in as much as they reflect the essential structure and systematic construction of mathematical proofs. We emphasize three crucial features of our formal inference mechanism: (1) the underlying logical calculus is built for reasoning with gaps and for providing strategic directions, (2) the mathematical frame is a definitional extension of Zermelo–Fraenkel set theory and has a hierarchically organized structure of concepts and operations, and (3) the construction of formal proofs is deeply connected to the frame through rules for definitions and lemmas. To bring these general ideas to life, we examine, as a case study, proofs of the Cantor–Bernstein Theorem that do not appeal to the principle of choice. A thorough analysis of the multitude of “different” informal proofs seems to reduce them to exactly one. The natural formalization confirms that there is one proof, but that it comes in two variants due to Dedekind and Zermelo, respectively. In this way it enhances the conceptual understanding of the represented informal proofs. The formal, computational work is carried out with the proof search system AProS that serves as a proof assistant and implements the above inference mechanism; it can be fully inspected at http://www.phil.cmu.edu/legacy/Proof_Site/. We must—that is my conviction—take the concept of the specifically mathematical proof as an object of investigation. Hilbert 1918

A SYNTACTIC CHARACTERIZATION OF MORITA EQUIVALENCE

We characterize Morita equivalence of theories in the sense of Johnstone in terms of a new syntactic notion of a common definitional extension developed by Barrett and Halvorson for cartesian, regular, coherent, geometric and first-order theories. This provides a purely syntactic characterization of the relation between two theories that have equivalent categories of models naturally in any Grothendieck topos.

HOLCF = HOL + LCF

HOLCF is the definitional extension of Church's Higher-Order Logic with Scott's Logic for Computable Functions that has been implemented in the theorem prover Isabelle. This results in a flexible setup for reasoning about functional programs. HOLCF supports standard domain theory (in particular fixpoint reasoning and recursive domain equations), but also coinductive arguments about lazy datatypes. This paper describes in detail how domain theory is embedded in HOL, and presents applications from functional programming, concurrency and denotational semantics.

On Boolean algebras and integrally closed commutative regular rings

In this paper we consider properties, related to model-completeness, of the theory of integrally closed commutative regular rings. We obtain the main theorem claiming that in a Boolean algebra B, the truth of a prenex Σn-formula whose parameters ai, partition B, can be determined by finitely many conditions built from the first entry of Tarski invariant T(ai)'s, n-characteristic D(n, ai)'s and the quantities S(ai, l) and S′(ai, l) for l < n. Then we derive two important theorems. One claims that for any Boolean algebras A and B, an embedding of A into B preserving D(n, a) for all a ϵ A is a Σn-extension. The other claims that the theory of n-separable Boolean algebras admits elimination of quantifiers in a simple definitional extension of the language of Boolean algebras. Finally we translate these results into the language of commutative regular rings.

Categorical semantics for higher order polymorphic lambda calculus

A categorical structure suitable for interpreting polymorphic lambda calculus (PLC) is defined, providing an algebraic semantics for PLC which is sound and complete. In fact, there is an equivalence between the theories and the categories. Also presented is a definitional extension of PLC including “subtypes”, for example, equality subtypes, together with a construction providing models of the extended language, and a context for Girard's extension of the Dialectica interpretation.

Algebraic theories with definable Skolem functions

(1.1) A well-known example of a theory with built-in Skolem functions is (first-order) Peano arithmetic (or rather a certain definitional extension of it). See [C-K, pp. 143, 162] for the notion of a theory with built-in Skolem functions, and for a treatment of the example just mentioned. This property of Peano arithmetic obviously comes from the fact that in each nonempty definable subset of a model we can definably choose an element, namely, its least member.(1.2) Consider now a real closed field R and a nonempty subset D of R which is definable (with parameters) in R. Again we can definably choose an element of D, as follows: D is a union of finitely many singletons and intervals (a, b) where – ∞ ≤ a < b ≤ + ∞; if D has a least element we choose that element; if not, D contains an interval (a, b) for which a ∈ R ∪ { − ∞}is minimal; for this a we choose b ∈ R ∪ {∞} maximal such that (a, b) ⊂ D. Four cases have to be distinguished:(i) a = − ∞ and b = + ∞; then we choose 0;(ii) a = − ∞ and b ∈ R; then we choose b − 1;(iii) a ∈ R and b ∈ = + ∞; then we choose a + 1;(iv) a ∈ R and b ∈ R; then we choose the midpoint (a + b)/2.It follows as in the case of Peano arithmetic that the theory RCF of real closed fields has a definitional extension with built-in Skolem functions.