diff --git a/set.mm b/set.mm index 27e8b50251..83080dff02 100644 --- a/set.mm +++ b/set.mm @@ -478810,22 +478810,6 @@ orthogonal vectors (i.e. whose inner product is 0) is the sum of the "ALT=' TosetRel' TITLE='TosetRel'> "; althtmldef "TosetRel" as " TosetRel "; latexdef "TosetRel" as "\mathrm{TosetRel}"; -/* obsolete as of 28-Aug-2018. -NM -htmldef "supw" as - " sup" + - "w "; - althtmldef "supw" as " supw "; - latexdef "supw" as "\mathrm{sup}_\mathrm{w}"; -htmldef "infw" as - " inf" + - "w "; - althtmldef "infw" as " infw "; - latexdef "infw" as "\mathrm{inf}_\mathrm{w}"; -htmldef "LatRel" as - " LatRel"; - althtmldef "LatRel" as "LatRel"; - latexdef "LatRel" as "\mathrm{LatRel}"; -*/ htmldef "DirRel" as " DirRel"; althtmldef "DirRel" as "DirRel"; @@ -598636,8 +598620,8 @@ three theorems are (more or less) independent of each other, which means $(
Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong. This - and the following texts should be read as explorations rather than as - definite statements, open to doubt, alternatives, and reinterpretation. + text should be read as an exploration rather than as definite + statements, open to doubt, alternatives, and reinterpretation.

Grammars and Parsable contents

@@ -598698,8 +598682,66 @@ both sides with predefined tokens (in Metamath: keywords), beginning $(
Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong. This - and the following texts should be read as explorations rather than as - definite statements, open to doubt, alternatives, and reinterpretation. + text should be read as an exploration rather than as definite + statements, open to doubt, alternatives, and reinterpretation. + +

Vocabulary

+ + Sentence:
 + A _sentence_ or _closed form theorem_ is a theorem without any + hypothesis, as opposed to the inference form. Although distinct + variable conditions can be viewed as a particular kind of hypothesis, in + Metamath they are treated as side conditions, and do not affect formal + structure of the theorem. Expressions such as ` F/ x ph ` or the + distinctor ` A. x ( x = y ) ` play a similar role, but appear as + separate hypotheses, or they can simply serve as the first antecedent + in a sentence. + + Bound / Free / Dependent:
 + In formal theories, variables are used to represent + objects, allowing for general statements about relations rather than + individual cases. In Metamath, for example, mathematical objects are + represented by variables of type "setvar". + + An occurrence of such a variable in any formula ` ph ` is said to be + bound. if ` ph ` quantifies that variable, as in ` A. x ph ` . + Variables not bound by a quantifier are called free. Variables of type + "class" are always free, since quantifiers do not apply to them. + + A free variable often indicates a parameter dependency; however, the + formula ` x = x ` shows that this is not necessarily the case. In + Metamath, a variable expressing a real dependency is also called + "effectively free" (see ~ nfequid , with thanks to SN for pointing out + this theorem). + + Instance:
 + A formula of type "class" that is not a mere variable is called an + _instance_ of any "class" type variable. An instance may represent a + single object, or it may still describe a family of objects, when + variables expressing dependencies occur within that formula. + + Attribute:
 + Objects possess properties, some of which may uniquely identify them. + In logic, properties are also known as attributes. They are described + by formulas depending on a variable, which can then be substituted with + a specific object. If the resulting statement is true, that particular + attribute is said to apply to the object. + + Multiple objects forming an instance may share common attributes. A + variable inherits the attributes of the instance it represents. + + (Contributed by Wolf Lammen, 12-Oct-2025.) $) + wl-cleq-2 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= + ( dfcleq ) ABCD $. + $} + + ${ + $d x A $. $d x B $. + $(
Disclaimer: The material presented here is just + my (WL's) personal perception. I am not an expert in this field, so + some or all of the text here can be misleading, or outright wrong. This + text should be read as an exploration rather than as definite + statements, open to doubt, alternatives, and reinterpretation.

Introducing a New Concept: Well-formed formulas

@@ -598738,6 +598780,10 @@ both sides with predefined tokens (in Metamath: keywords), beginning variable for another. This suffices only for very elementary theorems such as ~ idi . + In the formal language of Metamath these variables are not interpreted + with concrete statements, but serve purely as placeholders for + substitution. + 3. Add primitive formulas Rewrite rules describing primitive formulas of type "wff" are then added @@ -598770,7 +598816,7 @@ both sides with predefined tokens (in Metamath: keywords), beginning following later. (Contributed by Wolf Lammen, 21-Aug-2025.) $) - wl-cleq-2 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= + wl-cleq-3 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= ( dfcleq ) ABCD $. $} @@ -598779,12 +598825,12 @@ both sides with predefined tokens (in Metamath: keywords), beginning $(
Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong. This - and the following texts should be read as explorations rather than as - definite statements, open to doubt, alternatives, and reinterpretation. + text should be read as an exploration rather than as definite + statements, open to doubt, alternatives, and reinterpretation.

Introducing a New Concept: Classes

- In ~ wl-cleq-2 we examined how the basic notion of a well-formed formula + In ~ wl-cleq-3 we examined how the basic notion of a well-formed formula is introduced in set.mm. A similar process is used to add the notion of a class to Metamath. This process is somewhat more involved, since two parallel variants are established: sets and the broader notion of @@ -598802,7 +598848,7 @@ In the First Order Logic (FOL) portion of set.mm objects themselves are variables, is somewhat of a misnomer. Its final meaning - and the name that goes with it - becomes justified only in later developments. - We will now revisit the four basic steps presented in ~ wl-cleq-2 , + We will now revisit the four basic steps presented in ~ wl-cleq-3 , this time focusing on object variables and paying special attention to the additional complexities that arise from extending sets to classes. @@ -598811,7 +598857,7 @@ In the First Order Logic (FOL) portion of set.mm objects themselves are 1a. Reserve a type code for classes, specifically the grammar constant "class". Initially, this type code applies to class variables and will later, beyond these four steps, also be assigned to formulas that - define specific classes, i.e. objects. + define specific classes, i.e. instances. 1b. Reserve a type code for set variables, represented by the grammar constant "setvar". The name itself indicates that this type code will @@ -598870,7 +598916,7 @@ In the First Order Logic (FOL) portion of set.mm objects themselves are represent sets to those variables. (Contributed by Wolf Lammen, 25-Aug-2025.) $) - wl-cleq-3 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= + wl-cleq-4 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= ( dfcleq ) ABCD $. $} @@ -598879,8 +598925,8 @@ In the First Order Logic (FOL) portion of set.mm objects themselves are $(
Disclaimer: The material presented here is just my (WL's) personal perception. I am not an expert in this field, so some or all of the text here can be misleading, or outright wrong. This - and the following texts should be read as explorations rather than as - definite statements, open to doubt, alternatives, and reinterpretation. + text should be read as an exploration rather than as definite + statements, open to doubt, alternatives, and reinterpretation.

Semantics of Equality

@@ -598896,19 +598942,18 @@ In the First Order Logic (FOL) portion of set.mm objects themselves are 3. Transitivity ` (( x = y /\ x = z ) -> y = z ) ` 4. Identity of Indiscernables (Leibniz's Law): distinct (i.e., - unequal), objects cannot share all the same properties. + unequal), objects cannot share all the same properties (or attributes). - In formal theories, variables are often used to represent objects, - allowing for general statements about relations rather than individual - cases. In such contexts, the properties of a variable are assumed to - mirror those of the object it denotes. For both variables and objects, - items (1) - (4) must either be derived or postulated as axioms. + In formal theories using variables, the attributes of a variable are + assumed to mirror those of the instance it denotes. For both variables + and objects, items (1) - (4) must either be derived or postulated as + axioms. - If the theory allows substituting objects for variables, then the + If the theory allows substituting instances for variables, then the equality rules for objects follow directly from those governing - variables. However, if variables and objects are formally + variables. However, if variables and instances are formally distinguished, this distinction introduces an additional metatheoretical - property, relevant for (4). + attribute, relevant for (4). A similar issue arises when equality is considered between different types of variables sharing properties. Such mixed-type equalities are @@ -598917,23 +598962,23 @@ In the First Order Logic (FOL) portion of set.mm objects themselves are various forms of transitivity typically remain valid, and must be proven or established within the theory. - In set.mm properties are expressed by formulas. Therefore, equal - objects must behave identically, yielding the same results when - substituted into any formula. To verify equality, it suffices to - consider only primitive operations involving free variables, since all - formulas - once definitions are eliminated - reduce to these. Equality - itself introduces no new properties, and can thus be excluded from this - examination. + In set.mm formulas express attributes. Therefore, equal instances must + behave identically, yielding the same results when substituted into any + formula. To verify equality, it suffices to consider only primitive + operations involving free variables, since all formulas - once + definitions are eliminated - reduce to these. Equality itself + introduces no new attribute (an object is always different from all + others), and can thus be excluded from this examination.

Equality in First Order Logic (FOL)

In the FOL component of set.mm, the notion of an "object" is absent. - Only set variables are used to formulate theorems, and their properties + Only set variables are used to formulate theorems, and their attributes - expressed through an unspecified membership operator - are addressed at a later stage. Instead, several axioms address equality directly: ~ ax-6 , ~ ax-7 , - ~ ax-8 , ~ ax-9 and ~ ax-12 , and ax-13 . In practice, restricted + ~ ax-8 , ~ ax-9 and ~ ax-12 , and ~ ax-13 . In practice, restricted versions with distinct variable conditions are used ( ~ ax6v , ~ ax12v ). The unrestricted forms together with axiom ~ ax-13 , allow for the elimination of distinct variable conditions, this benefit is @@ -598954,20 +598999,32 @@ versions with distinct variable conditions are used ( ~ ax6v , derived expressions, often introducing quantification (see for example ~ cbvalvw ). + The auxiliary axioms ~ ax-10 , ~ ax-11 , ax-12 are provable (see + ~ ax10w , for example) if you can substitute ` y ` for ` x ` in a + formula ` ph ` that contains no occurrence of ` y ` and leaves no + remaining trace of ` x ` after substitution. An implicit substitution + is then established by setting the resulting formula equivalent to + ` ph ` under the assumption ` x = y ` . Ordinary FOL substitution + ` [ y / x ] ph ` is insufficient in this context, since ` x ` still + occurs in the substituted formula. A simple textual replacement of the + token ` x ` by ` y ` in ` ph ` might seem an intuitive solution, but + such operations are out of the formal scope of Metamath. + 2e. Axiom of Extensionality. In its elaborated form ( ~ axextb ), it - states that the determining properties of a set ` x ` are the elements + states that the determining attributes of a set ` x ` are the elements ` z ` it contains, as expressed by ` z e. x ` . This is the only primitive operation relevant for equality between set variables. - 3. Equality between classes +

Equality between classes

In set.mm class variables of type "class" are introduced analoguously to set variables. Besides the primitive operations equality and membership, class builders allow other syntactical constructs to - substitute for class variables, enabling them to represent classes. + substitute for class variables, enabling them to represent class + instances. One such builder ( ~ cv ) allows set variables to replace class - variables. Another ( ~ df-clab ) introduces a class object, known as + variables. Another ( ~ df-clab ) introduces a class instance, known as class abstraction. Since a class abstraction can freely substitute for a class variable, formulas hold for both alike. Hence, there is no need to distinguish between class variables and abstractions; the term @@ -598983,23 +599040,23 @@ One such builder ( ~ cv ) allows set variables to replace class extends to all mixed equalities, including those with set variables, since they automatically convert to classes upon substitution. - 3b. Properties. The primitive operation of membership constitutes the - fundamental properties of a class. Axiom ~ df-clel reduces possible + 3b. Attributes. The primitive operation of membership constitutes the + fundamental attributes of a class. Axiom ~ df-clel reduces possible membership relations between class variables to those between a set variable and a class variable. Axiom ~ df-cleq extends ~ axextb to classes, stating that classes are fully determined by their set members. - A class builder may introduce a new property for classes. An equation - involving such a class instance may reveal this property. In the case - of the class builder ~ cv , a property called sethood is in fact + A class builder may introduce a new attribute for classes. An equation + involving such a class instance may express this attribute. In the case + of the class builder ~ cv , an attribute called sethood is in fact introduced: A class is a set if it can be equated with some set variable. - Class abstractions supported by class builder ~ df-clab also introduce - formal properties. Whether a class can be expressed as an abstraction - with a specific predicate may be relevant in analysis. However, since - theorem ~ df-clab is a definition (and hence eliminable), these - properties can also be expressed in other ways. + Class abstractions supported by class builder ~ df-clab also formally + introduce attributes. Whether a class can be expressed as an + abstraction with a specific predicate may be relevant in analysis. + However, since theorem ~ df-clab is a definition (and hence eliminable), + these attributes can also be expressed in other ways. 3c. Conservativity. Because set variables can substitute for class variables, all axioms and definitions must be consistent with theorems @@ -599013,12 +599070,12 @@ One such builder ( ~ cv ) allows set variables to replace class ~ df-clel provide class versions of ~ ax-8 and ~ ax-9 , ensuring that membership is consistent with Leibniz's Law. - Sethood, being based on mixed equality, preserves its value among equal - classes. + Sethood, being based on mixed-type equality, preserves its value among + equal classes. As long as additional class builders beyond those mentioned are only - defined, the reasoning given for ~ df-clab applies generally, and - Leibniz's Law continues to hold. + defined, the reasoning given for class abstraction above applies + generally, and Leibniz's Law continues to hold. 3e. Backward Compatability. A class ` A ` equal to a set should be substitutable for a free set variable ` x ` in any theorem, yielding a @@ -599033,15 +599090,58 @@ One such builder ( ~ cv ) allows set variables to replace class If these axioms hold when ` A ` replaces ` x ` - under the above assumptions - then the replacement can be considered generally valid. - The affected FOL axioms are ~ ax-6 (in the form ~ ax6ev ), ~ ax-7 - ( ~ ax7v1 ), ~ ax-8 ( ~ ax8v1 ) , ~ ax-9 ( ~ ax9v1 ), ~ ax-12 - ( ~ ax12v2 ), and to some extent ~ ax-13 ( ~ ax13v ). Since ZF - (Zermelo-Fraenkel) set theory does not allow quantifification over class - variables, no similar class-based versions of the quantified FOL axioms - exist. + The affected FOL axioms are ~ ax-6 (in the form ~ ax6ev ), ~ ax-7 , + ~ ax-8 , ~ ax-9 , ~ ax-12 ( ~ ax12v2 ), and to some extent ~ ax-13 + ( ~ ax13v ). Since ZF (Zermelo-Fraenkel) set theory does not allow + quantifification over class variables, no similar class-based versions + of the quantified FOL axioms exist. (Contributed by Wolf Lammen, 18-Sep-2025.) $) - wl-cleq-4 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= + wl-cleq-5 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= + ( dfcleq ) ABCD $. + $} + + ${ + $d x A $. $d x B $. + $(
Disclaimer: The material presented here is just + my (WL's) personal perception. I am not an expert in this field, so + some or all of the text here can be misleading, or outright wrong. This + text should be read as an exploration rather than as definite + statements, open to doubt, alternatives, and reinterpretation. + +

Eliminability of classes

+ + One requirement of Zermelo-Fraenkel set theory (ZF) is that it can be + formulated without referring to classes. Since set.mm implements ZF, + it must therefore be possible to eliminate all classes. + + This has two main implications. + + First, every class builder other than ~ cv must be a definition, making + its elimination straightforward. The class abstraction ~ df-clab is a + special case: it reduces the primitive expression ` x e. { y | ph } ` to + a first-order logic (FOL) predicate. Other class expressions, such as + ` A = B ` or ` A e. B ` , can ultimately be reduced to occurrences of + ` x e. A ` . Hence, if a class variable ` A ` represents only class + abstractions, some groundwork for eliminability is already established. + + Since set variables themselves can be expressed as class abstractions + - namely ` x = { y | y e. x } ` (see ~ cvjust ) - this formulation does + not conflict with the use of class builder ~ cv . + + Second, substituting a class abstraction for a class variable ` A ` must + not introduce a recursion. The predicate used in the abstraction must + not depend on class variables again. Under this restriction, a finite + number of elimination steps will reduce the class variable ` A ` to a + term expressed purely in FOL, without classes. + + These conditions apply only to substitution. The expression + ` A = { x | x e. A } ` ( ~ abid1 ) is a valid and provable equation, and + it should not be interpreted as an assignment that binds a particular + instance to ` A ` . + + (Contributed by Wolf Lammen, 13-Oct-2025.) $) + wl-cleq-6 $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $= ( dfcleq ) ABCD $. $}