Records the three layers under the foundations: an informal metatheory, classical first-order logic with equality, and von Neumann-Bernays-Gödel class theory as a first-order theory with dependent choice to be added; explains where formulas enter and why statements about all subsets are first-order inside the theory.
The foundations of the database rest on three layers.
The metatheory. Proofs are written informally but rigorously, as in mathematical textbooks; derivations in a formal calculus are not written out. The metatheory is also where strings of symbols and their finite counts are understood: Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations and the theorem scheme The Class Comprehension Theorem for Predicative Formulas belong to it. The numbers used there to count symbols are informal; they are not the natural numbers constructed inside the theory.
The logic. The logic is classical first-order predicate logic with equality: proof by contradiction and the law of excluded middle are allowed, and quantifiers range over the objects of the theory only. The language has class variables and set variables, and a quantifier over a set variable ranges over the sets; underneath, the logic is one-sorted, a set quantifier being the relativisation of a class quantifier to the classes that are sets.
The theory. The theory is von Neumann-Bernays-Gödel class theory (NBG) without global choice, in the presentation of Mendelson, whose objects are classes, with the sets among them. Its axioms are Axiom of Extensionality for Classes, Axiom of Pairing, Axiom of the Empty Set, Axioms of Class Existence (Gödel's Axioms B1-B7), Axiom of Separation for Classes, Axiom of Union, Axiom of Power Set, Axiom of Replacement for Classes, Axiom of Infinity and Axiom of Foundation for Classes; each is a single sentence, except class existence, which consists of Gödel's seven sentences B1-B7, and there is no axiom scheme. The schemes that do occur belong to the metatheory: the tuple notation of The Ordered Pair of Two Sets and Nested Tuples §tuple with its characteristic property The Characteristic Property of Ordered Pairs and Nested Tuples of Sets §tuples, and class comprehension for predicative formulas, which is a theorem scheme. The axiom of dependent choice is to be added once the natural numbers and sequences are available. NBG proves exactly the same statements about sets as Zermelo-Fraenkel set theory ZF (it is a conservative extension of ZF), and this persists when dependent choice, stated for sets, is added to both.
Second-order statements. Statements quantifying over all subsets of a set, such as induction over the natural numbers or the least upper bound property of the real numbers, are first-order statements in NBG: the subsets are sets, and the quantifier ranges over them. Their categoricity is accordingly a theorem proved inside the theory. That different models of NBG may contain different subsets of a given infinite set is a fact about models, observed from outside, and affects no theorem.
Loading…
No relations recorded yet.