From 50de00a2e9ba4f268fab977a1656fa0d7a709d48 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sun, 21 Jan 2024 17:53:27 +0100 Subject: [PATCH 1/3] mmset.raw.html: fix a few typos and use uniform term 'condition'. --- mmset.raw.html | 185 ++++++++++++++++++++++++------------------------- 1 file changed, 92 insertions(+), 93 deletions(-) diff --git a/mmset.raw.html b/mmset.raw.html index 207b8ec05..200c426de 100644 --- a/mmset.raw.html +++ b/mmset.raw.html @@ -671,7 +671,7 @@ the direct replacement of a variable with an expression. The more complex proper substitution of traditional logic is a derived concept in Metamath, broken down into multiple primitive steps. -Distinct variable provisos, which accompany certain +Distinct variable conditions, which accompany certain axioms and are inherited by theorems, forbid unsound substitutions.]

@@ -1076,7 +1076,7 @@

-Distinct variable restrictions +Distinct variable conditions     Our final requirement for substitutions is described in Appendix 3: Distinct Variables below. These @@ -2757,7 +2757,7 @@ clever use of equality axioms) it eliminates the latter's primitive notions of "proper substitution" and "free variable," replacing them with direct substitution and the notion of a variable not occurring in a formula (which we -express with distinct variable constraints). +express with distinct variable conditions).

@@ -2812,7 +2812,7 @@ the system). Simple metalogic consists of schemes containing wff metavariables (with no arguments) and/or setvar (also called "individual") metavariables (i.e. in the form of the wff syntax -described above), accompanied by optional provisos each stating that two +described above), accompanied by optional conditions, each stating that two specified setvar metavariables must be distinct or that a specified setvar metavariable may not occur in a specified wff metavariable. Metamath's logic and set theory axiom and rule schemes are all examples of simple metalogic. @@ -3074,11 +3074,11 @@

Except for ~ ax-6 , our system includes all axiom schemes of Tarski's -system. In the case of ax-6, Tarski's version is weaker because it -includes a distinct variable proviso. If we wish, we can also weaken +system. In the case of ~ ax-6 , Tarski's version is weaker because it +includes a distinct variable condition. If we wish, we can also weaken our version in this way and still have a system that is scheme-complete. Theorem ~ ax6 shows this by deriving, in the presence of the other -axioms, our ax-6 from Tarski's weaker version ~ ax6v . However, we chose +axioms, our ~ ax-6 from Tarski's weaker version ~ ax6v . However, we chose the stronger version for our system because it is simpler to state and easier to use. (Technically, our ~ ax-7 , ~ ax-8 , and ~ ax-9 are sub-schemes of a single higher-order scheme in Tarski's system, but @@ -3088,21 +3088,22 @@

Substitution -instances of schemes    In Metamath, by -default (i.e. when no distinct variable provisos are present; see     +In Metamath, by +default (i.e., when no distinct variable conditions are present; see below) there are no restrictions on substitutions that may be made into a scheme, provided we honor the metavariable types (wff variable or setvar variable). This is called -direct substitution, in constrast to a more complicated "proper +direct substitution, in contrast to a more complicated "proper substitution" used in textbook predicate calculus. Consider, for -example, axiom scheme ~ ax-6 , which can be abbreviated as "` E. x ` ` x = y `" +example, axiom scheme ~ ax-6 , which can be abbreviated as "` E. x x = y `" (theorem scheme ~ ax6e ), "there exists (` E. `) an ` x ` -such that ` x ` equals ` y ` ." In traditional predicate +such that ` x ` equals ` y ` ". In traditional predicate calculus, the first argument (a variable) of the quantifier ` E. ` is considered "bound" in the wff serving as its second -argument (i.e. in the quantifier's "scope"), otherwise it is -"free." Substitutions must follow careful rules taking into account -of whether the variable is bound or free at a given position. In the +argument (i.e., in the quantifier's "scope"), otherwise it is +"free". Substitutions must follow careful rules taking into account +whether the variable is bound or free at a given position. In the Metamath language, ` E. ` is merely a 2-place prefix connective or "operation" that evaluates to a wff, taking a setvar variable as its first argument and a wff as its @@ -3115,15 +3116,14 @@ In fact, ` x ` and ` y ` are metavariables and not the actual individual variables that predicate calculus refers to. --> -(When we do need to prohibit certain substitutions, they are done with -"distinct variable" provisos we describe below, that apply to a theorem as a +(When we do need to prohibit certain substitutions, we use "distinct variable" +conditions, which we describe below, that apply to a theorem scheme as a whole without consideration of whether a variable's occurrence is free or -bound. This makes makes figuring out what substitutions are allowed very -simple.) +bound. This makes figuring out what substitutions are allowed very simple.)

-The expression "` E. x ` ` x = y `" is just a recipe for generating an infinite +The expression "` E. x x = y `" is just a recipe for generating an infinite number of actual axioms. In an actual axiom such as "` E. ` v3 v3 ` = ` @@ -3135,8 +3135,8 @@ (This is what traditional predicate calculus means when it says that free variable v2 and bound variable -v3 must be distinct i.e. can't -both be substituted with a common third variable.) +v3 must be distinct, i.e., cannot +both be substituted with a common variable.) --> Another axiom that results from the recipe is "` E. ` v3 @@ -3264,7 +3264,7 @@     Sometimes we must place restrictions on the formulas generated by a scheme in order to ensure their soundness, and we use distinct -variable restrictions for this purpose. For example, the theorem scheme +variable conditions for this purpose. For example, the theorem scheme ~ dtru , ` -. A. x ` ` x = y ` , has the restriction that metavariables ` x ` and ` y ` cannot be substituted with the same actual variable, otherwise we could end up with the nonsense substitution instance "` -. A. ` @@ -3273,15 +3273,15 @@ v1" which would mean "it is not true that every object v1 equals itself." -The substitution rule of Metamath ensures that distinct variable restrictions +The substitution rule of Metamath ensures that distinct variable conditions "propagate" from axiom schemes having such restrictions into theorem schemes -using those axiom schemes; in other words, distinct variable restrictions in +using those axiom schemes; in other words, distinct variable conditions in axiom schemes are inherited by theorems whose proofs make use of those schemes.

-Note that distinct variable restrictions are metalogical conditions +Note that distinct variable conditions are metalogical conditions imposed on certain axiom and theorem schemes. They have no role in the actual logic (object language), where two actual variables with different names are distinct by definition—simply because they have different names, @@ -3305,7 +3305,7 @@ v1 v1 = v2." Instead, the distinct variable -restriction on ~ dtru is enforced at the level of +condition on ~ dtru is enforced at the level of theorem schemes. In this example, we are not allowed to substitute the same metavariable, say ` z ` , for both ` x ` and ` y ` whenever we reference ~ dtru in a proof step. @@ -3371,7 +3371,7 @@ @@ -3630,23 +3630,23 @@     In logic and set theory literature, theorems (or more precisely, theorem schemes) are often accompanied by side conditions, or provisos, written in -informal English. Typically these are written after the statement of the -theorem and expressed in a form such as "where x is a variable that -[satisfies some constraint]." In order to satisfy the metalogical requirements +informal English. Typically, these are written after the statement of the +theorem and expressed in a form such as "where ` x ` is a variable that +[satisfies some constraint]". In order to satisfy the metalogical requirements of Tarski's axiom system on which it is based, Metamath implements three kinds of provisos through the use of its "distinct variable" conditions. These restrict what substitutions are allowed, and often -you will see a proviso such as the following accompanying an axiom or theorem +you will see a condition such as the following accompanying an axiom or theorem (for example, ~ ax-5 and ~ dtru ):

Distinct variable groups: -  ` x ` ,` y `   ` x ` ,` ph `   ` x ` ,` A ` +  ` x , y `   ` x , ph `   ` x , A `

-These three groups (in this example 3 pairs) have the following meanings, +These three groups (in this example, three pairs) have the following meanings, respectively, as side conditions of the theorem scheme or axiom scheme shown above them:

    @@ -3683,9 +3683,9 @@ variable pair is officially called a "disjoint variable pair" in the Metamath specification. We present the rule as three separate cases above for clarity. In the set theory database file, set.mm, we adopt the convention that at least -one setvar variable always appears in a distinct variable pair, so these are +one setvar variable always appear in a distinct variable pair, so these are the only cases you will see. Under this convention, a distinct variable pair -such as "` A ` ,` ph `" will never occur, even though technically it is not +such as "` A , ph `" will never occur, even though technically it is not illegal.]

    @@ -3693,59 +3693,59 @@ Note that

    -Distinct variable group:   ` ph ` ,` x ` +Distinct variable group:   ` ph , x `
    means the same thing as

    -Distinct variable group:   ` x ` ,` ph ` +Distinct variable group:   ` x , ph `

    Finally, if more than two variables appear in a group, this is an abbreviated -way of saying that the restrictions apply to all possible pairs in the group. +way of saying that the conditions apply to all possible pairs in the group. So,

    -Distinct variable group:   ` x ` ,` y ` ,` ph ` +Distinct variable group:   ` x , y , ph `
    means the same thing as

    Distinct variable groups:   -` x ` ,` y `   ` x ` ,` ph `   ` y ` ,` ph ` +` x , y `   ` x , ph `   ` y , ph `

    -The basic rule to remember is that distinct variable provisos are inherited +The basic rule to remember is that distinct variable conditions are inherited by substitutions (that take place in a proof step). For example, look at Step 1 of the proof of ~ cleljustALT , which has a substitution instance of -~ ax-5 . As you can see, ~ ax-5 requires the distinct variable pair ` x ` , -` ph ` . +~ ax-5 . As you can see, ~ ax-5 requires the distinct variable pair ` x , ph ` . Step 1 substitutes ` z ` for ` x ` and ` x e. y ` for ` ph ` . This substitution transforms the original distinct variable requirement into -the two distinct variable pairs ` z ` ,` x ` and ` z ` ,` y ` , which will -implicitly accompany step 1 (although not shown explicitly in step 1 of the -proof listing). Thus step 1 can be read in full, "` ( x e. y -> A. z ` -` x e. y ) ` where ` z ` ,` x ` are distinct and ` z ` ,` y ` are distinct." +the two distinct variable pairs ` z , x ` and ` z , y ` , which will +implicitly accompany Step 1 (although not shown explicitly in step 1 of the +proof listing). Thus, Step 1 can be read in full, +"` |- ( x e. y -> A. z x e. y ) ` where ` z , x ` are distinct and +` z , y ` are distinct". The proof verifier will check that this requirement accompanies the final theorem, otherwise it will flag the proof step as invalid. You can see this requirement in the "Distinct variable groups" list on the ~ cleljustALT page.

    -This can be confusing if you don't understand -how distinct variables requirements are inherited from referenced axioms -or theorems in order to satisfy their distinct variable requirements. +This can be confusing if you do not understand +how distinct variables conditions are inherited from referenced axioms +or theorems in order to satisfy their distinct variable conditions. Let us consider an example (courtesy of Gérard Lang). Naively, one might think that ~ ax-13 (which has no -distinct variable requirements) is derivable from ~ ax-5 , arguing as follows. +distinct variable conditions) is derivable from ~ ax-5 , arguing as follows. Since the letter ` x ` has no occurrence in the wff ` y = z ` , one might think that a direct application of ~ ax-5 would give (` y = z -> A. x ` ` y = z `) as a theorem -with no distinct variable requirements, so that ~ ax-13 easily +with no distinct variable conditions, so that ~ ax-13 easily follows by adding an antecedent with ~ a1i . However, "distinct" does not merely mean that two setvar variables have different names; it means that we also must prevent them from being @@ -3754,27 +3754,27 @@ Axioms vs. axiom schemes and Distinct metavariables above.) To apply ~ ax-5 , we must explicitly ensure that ` x ` is distinct from both -` y ` and ` z ` in ` y = z ` by adding two distinct variable requirements. +` y ` and ` z ` in ` y = z ` by adding two distinct variable conditions. Otherwise, we could further substitute ` x ` for ` y ` to -arrive at (` x = z -> A. x ` ` x = z `); this violates the ~ ax-5 requirement -since ` x ` does appear in ` x = z ` . +arrive at (` x = z -> A. x x = z `); this violates the distinct variable +condition of ~ ax-5 since ` x ` does appear in ` x = z ` . In fact, from ~ ax-5 we can conclude only the very restricted theorem ~ ax13w , which because of -its distinct variable requirements is much weaker than axiom ~ ax-13 . +its distinct variable conditions is much weaker than axiom ~ ax-13 . (If we omit them, the Metamath proof verifier will give an error message.) -We say that the distinct variable requirements in ~ ax13w are inherited +We say that the distinct variable conditions in ~ ax13w are inherited from ~ ax-5 .

    -In the Metamath language, distinct variable requirements are specified with $d +In the Metamath language, distinct variable conditions are specified with $d statements, placed before an assertion ($a or $p) and in the same scope. Each theorem must be accompanied by those $d statements needed to satisfy all -distinct variable requirements implicitly attached the proof steps. +distinct variable conditions implicitly attached the proof steps.

    -To get a concrete feel for distinct variable requirements, you can temporarily +To get a concrete feel for distinct variable conditions, you can temporarily comment out the "$d x z $." condition for theorem ~ cleljustALT in the database file set.mm. When you try to verify the proof with the Metamath program, the resulting error @@ -3792,7 +3792,7 @@ There is a disjoint variable ($d) violation at proof step 25. Assertion "ax-5" requires that variables "ph" and "x" be disjoint. But "ph" was substituted with "x e. y" and "x" was substituted with "z". -Variables "x" and "z" do not have a disjoint variable requirement in the +Variables "x" and "z" do not have a disjoint variable condition in the assertion being proved, "cleljustALT". Such error messages can also be used to determine any missing $d statements @@ -3801,7 +3801,7 @@ automatically. "` /\ `" and "≡" in -place of our "` A. `" and "=", and the notation "OC(φ)" means "the +place of our "` A. `" and "=" respectively (which allows him to use "=" for +the side condition of (B7)), and the notation "OC(φ)" means "the set of all variables occurring in φ". These two schemes are identical to our ~ ax-5 and ~ ax6v , which are accompanied by distinct variable conditions that can be read "where ` x ` doesn't occur in ` ph `" and "where @@ -3881,7 +3882,7 @@ Sometimes new or "dummy" variables are used inside of a proof that do not appear in the theorem being proved. On the web pages we omit them from the "Distinct variable group(s)" list, which is intended to show only those -distinct variable requirements that need to be satisfied by any proof that +distinct variable conditions that need to be satisfied by any proof that references the theorem.

    @@ -3936,7 +3937,7 @@

    -Some people who dislike this requirement have made $d statements for dummy +Some people who dislike this requirement have made $d statements for dummy variables optional for their Metamath language verifiers (although strictly speaking this violates the current Metamath spec); an example is Hmm. There is nothing wrong with this in @@ -3964,7 +3965,7 @@ In a sense, Metamath is opposite from the usual textbook convention: in Metamath, any variable may appear in a substitution instance of a wff by default; it is the exceptions that must be made explicit with distinct -variable requirements. Keeping this in mind may make the comparison to logic +variable conditions. Keeping this in mind may make the comparison to logic textbooks a little easier.

    --> @@ -4055,7 +4056,7 @@

    @@ -4063,7 +4064,7 @@ Note 4     -Distinct variable requirements are sometimes confusing to Metamath newcomers. +Distinct variable conditions are sometimes confusing to Metamath newcomers. Unlike traditional predicate calculus, Metamath does not confer a special status to a bound variable (e.g. the quantifier variable ` x ` in ` A. x ph `); there is no built-in @@ -4073,7 +4074,7 @@ from a variable after any other constant connective such as "` -. `". The only thing that matters is that the syntax is legal for the variable type (wff, setvar, or class), and that any distinct -variable requirements are satisfied. This different paradigm may take +variable conditions are satisfied. This different paradigm may take some getting used to by someone used to traditional "proper substitution" (which involves analyzing the scopes of bound variables and renaming them if necessary), even though it is significantly @@ -4096,20 +4097,18 @@

    @@ -4118,12 +4117,12 @@ Note 5     Interestingly, the -distinct variable requirements ($d statements) accompanying theorems are +distinct variable conditions ($d statements) accompanying theorems are theoretically redundant, because the proof verifier could in principle -infer and propagate them forward from the distinct variable requirements +infer and propagate them forward from the distinct variable conditions of the axioms. The Metamath Solitaire applet does this, inferring both the resulting proof steps -and their distinct variable requirements as you feed it axioms to +and their distinct variable conditions as you feed it axioms to build a proof. (The mmj2 program will also infer the necessary $d statements for a proof under development.) The Metamath language spec, on the other hand, requires them to be @@ -4132,7 +4131,7 @@ verify a proof in isolation but would have to analyze every proof it depends on), but making them explicit also allows someone writing a proof to easily determine by inspection the distinct variable -requirements of a theorem he or she wishes to reference. +conditions of a theorem he or she wishes to reference.

    @@ -4157,7 +4156,7 @@ discussion about distinctors.

    - @@ -4785,19 +4784,19 @@

    -System with no distinct variables. -This system has no distinct variable constraints, making the concept of +System with no distinct variable conditions. +This system has no distinct variable conditions, making the concept of substitution as simple as it can possibly be and also significantly simplifying the algorithm for verifying proofs. It is equivalent to system S2 in Section 4 of [Megill]. The primary drawback of this system is that for it to be considered complete, we must ignore antecedents called "distinctors" that stand in for what -would be distinct variable constraints (see the linked discussion). +would be distinct variable conditions (see the linked discussion).

    We can optionally include ~ ax-c15 or ~ ax-12 for a somewhat more powerful -metalogic, since these also involve no distinct variable restrictions (although +metalogic, since these also involve no distinct variable conditions (although without them we can still derive any instance of them not containing wff metavariables).

    From 5c90cdc5a87c67c6266a996942611cc94dded881 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Sun, 21 Jan 2024 17:55:59 +0100 Subject: [PATCH 2/3] Link from the comment of ax-5 to the explanation of DV conditions. --- set.mm | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/set.mm b/set.mm index 6c107f911..baa869230 100644 --- a/set.mm +++ b/set.mm @@ -15583,8 +15583,11 @@ only postulated (that is, axiomatic) rule of inference of predicate This axiom essentially says that if ` x ` does not occur in ` ph ` , i.e. ` ph ` does not depend on ` x ` in any way, then we can add the quantifier ` A. x ` to ` ph ` with no further assumptions. By ~ sp , we - can also remove the quantifier (unconditionally). (Contributed by NM, - 10-Jan-1993.) $) + can also remove the quantifier (unconditionally). + + For an explanation of disjoint variable conditions, see + ~ https://us.metamath.org/mpeuni/mmset.html#distinct . (Contributed by + NM, 10-Jan-1993.) $) ax-5 $a |- ( ph -> A. x ph ) $. $} From 346c93b756c19bb58432ae0ebec5995a30660992 Mon Sep 17 00:00:00 2001 From: Benoit Jubin Date: Tue, 23 Jan 2024 21:12:05 +0100 Subject: [PATCH 3/3] typo --- mmset.raw.html | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mmset.raw.html b/mmset.raw.html index 200c426de..33f328d4f 100644 --- a/mmset.raw.html +++ b/mmset.raw.html @@ -3683,7 +3683,7 @@ variable pair is officially called a "disjoint variable pair" in the Metamath specification. We present the rule as three separate cases above for clarity. In the set theory database file, set.mm, we adopt the convention that at least -one setvar variable always appear in a distinct variable pair, so these are +one setvar variable should always appear in a distinct variable pair, so these are the only cases you will see. Under this convention, a distinct variable pair such as "` A , ph `" will never occur, even though technically it is not illegal.]