From cd40451f4dd31504d0541ca873a84aa5d71d0533 Mon Sep 17 00:00:00 2001 From: "David A. Wheeler" Date: Mon, 21 Oct 2024 10:34:10 -0400 Subject: [PATCH 1/2] Document unbound variables are basically universal Document an issue discussed in the Metamath mailing list, subject "Re: [Metamath] Question about a specific problem probably unrelated with metamath". Signed-off-by: David A. Wheeler --- set.mm | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/set.mm b/set.mm index f0c9ab553b..67c48050ae 100644 --- a/set.mm +++ b/set.mm @@ -431159,6 +431159,13 @@ be applied for new theorems (formerly, the class and wff variables ~ mmtheorems32.html#mm3146s also describes the metatheorem that underlies this. +

You should read any statement starting with ` |- ` + and having one or more unbound set variable(s) as universally + quantified over those + variables. So when you see ` |- 0 < k ` that's saying " ` 0 < k ` is + derivable in the empty context" which is a strong statement, + equivalent to ` A. k 0 < k ` which without further context is false. +

Additional rules for definitions

Standard Metamath verifiers do not distinguish between axioms and From 0c028aece1514dd4b1dc16850a13598f02c9876f Mon Sep 17 00:00:00 2001 From: "David A. Wheeler" Date: Mon, 21 Oct 2024 10:56:47 -0400 Subject: [PATCH 2/2] Note that class variables as postulates are fine Attempt to resolve a comment from Scott Fenton (@sctfn). Signed-off-by: David A. Wheeler --- set.mm | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/set.mm b/set.mm index 67c48050ae..864cb7dc1f 100644 --- a/set.mm +++ b/set.mm @@ -431162,9 +431162,12 @@ be applied for new theorems (formerly, the class and wff variables

You should read any statement starting with ` |- ` and having one or more unbound set variable(s) as universally quantified over those - variables. So when you see ` |- 0 < k ` that's saying " ` 0 < k ` is - derivable in the empty context" which is a strong statement, - equivalent to ` A. k 0 < k ` which without further context is false. + variables. So if you state ` |- 0 < k ` , say as a postulate, + that's saying " ` 0 < k ` is derivable in the empty context" + which is a strong statement, + equivalent to ` A. k 0 < k ` , which without further context is false. + The same is not true for class variables (e.g., ` 0 < K ` is typically + safe to postulate).

Additional rules for definitions