ZFC Axioms Without Distinct Variable Conditions - 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 (and corresponds to its $d restriction in the database source file, set.mm).

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 imagine a fixed assignment of individual variables to our set metavariables, outside of Metamath. 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 a theorem is not affected by renaming its variables as long as the variables 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 a simple additional scheme, which we have called the Axiom of Twoness, that does have a proviso and will be discussed below.

ZFC Axioms Without Distinct Variable Conditions (browser note: large proofs, up to 300K)

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 Union with no distinct variable conditions	|- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)
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 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))
Axiom of Twoness	|- -. A.x x = y, where x and y are distinct variables.

To prove that they are really 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 much easier 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 do provide interesting exercises that stress a student's understanding of free and bound variables.

Nonetheless, I think it is remarkable that the need for distinct variables in the axiom schemes for (essentially) all of mathematics can be distilled down to a single simple axiom scheme, which I call the "Axiom of Twoness," that in essence asserts merely that at least two things exist.

Axiom of Twoness    The Axiom of Twoness implies the Axiom of Distinct Variables ax-16 and makes that axiom redundant (as shown by theorem ax16b). We could, if we wish, consider the Axiom of Twoness to be an axiom of a somewhat stronger and less general predicate calculus, where the domain of discourse is assumed to contain at least two objects, in place of the usual assumption that at least one object exists. (Even this latter 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, I have been able to rederive all of the other axioms 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, we can postpone the application of the Axiom of Twoness until the very end of the proof, using it to trim off redundant distinctors (i.e. those containing dummy variables) in a trivial algorithmic way. If we view this as just a postprocessing clean-up "outside" of the proof for the benefit of readability, it means that in principle the no distinct variables at all are needed for mathematics. (However, from a practical point of view, the explicit manipulation of distinctors is tedious and results in long proofs, so such a system is mostly only of theoretical interest.)

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.