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.
