Introduction. The system of axioms for set theory to be exhibited in this paper is a modification of the axiom system due to von Neumann. In particular it adopts the principal idea of von Neumann, that the elimination of the undefined notion of a property (“definite Eigenschaft”), which occurs in the original axiom system of Zermelo, can be accomplished in such a way as to make the resulting axiom system elementary, in the sense of being formalizable in the logical (...) calculus of first order, which contains no other bound variables than individual variables and no accessory rule of inference (as, for instance, a scheme of complete induction).The purpose of modifying the von Neumann system is to remain nearer to the structure of the original Zermelo system and to utilize at the same time some of the set-theoretic concepts of the Schröder logic and of Principia mathematica which have become familiar to logicians. As will be seen, a considerable simplification results from this arrangement.The theory is not set up as a pure formalism, but rather in the usual manner of elementary axiom theory, where we have to deal with propositions which are understood to have a meaning, and where the reference to the domain of facts to be axiomatized is suggested by the names for the kinds of individuals and for the fundamental predicates.On the other hand, from the formulation of the axioms and the methods used in making inferences from them, it will be obvious that the theory can be formalized by means of the logical calculus of first order (“Prädikatenkalkul” or “engere Funktionenkalkül”) with the addition of the formalism of equality and the ι-symbol for “descriptions” (in the sense of Whitehead and Russell). (shrink)

The reader of Part VI will have noticed that among the set-theoretic models considered there some models were missing which were announced in Part II for certain proofs of independence. These models will be supplied now.Mainly two models have to be constructed: one with the property that there exists a set which is its own only element, and another in which the axioms I–III and VII, but not Va, are satisfied. In either case we need not satisfy the axiom of (...) infinity. Thereby it becomes possible to set up the models on the basis of only I–III, and either VII or Va, a basis from which number theory can be obtained as we saw in Part II.On both these bases the Π0-system of Part VI, which satisfies the axioms I–V and VII, but not VI, can be constructed, as we stated there. An isomorphic model can also be obtained on that basis, by first setting up number theory as in Part II, and then proceeding as Ackermann did.Let us recall the main points of this procedure.For the sake of clarity in the discussion of this and the subsequent models, it will be necessary to distinguish precisely between the concepts which are relative to the basic set-theoretic system, and those which are relative to the model to be defined. (shrink)

We discuss the work of Paul Bernays in set theory, mainly his axiomatization and his use of classes but also his higher-order reflection principles.

We present an axiomatic framework for nonstandard analysis-the Nonstandard Class Theory which extends von Neumann-Godel-Bernays Set Theory by adding a unary predicate symbol St to the language of NBG means that the class X is standard) and axioms-related to it- analogs of Nelson's idealization, standardization and transfer principles. Those principles are formulated as axioms, rather than axiom schemes, so that NCT is finitely axiomatizable. NCT can be considered as a theory of definable classes of Bounded Set (...) class='Hi'>Theory by V. Kanovei and M. Reeken. In many aspects NCT resembles the Alternative Set Theory by P. Vopenka. For example there exist semisets in NCT and it can be proved that a set has a standard finite cardinality iff it does not contain any proper subsemiset. Semisets can be considered as external classes in NCT. Thus the saturation principle can be formalized in NCT. (shrink)

As is well-known, the Bernays-Schönfinkel-Ramsey class of all prenex ∃*∀* -sentences which are valid in classical first-order logic is decidable. This paper paves the way to an analogous result which the authors deem to hold when the only available predicate symbols are ∈ and =, no constants or function symbols are present, and one moves inside a (rather generic) Set Theory whose axioms yield the well-foundedness of membership and the existence of infinite sets. Here semi-decidability of the satisfiability problem (...) for the BSR class is proved by following a purely semantic approach, the remaining part of the decidability result being postponed to a forthcoming paper. (shrink)

As proved recently, the satisfaction problem for all prenex formulae in the set-theoretic Bernays-Shönfinkel-Ramsey class is semi-decidable over von Neumann's cumulative hierarchy. Here that semi-decidability result is strengthened into a decidability result for the same collection of formulae.

Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel set theory for (...) reasoning about sets, proper classes, and partial functions represented as classes of ordered pairs. The underlying logic of the system is a partial first-order logic, so class-valued terms may be nondenoting. Functions can be specified using lambda-notation, and reasoning about the application of functions to arguments is facilitated using sorts similar to those employed in the logic of the IMPS Interactive Mathematical Proof System. The set theory is intended to serve as a foundation for mechanized mathematics systems. (shrink)

A pointwise definable model is one in which every object is \loos definable without parameters. In a model of set theory, this property strengthens $V=\HOD$, but is not first-order expressible. Nevertheless, if \ZFC\ is consistent, then there are continuum many pointwise definable models of \ZFC. If there is a transitive model of \ZFC, then there are continuum many pointwise definable transitive models of \ZFC. What is more, every countable model of \ZFC\ has a class forcing extension that is pointwise (...) definable. Indeed, for the main contribution of this article, every countable model of Gödel-Bernays set theory has a pointwise definable extension, in which every set and class is first-order definable without parameters. (shrink)

This text unites the logical and philosophical aspects of set theory in a manner intelligible both to mathematicians without training in formal logic and to logicians without a mathematical background. It combines an elementary level of treatment with the highest possible degree of logical rigor and precision. Starting with an explanation of all the basic logical terms and related operations, the text progresses through a stage-by-stage elaboration that proves the fundamental theorems of finite sets. It focuses on the Bernays (...) theory of finite classes and finite sets, exploring the system's basis and development, including Stage I and Stage II theorems, the theory of finite ordinals, and the theory of finite classes and finite sets. This volume represents an excellent text for undergraduates studying intermediate or advanced logic as well as a fine reference for professional mathematicians. (shrink)

A new axiomatization of set theory, to be called Bernays-Boolos set theory, is introduced. Its background logic is the plural logic of Boolos, and its only positive set-theoretic existence axiom is a reflection principle of Bernays. It is a very simple system of axioms sufficient to obtain the usual axioms of ZFC, plus some large cardinals, and to reduce every question of plural logic to a question of set theory.

In this article I investigate the phenomenon of minimum and minimal models of second-order set theories, focusing on Kelley–Morse set theory KM, Gödel–Bernays set theory GB, and GB augmented with the principle of Elementary Transfinite Recursion. The main results are the following. (1) A countable model of ZFC has a minimum GBC-realization if and only if it admits a parametrically definable global well order. (2) Countable models of GBC admit minimal extensions with the same sets. (3) There is (...) no minimum transitive model of KM. (4) There is a minimum β-model of GB+ETR. The main question left unanswered by this article is whether there is a minimum transitive model of GB+ETR. (shrink)

We introduce an extension of the propositional calculus to include abstracts of predicates and quantifiers, employing a single rule along with a novel comprehension schema and a principle of extensionality, which are substituted for the Bernays postulates for quantifiers and the comprehension schemata of ZF and other set theories. We prove that it is consistent in any finite Boolean subset lattice. We investigate the antinomies of Russell, Cantor, Burali-Forti, and others, and discuss the relationship of the system to other set-theoretic (...) systems ZF, NBG, and NF. We discuss two methods of axiomatizing higher order quantification and abstraction, and then very briefly discuss the application of one of these methods to areas of mathematics outside of logic. (shrink)

John Burgess in a 2004 paper combined plural logic and a new version of the idea of limitation of size to give an elegant motivation of the axioms of ZFC set theory. His proposal is meant to improve on earlier work by Paul Bernays in two ways. I argue that both attempted improvements fail. I am grateful to Philip Welch, two anonymous referees, and especially Ignacio Jané for written comments on earlier versions of this paper, which have led to (...) substantial improvements. Thanks also to the participants in a discussion group at the University of Bristol, where an earlier version was presented. (shrink)

The focus in this essay will be upon the paradoxes, and foremostly in set theory. A central result is that the librationist set theory £ extension \Pfund $\mathscr{HR}(\mathbf{D})$ of \pounds \ accounts for \textbf{Neumann-Bernays-Gödel} set theory with the \textbf{Axiom of Choice} and \textbf{Tarski's Axiom}. Moreover, \Pfund \ succeeds with defining an impredicative manifestation set $\mathbf{W}$, \emph{die Welt}, so that \Pfund$\mathscr{H}(\mathbf{W})$ %is a model accounts for Quine's \textbf{New Foundations}. Nevertheless, the points of view developed support the view that (...) the truth-paradoxes and the set-paradoxes have common origins, so that the librationist resolutions of the set theoretic paradoxes are at the same time resolutions of the truth theoretic paradoxes. Both the librationist resolutions of the set theoretic paradoxes and the truth theoretic paradoxes have non-trivial philosophical implications: librationist set theories have the consequence that there are no absolutely uncountable sets, and librationist truth theories allow the use of syntactical modalities in ways which circumvent limitations as those of \parencite{Montague1963}, and a truth predicate which is useful for more precise philosophical discourse. (shrink)

In this paper, we study when a set-continuous operator has a fixed-point that is the intersection of a directed family. The framework of our study is the Kelley-Morse theory KMC– and the Gödel-Bernays theory GBC–, both theories including an Axiom of Choice and excluding the Axiom of Foundation. On the one hand, we prove a result concerning monotone operators in KMC– that cannot be proved in GBC–. On the other hand, we study conditions on directed superclasses in GBC– (...) in order that their intersection is a fixed-point of a set-continuous operator. Finally, we illustrate our results with a solution to the liar paradox and a construction of maximal bisimulations. (shrink)

This accessible book gives a new, detailed and elementary explanation of the Gödel incompleteness theorems and presents the Chaitin results and their relation to the da Costa-Doria results, which are given in full, but with no ...

In spite of differences the thought of Bernays, Dooyeweerd and Gödel evinces a remarkable convergence. This is particularly the case in respect of the acknowledgement of the difference between the discrete and the continuous, the foundational position of number and the fact that the idea of continuity is derived from space (geometry – Bernays). What is furthermore similar is the recognition of what is primitive (and indefinable) as well as the account of the coherence of what is unique, such as (...) when Gödel observes something quasi-spatial character of sets. It is shown that Dooyeweerd’s theory of modal aspects provides a philosophical framework that exceeds his own restrictive understanding of infinity )to the potential infinite) and at the same time makes it possible to account for key insights found in the thought of Bernays and Gödel. When Laugwitz says that discreteness rules within the sphere of the numerical, he says nothing more than what Dooyeweerd had in mind with his idea that discrete quantity, as the meaning-nucleus of the arithmetical aspect, qualifies every element within the structure of the quantitative aspect. And when Bernays says that analysis expresses the idea of the continuum in arithmetical language his mode of speech is equivalent to saying that mathematical analysis could seen as being founded upon the spatial anticipation within the modal structure of the arithmetical aspect. The view of the actual infinite (the at once infinite) in terms of an “as if” approach (Bernays), that is, as appreciated as a regulative hypothesis through which every successively infinite multiplicity of numbers could be envisaged as being giving all at once, as an infinite totality, provides a sound understanding of the at once infinite and makes it plain why every form of arithmeticism fails. Such attempts have to call upon Cantor’s proof on the non-denumerability of the real numbers – and this proof pre-supposes the use of the at once infinite which, in turn, pre-supposes the (irreducibile) spatial order of simultaneity and the patial whole-parts relation. (shrink)

Bernays' idea of the power-set is neither univocal nor ambiguous. according to its domain of application it has a different mathematical meaning in spite of its identical logical definition. in his last axiomatisation of set-theory bernays' introduced a very powerful axiom stating that every property of the universe of all sets is mirrored by some set. this is a most peculiar application of the general--philosophical and theological--principle of analogy as a key principle in the foundations of mathematics.

Let Q be an equivalence relation whose equivalence classes, denoted Q[x], may be proper classes. A function L defined on Field(Q) is a labelling for Q if and only if for all x,L(x) is a set and L is a labelling by subsets for Q if and only if BG denotes Bernays-Gödel class-set theory with neither the axiom of foundation, AF, nor the class axiom of choice, E. The following are relatively consistent with BG. (1) E is true but (...) there is an equivalence relation with no labelling.(2) E is true and every equivalence relation has a labelling, but there is an equivalence relation with no labelling by subsets. (shrink)

The class forcing theorem, which asserts that every class forcing notion ${\mathbb {P}}$ admits a forcing relation $\Vdash _{\mathbb {P}}$, that is, a relation satisfying the forcing relation recursion—it follows that statements true in the corresponding forcing extensions are forced and forced statements are true—is equivalent over Gödel–Bernays set theory $\text {GBC}$ to the principle of elementary transfinite recursion $\text {ETR}_{\text {Ord}}$ for class recursions of length $\text {Ord}$. It is also equivalent to the existence of truth predicates for (...) the infinitary languages $\mathcal {L}_{\text {Ord},\omega }$, allowing any class parameter A; to the existence of truth predicates for the language $\mathcal {L}_{\text {Ord},\text {Ord}}$ ; to the existence of $\text {Ord}$ -iterated truth predicates for first-order set theory $\mathcal {L}_{\omega,\omega }$ ; to the assertion that every separative class partial order ${\mathbb {P}}$ has a set-complete class Boolean completion; to a class-join separation principle; and to the principle of determinacy for clopen class games of rank at most $\text {Ord}+1$. Unlike set forcing, if every class forcing notion ${\mathbb {P}}$ has a forcing relation merely for atomic formulas, then every such ${\mathbb {P}}$ has a uniform forcing relation applicable simultaneously to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between $\text {GBC}$ and Kelley–Morse set theory $\text {KM}$. (shrink)

PA is Peano arithmetic. The formula $\operatorname{Interp}_\mathrm{PA}(\alpha, \beta)$ is a formalization of the assertion that the theory PA + α interprets the theory PA + β (the variables α and β are intended to range over codes of sentences of PA). We extend Solovay's modal analysis of the formalized provability predicate of PA, Pr PA (x), to the case of the formalized interpretability relation $\operatorname{Interp}_\mathrm{PA}(x, y)$ . The relevant modal logic, in addition to the usual provability operator `□', (...) has a binary operator ` $\triangleright$ ' to be interpreted as the formalized interpretability relation. We give an axiomatization and a decision procedure for the class of those modal formulas that express valid interpretability principles (for every assignment of the atomic modal formulas to sentences of PA). Our results continue to hold if we replace the base theory PA with Zermelo-Fraenkel set theory, but not with Gödel-Bernays set theory. This sensitivity to the base theory shows that the language is quite expressive. Our proof uses in an essential way earlier work done by A. Visser, D. de Jongh, and F. Veltman on this problem. (shrink)

A modal theory Z using the Guaspari witness comparison signs $\leq, is developed. The theory Z is similar to, but weaker than, the theory R of Guaspari and Solovay. Nevertheless, Z proves the independence of the Rosser fixed-point. A Kripke semantics for Z is presented and some arithmetical interpretations of Z are investigated. Then Z is enriched to ZI by adding a new modality sign for interpretability and by axioms expressing some facts about interpretability of theories. Two (...) arithmetical interpretations of ZI are presented. The proofs of the validity of the axioms of ZI in arithmetical interpretations use some strengthening of Solovay's result about interpretability in Godel-Bernays set theory. (shrink)

The interpretability logic ILP is the interpretability logic of all sufficiently strong |$\varSigma _1$|-sound finitely axiomatised theories, such as the Gödel-Bernays set theory. The interpretability logic IL is a strict subset of the intersection of the interpretability logics of all so-called reasonable theories, IL(All). It is known that both ILP and ILW are decidable, however their complexity has not been resolved previously. In [10] it was shown that the basic interpretability logic IL is PSPACE-complete. Here we prove the same (...) for ILP and ILW. (shrink)

Classes are a kind of collection. Typically, they are too large to be sets. For example, there are classes containing absolutely all sets even though there is no set of all sets. But what are classes, if not sets? When our theory of classes is relatively weak, this question can be avoided. In particular, it is well known that von Neuman–Bernays–Godel class theory is conservative over the standard axioms of set theory ): anything NGB can prove about (...) the sets is already provable in ZFC. In this paper I will prove a new conservativity result for a much broader range of class theories. It tells us that as long as our set theory T contains an independently well-motivated reflection principle, anything provable about the sets in any reasonable class theory extending T is already provable in T. (shrink)

This paper explores the relationship borne by the traditional paradoxes of set theory and semantics to formal incompleteness phenomena. A central tool is the application of the Arithmetized Completeness Theorem to systems of second-order arithmetic and set theory in which various “paradoxical notions” for first-order languages can be formalized. I will first discuss the setting in which this result was originally presented by Hilbert & Bernays (1939) and also how it was later adapted by Kreisel (1950) and Wang (...) (1955) in order to obtain formal undecidability results. A generalization of this method will then be presented whereby Russell’s paradox, a variant of Mirimanoff’s paradox, the Liar, and the Grelling–Nelson paradox may be uniformly transformed into incompleteness theorems. Some additional observations are then framed relating these results to the unification of the set theoretic and semantic paradoxes, the intensionality of arithmetization (in the sense of Feferman, 1960), and axiomatic theories of truth. (shrink)

Let T be Kripke–Platek set theory with infinity extended by the axiom (Beta) plus the schema that claims that every set-bounded Σ-definable monotone operator from the collection of all sets to Pow(a) for some set a has a fixed point. Then T proves that every such operator has a least fixed point. This result is obtained by following the proof of an analogous result for von Neumann–Bernays–Gödel set theory in an earlier work by Sato, with some minor modifications.