To be fair, set.mm doesn't really ever use the term "valid" in the logical sense. At best, it talks about wffs being "universally true", "unconditionally true" (in ax-gen), or "provable" (when explaining the turnstile symbol), and in some descriptions (e.g., idi, ax-mp) imprecisely abbreviates this to "true". Perhaps avoiding that terminology was in the interest of accessibility, or perhaps it may have been a particular habit of NM, who in his paper uses "valid" to mean "syntactically well-formed".
If I were writing it, I'd likely just steal "unconditionally true" from the ax-gen description. Matthew House On Mon, Dec 1, 2025, 9:13 AM 'Discher, Samiro' via Metamath < [email protected]> wrote: > Such issues highlight that natural language contains many pitfalls when > it comes to precision. > Technically, when you say "Any theorem of logic is necessary", I would > interpret that as (⊢p) ⇒ □(⊢p). But you mean to say (⊢p) ⇒ (⊢□p). > > Already the term "necessary" is questionable, as modal logic is about > whether something is "necessarily true", which is not the same as > "necessary" (the latter is less specific and can refer to things that are > not about truth). > > A more natural way to express that "□p" is a theorem in GL is to say that > the statement that p is PA-provable is GL-provable. Which circumvents an > issue that emerges only due to mixing meta with object language in natural > language.. > > I only meant to point out some mistakes in terminology, it is up to you > what you make of it! > ------------------------------ > *Von:* [email protected] <[email protected]> im Auftrag > von savask <[email protected]> > *Gesendet:* Montag, 1. Dezember 2025 14:01:03 > *An:* Metamath > *Betreff:* [Metamath] Re: Advent of Metamath 2025 > > Thank you for the remarks. Admittedly, I haven't tried to be very precise > in theorem comments, for the most part their goal is to provide at least > some intuition for the symbols. I'll wait for a bit in case others (or you) > have other remarks, so I'll update the file all in one go. > > > But that is false. The necessitation rule actually says: if something > (to be true) is a theorem (i.e. provable from only axioms, no premises), > then it to be necessary (necessarily true) is also a theorem. > > I'm a bit reluctant to use "provable" here as the box symbol is later > interpreted as "provable in PA". I can rephrase the comment as follows "Any > theorem of logic is necessary", this is the motivation used by Standford's > encyclopedia of philosophy > <https://plato.stanford.edu/entries/logic-modal/>. > > > "Turns out this axiom is true in GL, hence GL extends K4." should > probably read "valid" rather than "true". > > Again, to avoid loaded terms, I can rephrase it as "Turns out this axiom * > holds* in GL ...". Is that okay? > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/a59931d7-5724-4a11-950c-84f4aeac64c8n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/a59931d7-5724-4a11-950c-84f4aeac64c8n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion visit > https://groups.google.com/d/msgid/metamath/aa62e696d6bd4d1c827e72d779391311%40rwth-aachen.de > <https://groups.google.com/d/msgid/metamath/aa62e696d6bd4d1c827e72d779391311%40rwth-aachen.de?utm_medium=email&utm_source=footer> > . > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion visit https://groups.google.com/d/msgid/metamath/CADBQv9ZjSUzN5pORwzW6A9YC0V38ttW3xY1LKNwEbs7%3DyE%3DpCw%40mail.gmail.com.
