Metamath Proof Explorer - ZFC Axioms Without Distinct Variable Conditions

ZFC Axioms Without Distinct Variable Conditions

ZFC Axioms Without Distinct Variable Conditions   The standard ZFC axioms are stated with a requirement that all of their set variables be distinct. An interesting exercise is to use various logic tricks to formulate an equivalent set of axioms that require that no variables be distinct. Here we show such a set, proved as theorems from the standard axioms, along with a simple additional axiom that does require distinct variables. To prove that they are really equivalent, we also re-derive the standard axioms 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.

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

Ref	Expression
Conditionless Axiom of Extensionality	|- E.x((x e. y <-> x e. z) -> y = z)
Conditionless Axiom of Replacement	|- E.x(E.yA.z(ph -> z = y) -> A.z(A.y z e. x <-> E.x(A.z x e. y /\ A.yph)))
Conditionless Axiom of Union	|- E.xA.y(E.x(y e. x /\ x e. z) -> y e. x)
Conditionless Axiom of Power Sets	|- (-. x = y -> E.xA.y(A.x(E.z x e. y -> A.y x e. z) -> y e. x))
Conditionless Axiom of Regularity	|- (x e. y -> E.x(x e. y /\ A.z(z e. x -> -. z e. y)))
Conditionless Axiom of Infinity	|- E.x(y e. z -> (y e. x /\ A.y(y e. x -> E.z(y e. z /\ z e. x))))
Conditionless Axiom of Choice	|- 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.

Colors of variables: wff set class

Most mathematicians are used to free and bound variables being intrinsically distinct (which they are in the actual axioms of logic - see Note on the Axioms), and this version may make some of them grimace, which is why I did'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.

The Axiom of Twoness implies the Axiom of Distinct Variables ax-16 and makes that axiom redundant. (Proof: plug it into pm2.21i.) 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.)

The Axiom of Twoness appears to be essential for completeness, although I unfortunately I haven't been able to find a proof. Specifically, it seems to be needed to rederive the standard Axiom of Power Sets from our conditionless version. I don't think it is possible to state a conditionless version of the Axiom of Power Sets from which the standard version can be derived without also invoking the Axiom of Twoness.

Is there any way to avoid the Axiom of Twoness? Yes, provided that we are willing to live with theorems prefixed with antecedents of the form "-. A.x x = y", which we dub "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 though those variables may not be part of the theorem itself. It is theoretically impossible to avoid dummy variables, which was proved by a theorem of Andréka and is discussed in the 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 and then get rid of the distinctors with dummy variables in them 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. The body of any such proof can be verified with a simple, fast algorithm called "condensed detachment" (described in the paper), which is ordinarily limited to propositional calculus.

Although these 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 as a study of axiomatics (what theorems depend on what axioms), these conditionless axioms are not always suitable.

This page was last updated on 27-Dec-2004.

metamath.org