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]<mailto:[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.
