Mathbox for Wolf Lammen |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax-wl-8cl | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ax-wl-8cl | ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 setvar 𝑥 | |
2 | vy | . . 3 setvar 𝑦 | |
3 | 1, 2 | weq 2056 | . 2 wff 𝑥 = 𝑦 |
4 | cA | . . . 4 class 𝐴 | |
5 | 1, 4 | wcel-wl 33800 | . . 3 wff 𝑥 ∈ 𝐴 |
6 | 2, 4 | wcel-wl 33800 | . . 3 wff 𝑦 ∈ 𝐴 |
7 | 5, 6 | wi 4 | . 2 wff (𝑥 ∈ 𝐴 → 𝑦 ∈ 𝐴) |
8 | 3, 7 | wi 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 |