S is an axiomatic set theory set out by George Boolos in his 1989 article, "Iteration Again". S, a first-order theory, is two-sorted because its ontology includes "stages" as well as sets. Boolos designed S to embody his understanding of the "iterative conception of set" and the associated iterative hierarchy. S has the important property that all axioms of Zermelo set theory Z, except the axiom of extensionality and the axiom of choice, are theorems of S or a slight modification thereof.
Any grouping together of mathematical, abstract, or concrete objects, however formed, is a collection, a synonym for what other set theories refer to as a class. The things that make up a collection are called elements or members. A common instance of a collection is the domain of discourse of a first-order theory.
All sets are collections, but there are collections that are not sets. A synonym for collections that are not sets is proper class. An essential task of axiomatic set theory is to distinguish sets from proper classes, if only because mathematics is grounded in sets, with proper classes relegated to a purely descriptive role.
The Von Neumann universe implements the "iterative conception of set" by stratifying the universe of sets into a series of "stages", with the sets at a given stage being possible members of the sets formed at all higher stages. The notion of stage goes as follows. Each stage is assigned an ordinal number. The lowest stage, stage 0, consists of all entities having no members. We assume that the only entity at stage 0 is the empty set, although this stage would include any urelements we would choose to admit. Stage n, n>0, consists of all possible sets formed from elements to be found in any stage whose number is less than n. Every set formed at stage n can also be formed at every stage greater than n. [1]
Hence the stages form a nested and well-ordered sequence, and would form a hierarchy if set membership were transitive. The iterative conception has gradually become more accepted, despite an imperfect understanding of its historical origins.
The iterative conception of set steers clear, in a well-motivated way, of the well-known paradoxes of Russell, Burali-Forti, and Cantor. These paradoxes all result from the unrestricted use of the principle of comprehension of naive set theory. Collections such as "the class of all sets" or "the class of all ordinals" include sets from all stages of the iterative hierarchy. Hence such collections cannot be formed at any given stage, and thus cannot be sets.
This section follows Boolos (1998: 91). The variables x and y range over sets, while r, s, and t range over stages. There are three primitive two-place predicates:
The axioms below include a defined two-place set-stage predicate, Bxr, which abbreviates:
Bxr is read as "set x is formed before stage r".
Identity, denoted by infix '=', does not play the role in S it plays in other set theories, and Boolos does not make fully explicit whether the background logic includes identity. S has no axiom of extensionality and identity is absent from the other S axioms. Identity does appear in the axiom schema distinguishing S+ from S, [2] and in the derivation in S of the pairing, null set, and infinity axioms of Z . [3]
The symbolic axioms shown below are from Boolos (1998: 91), and govern how sets and stages behave and interact. The natural language versions of the axioms are intended to aid the intuition.
The axioms come in two groups of three. The first group consists of axioms pertaining solely to stages and the stage-stage relation ‘<’.
Tra:
"Earlier than" is transitive.
Net:
A consequence of Net is that every stage is earlier than some stage.
Inf:
The sole purpose of Inf is to enable deriving in S the axiom of infinity of other set theories.
The second and final group of axioms involve both sets and stages, and the predicates other than '<':
All:
Every set is formed at some stage in the hierarchy.
When:
A set is formed at some stage if and only if its members are formed at earlier stages.
Let A(y) be a formula of S where y is free but x is not. Then the following axiom schema holds:
Spec:
If there exists a stage r such that all sets satisfying A(y) are formed at a stage earlier than r, then there exists a set x whose members are just those sets satisfying A(y). The role of Spec in S is analogous to that of the axiom schema of specification of Z.
Boolos’s name for Zermelo set theory minus extensionality was Z-. Boolos derived in S all axioms of Z- except the axiom of choice. [4] The purpose of this exercise was to show how most of conventional set theory can be derived from the iterative conception of set, assumed embodied in S. Extensionality does not follow from the iterative conception, and so is not a theorem of S. However, S + Extensionality is free of contradiction if S is free of contradiction.
Boolos then altered Spec to obtain a variant of S he called S+, such that the axiom schema of replacement is derivable in S+ + Extensionality. Hence S+ + Extensionality has the power of ZF. Boolos also argued that the axiom of choice does not follow from the iterative conception, but did not address whether Choice could be added to S in some way. [5] Hence S+ + Extensionality cannot prove those theorems of the conventional set theory ZFC whose proofs require Choice.
Inf guarantees the existence of stages ω, and of ω + n for finite n, but not of stage ω + ω. Nevertheless, S yields enough of Cantor's paradise to ground almost all of contemporary mathematics. [6]
Boolos compares S at some length to a variant of the system of Frege’s Grundgesetze, in which Hume's principle, taken as an axiom, replaces Frege’s Basic Law V, an unrestricted comprehension axiom which made Frege's system inconsistent; see Russell's paradox.
In mathematics, the axiom of regularity is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set A contains an element that is disjoint from A. In first-order logic, the axiom reads:
First-order logic—also called predicate logic, predicate calculus, quantificational logic—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables over non-logical objects, and allows the use of sentences that contain variables. Rather than propositions such as "all men are mortal", in first-order logic one can have expressions in the form "for all x, if x is a man, then x is mortal"; where "for all x" is a quantifier, x is a variable, and "... is a man" and "... is mortal" are predicates. This distinguishes it from propositional logic, which does not use quantifiers or relations; in this sense, propositional logic is the foundation of first-order logic.
In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of pairing is one of the axioms of Zermelo–Fraenkel set theory. It was introduced by Zermelo (1908) as a special case of his axiom of elementary sets.
In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite sets in ZF.
In axiomatic set theory, the axiom of union is one of the axioms of Zermelo–Fraenkel set theory. This axiom was introduced by Ernst Zermelo.
In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as Russell's paradox. Today, Zermelo–Fraenkel set theory, with the historically controversial axiom of choice (AC) included, is the standard form of axiomatic set theory and as such is the most common foundation of mathematics. Zermelo–Fraenkel set theory with the axiom of choice included is abbreviated ZFC, where C stands for "choice", and ZF refers to the axioms of Zermelo–Fraenkel set theory with the axiom of choice excluded.
In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing the natural numbers. It was first published by Ernst Zermelo as part of his set theory in 1908.
In mathematical logic, New Foundations (NF) is a non-well-founded, finitely axiomatizable set theory conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica.
The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement-free) Kripke–Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The purpose of allowing urelements is to allow large or high-complexity objects to be included in the theory's transitive models without disrupting the usual well-ordering and recursion-theoretic properties of the constructible universe; KP is so weak that this is hard to do by traditional means.
In set theory, -induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction.
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by Raphael M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is weaker than PA but it has the same language, and both theories are incomplete. Q is important and interesting because it is a finitely axiomatized fragment of PA that is recursively incompletable and essentially undecidable.
In the foundations of mathematics, Morse–Kelley set theory (MK), Kelley–Morse set theory (KM), Morse–Tarski set theory (MT), Quine–Morse set theory (QM) or the system of Quine and Morse is a first-order axiomatic set theory that is closely related to von Neumann–Bernays–Gödel set theory (NBG). While von Neumann–Bernays–Gödel set theory restricts the bound variables in the schematic formula appearing in the axiom schema of Class Comprehension to range over sets alone, Morse–Kelley set theory allows these bound variables to range over proper classes as well as sets, as first suggested by Quine in 1940 for his system ML.
In set theory, a branch of mathematics, a reflection principle says that it is possible to find sets that, with respect to any given property, resemble the class of all sets. There are several different forms of the reflection principle depending on exactly what is meant by "resemble". Weak forms of the reflection principle are theorems of ZF set theory due to Montague (1961), while stronger forms can be new and very powerful axioms for set theory.
In mathematical logic, second-order arithmetic is a collection of axiomatic systems that formalize the natural numbers and their subsets. It is an alternative to axiomatic set theory as a foundation for much, but not all, of mathematics.
Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "" and "" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.
An approach to the foundations of mathematics that is of relatively recent origin, Scott–Potter set theory is a collection of nested axiomatic set theories set out by the philosopher Michael Potter, building on earlier work by the mathematician Dana Scott and the philosopher George Boolos.
General set theory (GST) is George Boolos's (1998) name for a fragment of the axiomatic set theory Z. GST is sufficient for all mathematics not requiring infinite sets, and is the weakest known set theory whose theorems include the Peano axioms.
In mathematical logic, the ancestral relation of a binary relation R is its transitive closure, however defined in a different way, see below.
The following system is Mendelson's ST type theory. ST is equivalent with Russell's ramified theory plus the Axiom of reducibility. The domain of quantification is partitioned into an ascending hierarchy of types, with all individuals assigned a type. Quantified variables range over only one type; hence the underlying logic is first-order logic. ST is "simple" primarily because all members of the domain and codomain of any relation must be of the same type. There is a lowest type, whose individuals have no members and are members of the second lowest type. Individuals of the lowest type correspond to the urelements of certain set theories. Each type has a next higher type, analogous to the notion of successor in Peano arithmetic. While ST is silent as to whether there is a maximal type, a transfinite number of types poses no difficulty. These facts, reminiscent of the Peano axioms, make it convenient and conventional to assign a natural number to each type, starting with 0 for the lowest type. But type theory does not require a prior definition of the naturals.
Bounded arithmetic is a collective name for a family of weak subtheories of Peano arithmetic. Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates. The main purpose is to characterize one or another class of computational complexity in the sense that a function is provably total if and only if it belongs to a given complexity class. Further, theories of bounded arithmetic present uniform counterparts to standard propositional proof systems such as Frege system and are, in particular, useful for constructing polynomial-size proofs in these systems. The characterization of standard complexity classes and correspondence to propositional proof systems allows to interpret theories of bounded arithmetic as formal systems capturing various levels of feasible reasoning.