Metamath Proof Explorer Home Metamath Proof Explorer
ZFC Axioms Without Distinct Variable Conditions
Mirrors  >  Home  >  MPE Home  >  ZFC Axioms Without Distinct Variable Conditions
HomeHome Metamath Proof Explorer  
ZFC Axioms Without Distinct Variable Conditions

On the variables in the ZFC axioms   Each of our standard ZFC (Zermelo-Fraenkel with Choice) set theory axioms is accompanied by the proviso that all of its set variables be distinct from each other. This is indicated by the "Distinct variable group" on its web page (for example ax-ext) and corresponds to its $d restriction in the database source file,

Each "axiom" in Metamath's version of ZFC set theory is not an actual axiom in the language of first-order logic but is a scheme or template that represents an infinite number of actual axioms. From the point of view of first-order logic, the set and wff "variables" are metavariables that range over the individual variables and wffs of the language of the actual logic. This is the way Metamath—"metavariable math"—works; it doesn't have a way of directly representing an individual variable or a single actual axiom.

Most textbooks, on the other hand, state the ZFC axioms (except Replacement, which necessarily has a wff metavariable) as specific actual axioms in the language of first-order logic. So, for example, they will state the Axiom of Extensionality as a single actual axiom with fixed individual variables, not a scheme ranging over an infinite number of actual axioms. To recover the textbook version from Metamath's version, we simply make a fixed assignment of individual variables to our set metavariables, outside of Metamath; in other words, we pick any instance of the scheme that our Axiom of Extensionality statement represents. The math works out exactly the same, because we have attached provisos to our standard version of the ZFC axioms stating that their set metavariables must be distinct from each other, and a metatheorem of predicate calculus states that the truth of an axiom is not affected by renaming its variables as long as the variable names remain distinct.

ZFC axioms without distinct variable conditions   It is possible to exploit the fact that we are using metavariables instead of individual variables in the following interesting way. We can use various logic tricks to formulate an equivalent set of ZFC axiom schemes that have no distinct variable provisos. Here we show such a set, proved as theorems from the standard ones. Accompanying them is an optional simple additional scheme, which we have called the Axiom of Twoness, that does have a proviso and will be discussed below.

The axioms below can be added to a predicate calculus system with no distinct variables to obtain a logically complete set of axioms for logic and set theory.

ZFC Axioms Without Distinct Variable Conditions
Ref Expression
Axiom of Extensionality with no distinct variable conditions |- E.x((x e. y <-> x e. z) -> y = z)
Axiom of Replacement with no distinct variable conditions |- E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
Axiom of Power Sets with no distinct variable conditions |- (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x))
Axiom of Union with no distinct variable conditions |- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)
Axiom of Regularity with no distinct variable conditions |- (x e. y -> E.x(x e. y /\ A.z(z e. x -> -. z e. y)))
Axiom of Infinity with no distinct variable conditions |- E.x(y e. z -> (y e. x /\ A.y(y e. x -> E.z(y e. z /\ z e. x))))
Axiom of Choice with no distinct variable conditions |- E.xA.yA.z(A.x(y e. z /\ z e. w) -> E.wA.y(E.w((y e. z /\ z e. w) /\ (y e. w /\ w e. x)) <-> y = w))
(Optional; see below) Axiom of Twoness |- -. A.x x = y, where x and y are distinct variables.
Colors of variables: wff set class

To prove that they really are equivalent, we also rederive the standard ones from them: rederivation of Extensionality, rederivation of Replacement, rederivation of Union, rederivation of Power Sets, rederivation of Regularity, rederivation of Infinity, and rederivation of Choice.

Remarks    In an axiom scheme with no distinct variable restrictions, the complicated rules for free variables and proper substitution, needed to avoid distinct variable clashes, disappear. A quantified ("bound") variable loses its special status, and the concept of a quantified variable's scope vanishes—all variables become "global" throughout the expression. Think about what that means—it is a rather startling and even counterintuitive property if you are used to working with first-order logic. For example, in our condition-free Axiom of Union, we can blindly change all of its free and bound set variables to x, and the strange-looking result, |- E.xA.x(E.x(x e. x /\ x e. x) -> x e. x), is still a sound (although probably not very useful) theorem scheme of set theory! Among other things, such axiom schemes are trivial to manipulate with a computer program, since the "for all" and "there exists" quantifiers effectively become simple binary operations.

Most mathematicians are used to free and bound variables being intrinsically distinct (which they are in the actual axioms of logic—again, see the note on the axioms), and this version may make some of them grimace, which is why I didn't put them on the main Metamath Proof Explorer page. Certainly they are more difficult to grasp intuitively, and I would not advocate using them as the starting point for a set theory course, although they might provide interesting exercises that stress a student's understanding of free and bound variables.

Axiom of Twoness    The axiom above that I have dubbed the "Axiom of Twoness" in essence asserts merely that at least two things exist. When added to the axioms of our predicate calculus system with no distinct variables, the Axiom of Twoness implies ax-16 (as shown by theorem ax16b) and therefore all instances of ax-17, making those two axioms of predicate calculus unnecessary for logical completeness. This means that the need for distinct variables in mathematics completely captured by the Axiom of Twoness, a fact that I think is somewhat remarkable.

One way to look at the Axiom of Twoness is not as axiom of set theory but as an axiom of a somewhat stronger and less general predicate calculus, where the domain of discourse is assumed to contain at least two objects. (The ordinary assumption in predicate calculus is that at least one object exists. Even this assumption is somewhat arbitrary and made for convenience in standard predicate calculus. There are more complex versions of predicate calculus called "free logics" that allow the domain of discourse to be empty.)

My conjecture is that the Axiom of Twoness, and not just the weaker Axiom of Distinct Variables ax-16, is necessary for completeness. Specifically, I haven't been able to rederive the standard Axiom of Power Sets from our condition-free version without invoking the Axiom of Twoness, nor have I been able to find any other condition-free version of Power Sets that would let me do this. (On the other hand, as you can see from the rederivation proofs, all of the other axioms can be derived from their condition-free versions without invoking the Axiom of Twoness! There seems to be something special about the Axiom of Power Sets that the other axioms don't have.)

Distinctors    Is there any way to avoid the Axiom of Twoness, or more generally any need for distinct variable provisos at all? Yes and yes, provided that we are willing to live with theorems prefixed with antecedents of the form "-. A.x x = y", which I call "distinctors," in place of explicitly requiring x and y to be distinct variables. But the list of distinctors needed for a theorem can grow quite long, as it will accumulate all the "dummy" variables used in the theorem's proof, even if those variables do not appear in the main part of the theorem. It is theoretically impossible to avoid dummy variables, which was proved by a theorem of Andréka and is discussed in my paper, "A Finitely Axiomatized Formalization of Predicate Calculus with Equality."

Nonetheless, for informal display purpose we could drop the distinctors having dummy variables not occurring in the theorem. For more precise communication, we could abbreviate the list of distinctors for dummy variables with a notation such "d(7)", meaning that distinctors for 7 dummy variables are implicit in the antecedent. In this way, we could derive essentially all of mathematics from a system having no distinct variable requirements, without an excessive notational burden for the accumulation of distinctors.

Interdependence    Although these condition-free axioms are provably equivalent as a group to the standard ZFC axioms, it should be noted that there is a sense in which they are not "pure" individually. At the end of their proofs, in the list of axioms used, you can see that some of them involve the use of set theory axioms other than the ones they correspond to. For example, one of the tricks we use is the fact that A.x y e. z evaluates to y e. z if all three variables are distinct, and false otherwise. To prove this we need the Axiom of Regularity, so that any axiom using this trick incorporates a component derived from Regularity. So for some purposes, such studying the independence of the standard ZFC axioms, they are not suitable as a replacement for the standard ones.

  This page was last updated on 4-Jun-2009.
Copyright terms: Public domain
W3C HTML validation [external]