ZFC Axioms Without Distinct Variable Conditions - Metamath Proof Explorer

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 setvar 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, 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 setvar 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 setvar 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 setvar 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	⊢ ∃𝑥((𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧) → 𝑦 = 𝑧)
Axiom of Replacement with no distinct variable conditions	⊢ ∃𝑥(∃𝑦∀𝑧(𝜑 → 𝑧 = 𝑦) → ∀𝑧(∀𝑦𝑧 ∈ 𝑥 ↔ ∃𝑥(∀𝑧𝑥 ∈ 𝑦 ∧ ∀𝑦𝜑)))
Axiom of Power Sets with no distinct variable conditions	⊢ (¬ 𝑥 = 𝑦 → ∃𝑥∀𝑦(∀𝑥(∃𝑧𝑥 ∈ 𝑦 → ∀𝑦𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥))
Axiom of Union with no distinct variable conditions	⊢ ∃𝑥∀𝑦(∃𝑥(𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑥)
Axiom of Regularity with no distinct variable conditions	⊢ (𝑥 ∈ 𝑦 → ∃𝑥(𝑥 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑥 → ¬ 𝑧 ∈ 𝑦)))
Axiom of Infinity with no distinct variable conditions	⊢ ∃𝑥(𝑦 ∈ 𝑧 → (𝑦 ∈ 𝑥 ∧ ∀𝑦(𝑦 ∈ 𝑥 → ∃𝑧(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑥))))
Axiom of Choice with no distinct variable conditions	⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
(Optional; see below) Axiom of Twoness	⊢ ¬ ∀𝑥𝑥 = 𝑦, where 𝑥 and 𝑦 are distinct variables.

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 setvar variables to 𝑥, and the strange-looking result, ⊢ ∃𝑥∀𝑥(∃𝑥(𝑥 ∈ 𝑥 ∧ 𝑥 ∈ 𝑥) → 𝑥 ∈ 𝑥), 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-c16 (as shown by theorem axc16b) and therefore all instances of ax-5, making those two axioms of predicate calculus unnecessary for logical completeness. This means that the need for distinct variables in mathematics is 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-c16, is necessary for completeness. Specifically, I haven't been able to rederive the standard Axiom of Power Sets (nor the standard Axiom of Infinity, which uses it for its rederivation) 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.

Update 11-Apr-2018: Benoît Jubin has shown that the Axiom of Twoness is necessary to rederive the standard axioms of Power Sets and Infinity. See item 14 on the "Open problems and miscellany" page.

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 "¬ ∀𝑥𝑥 = 𝑦", which I call "distinctors," in place of explicitly requiring 𝑥 and 𝑦 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 ∀𝑥𝑦 ∈ 𝑧 evaluates to 𝑦 ∈ 𝑧 if all three variables are mutually 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 as studying the independence of the standard ZFC axioms, they are not suitable as a replacement for the standard ones.