Arithmetical hierarchy Created 2026-09-24 Updated 2026-10-14
The arithmetical hierarchy classifies sets by alternating blocks of number quantifiers over computable predicates.
An arithmetic theory is bounded-complete if it proves every true closed formula with only bounded quantifiers. It then proves every true Sigma-1 sentence by choosing a standard witness. If it is also consistent, it cannot prove a false Pi-1 sentence: a standard bounded counterexample supplies a provable contradiction to that universal theorem. This arithmetic condition is distinct from bounded completeness of a statistical model or family.
Bound variable 2026-10-25
A variable occurrence in a first-order formula is bound when it lies in the scope of a quantifier binding that name. The same name can have both bound and free occurrences in one formula. A first-order substitution replaces only free occurrences; a fresh renaming of bound occurrences and their binder preserves the formula up to alpha equivalence.
Class term 2026-10-31
A class term abbreviates a definable collection in first-order set theory. The expression can be eliminated from logical formulas by replacing class in set theory membership with its defining condition. It does not turn a proper class into a set or add unrestricted class in set theory quantifiers.
The underlying set of elements over which the quantifiers of a first-order structure range. Relation symbols are interpreted as finitary relations on this set, and function symbols as functions on it.
Eigenvariable condition 2026-10-25
An eigenvariable condition ensures that a variable chosen as arbitrary or as an existential witness cannot smuggle extra information into a quantifier inference. For the universal quantifier introduction rule, the generalized variable must not occur free in any undischarged assumption. For the existential quantifier elimination rule, the fresh witness must not occur free in the resulting conclusion or in the other undischarged assumptions. Temporary assumptions may contain it if they are discharged before the final inference.
Epsilon-delta definition of continuity Created 2026-10-14 Updated 2026-10-25
A function is continuous at when
First choose the required output tolerance ; then choose an input tolerance that works for every allowed function input in that window. Picking a different separately after seeing each would reverse the quantifiers and lose this guarantee. There is no need to exclude , because the output difference is then zero.
At an isolated point of the domain of a function, choose a small enough window that its only allowed function input is . This proves continuity there directly. At a point with arbitrarily close other inputs, the same definition is the limit of a function condition . For metric spaces, replace the two absolute values by their distance functions; for arbitrary topological spaces, the corresponding definition is a continuous map.
The input tolerance may depend on . A single choice valid everywhere on the domain of a function is the stronger requirement of uniform continuity. The continuous function on shows the difference: for any proposed , the points and have , yet . Thus the fixed output tolerance admits no global input tolerance on the real line.
The cumulative hierarchy is a transitive class even without the ambient Axiom of foundation. If is a nonempty member, choose the least ordinal with . It is a successor . An element of that intersection is a subset of , while has no element in , so . This proves internal Foundation. If the hierarchy also satisfies the other ZF axioms, restricting every quantifier of a finite ZF proof to this definable class translates it into a proof from ZF without foundation. Thus adjoining Foundation preserves consistency relative to the remaining axioms.
Free for substitution 2026-10-25
A first-order term is free for substitution for a variable in a first-order formula when no free variable of becomes bound after replacing a free occurrence of . Equivalently, at every free occurrence to be replaced, none of its enclosing quantifiers binds a variable appearing in . The test depends on occurrences and scopes, not merely on which variable names appear anywhere in the formula.
A Hilbert-style calculus specifies axiom schemes and a small collection of inference rules, typically implication elimination and universal generalization. Equality and quantifier schemes include substitution and free-variable side conditions. Proofs are finite syntactic derivations; validity is separately defined using structures and assignments. A context-sensitive presentation restricts generalization by its actual undischarged assumptions.
Logical formula 2026-10-31
A logical formula is a finite expression constructed by the formation rules of a formal language. Propositional formulas combine propositional variables by logical connectives. First-order formulas additionally contain terms, atomic relations and quantifiers. A logical formula is a syntactic object; its truth is determined only after specifying a suitable interpretation and values for its free variables.
Negation normal form 2026-10-24
A propositional formula or first-order formula is in negation normal form when its negations occur only directly before atomic formulas, and its other logical connectives are conjunction and disjunction, together with quantifiers in the first-order case. Remove implications using , then push negations inward using De Morgan's laws, double-negation cancellation, and
In particular, negating an implication gives , so its antecedent retains its original sign after the outer negation has been pushed through.
The class is transitive because all its levels are transitive. Let be nonempty. There is a least ordinal for which : existence follows by choosing an element of , which lies in , and then minimizing within some witnessing ordinal bound. The least ordinal is neither zero nor a limit, so write . Choose . Then , while minimality gives . Thus . Also , proving Foundation inside .
By the given hypothesis this same class satisfies every axiom of , and hence it satisfies every axiom of . Translate any finite formal proof by restricting each quantifier to the definable class . Within the translated axioms have proofs, logical steps remain valid, and the translated contradiction is still a contradiction. Substituting those axiom proofs therefore converts the original derivation effectively into a finite derivation of contradiction from . Equivalently,
This is the syntactic relative-consistency construction; it does not assume that is a set or that it equals the whole ambient universe.
Fix a logical formula with parameters in , and a set . Suppose satisfies that each has a unique with . Relativize every unbounded quantifier in to the definable class in set theory , obtaining an ambient first-order formula .
Transitivity of ensures that every member of belongs to . The ambient relation
therefore defines a unique ambient set for every . Apply ambient replacement to obtain its range set . By construction every element of belongs to , so part (ii) gives .
Membership in this set is exactly the range relation required by replacement inside the structure . Since the logical formula and parameters were arbitrary, every instance of the replacement scheme holds in the hierarchy class in set theory. The proof uses formula relativization to a class and the closure property from part (ii), not the unsupported assertion that is the whole ambient universe.
In first-order set theory a class in set theory is a definable collection, written schematically using a logical formula and set parameters. A class term is an abbreviation for such a defining condition; it does not add a new kind of object to the quantifiers of ZF. A class in set theory is proper if it is not the collection of elements of any set.
Define the cumulative hierarchy by transfinite recursion:
and let . Without foundation this denotes the well-founded part produced by the hierarchy; it must not simply be assumed to contain every ambient set. Transfinite recursion on ordinals and the relevant set constructions remain available in ZF without foundation.
Prove transitivity by transfinite induction. The empty stage is transitive. Suppose is transitive. Then each member of is a subset of , so . Also is transitive: if , then and, by transitivity of , , so . At a limit stage, a union of transitive sets is transitive. This proves transitivity at every stage.
Finally transitivity of itself implies that every member is a subset of , giving
These successive inclusions and the limit definition also imply whenever . The argument has not used foundation. This leaf includes the unnumbered definitions preceding the source's three claims.
A bounded quantifier has the form or , abbreviating or . A logical formula, also called , is built from atomic membership and equality logical formulas using Boolean connectives and only bounded quantifiers. It has no unbounded quantifier.
For example abbreviates the bounded logical formula . Quantifiers are bounded by an existing variable or parameter, not by an unrestricted class term such as the power set of a parameter unless that set has separately been supplied as a parameter.
A logical formula has the form
up to the standard logical transformations defining the hierarchy. The initial existential quantifiers may be unbounded; all quantifiers inside the matrix are bounded. A finite tuple of witnesses can be encoded by one set if desired, and logical formulas with no initial unbounded quantifier are included as the level-zero special case.
The dual class in set theory has an initial universal block with a bounded matrix. Negation interchanges these two classes, but does not in general preserve the existential class in set theory. Part (iii) supplies an explicit reason for the failure in this setting.
There are two ways for a set to fail to be the power set of : it may contain an object which is not a subset of , or omit a subset of . A single existential logical formula expressing these alternatives is
Its matrix is bounded, so this is . Its negation is precisely the first-order power-set specification
We prove the absoluteness fact needed to exclude a logically equivalent logical formula. If are transitive sets and all parameters lie in , bounded logical formulas have the same truth value in and . Atomic equality and membership agree because both structures use actual membership. Boolean operations preserve agreement. In a bounded quantifier over , transitivity ensures that every element of already lies in , so the two structures quantify over exactly the same elements of . Induction on logical formulas proves the claim. It follows that logical formulas are upward absolute: witnesses in remain available in , and their bounded matrix retains its truth value.
Now use a finite counterexample, so no existence of a transitive model of ZF is assumed. Let , the Finite von Neumann ordinal, and let . These are transitive sets with . Set and , both elements of . Inside , the subsets of which are available as elements of the domain are exactly ; the remaining domain element is not a subset of . Thus satisfies the displayed power-set specification with .
Inside , however, the set is also present and is a subset of , while . Thus the same specification is false in . If were logically equivalent to a logical formula, its truth in would transfer upward to , a contradiction. Therefore
This proves the requested unrestricted logical non-equivalence. The finite structures are not being claimed to satisfy all of ZF; logical equivalence must hold in them as well as in any models of a stronger theory.
Use the strict-order convention appropriate to the membership relation. A bounded logical formula is
The first clause is irreflexivity, the second transitivity, and the third comparability of distinct elements. Irreflexivity and transitivity exclude , so distinct elements cannot be ordered in both directions. These are exactly the axioms of a strict total order on the set , with as its order relation.
Every displayed quantifier is bounded by , so is . The logical formula does not assert that is transitive as a set, and no such additional assertion is needed to say that the restriction of membership to is a total order.