Users' Mathboxes Mathbox for Wolf Lammen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax-wl-8cl Structured version   Visualization version   GIF version

Axiom ax-wl-8cl 33804
Description: In ZFC, as presented in this document, classes are meant to be just a notational convenience, that can be reduced to pure set theory by means of df-clab 2752 (there stated in the eliminable property). That is, in an expression 𝑥𝐴, the class variable 𝐴 is implicitely assumed to represent an expression {𝑧𝜑} with some appropriate 𝜑. Unfortunately, 𝜑 syntactically covers any well-formed formula (wff), including 𝑧𝐴. This choice inevitably breaks the stated property. And it potentially carries over to any expression containing class variables. To fix this, a simple rule could exclude class variables at all in a class defining wff. A more elaborate rule could detect, and limit exclusion to proper classes (potentially problematic). In any case, the verification process should enforce any such rule during replacement, which it currently does not. The result is that we rely on the awareness of theorem designers to this problem. It seems, in ZFC proper classes are reduced to a few instances only, so a careful study may reveal that this limited use does not impose logical loop holes. It must be said, still, this necessary extra knowledge contradicts the general philosophy of Metamath, trying to establish certainty by a machine executable confirmation.

An extension to ZFC allows classes to exist on their own. Classes are then extensions to sets, also seamlessly extending the idea of elementhood. In order to move from the general to the specific, sets presuppose classes, so classes should be introduced first. This is somewhat in opposition to the classic order of introduction of syntactic elements, but has been carried out in the past, for example by the von-Neumann theory of classes.

In the context of Metamath, which is a purely text-based syntactical concept, no semantics are imposed at the very beginning on classes. Instead axioms will narrow down bit by bit how elementhood behaves in proofs, of course always with the intuitive understanding of a human in mind.

One basic property of elementhood we expect is that the 'element' is replaceable with something equal to it. Or that equality is finer grained than the elementhood relation. This idea is formally expressed in terms coined 'implicit substitution' in this document: ((𝑥 = 𝑦) → (𝑥𝐴𝑦𝐴)). This axiom prepares this notation.

Note that particular constructions of classes like that in df-clab 2752 in fact allow to prove this axiom. Can we expect to eliminate this axiom then? No, the generalizing term still refers to an unexplained subterm 𝑥𝐴, so this axiom recurs in the general case. On the other hand, our axiom here stays true, even when just the existence of a class is known, as is often the case after applying the axiom of choice, without a chance to actually construct it.

We provide a version of this axiom, that requires all variables to be distinct. Step by step these restrictions are lifted, in the end covering the most general term 𝐴𝐵.

This axiom is meant as a replacement for ax-8 2157. (Contributed by Wolf Lammen, 27-Nov-2021.)

Assertion
Ref Expression
ax-wl-8cl (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
Distinct variable group:   𝑥,𝑦,𝐴

Detailed syntax breakdown of Axiom ax-wl-8cl
StepHypRef Expression
1 vx . . 3 setvar 𝑥
2 vy . . 3 setvar 𝑦
31, 2weq 2056 . 2 wff 𝑥 = 𝑦
4 cA . . . 4 class 𝐴
51, 4wcel-wl 33800 . . 3 wff 𝑥𝐴
62, 4wcel-wl 33800 . . 3 wff 𝑦𝐴
75, 6wi 4 . 2 wff (𝑥𝐴𝑦𝐴)
83, 7wi 4 1 wff (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
Colors of variables: wff setvar class
This axiom is referenced by:  wl-ax8clv1  33805  wl-clelv2-just  33806
  Copyright terms: Public domain W3C validator