The initial version has a comment:
The necessitation rule: if something is true, it is necessary true. 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. (*true ≠ valid ≠ provable*) Also something like Turns out this axiom is true in GL, hence GL extends K4. should probably read "valid" rather than "true". savask schrieb am Sonntag, 30. November 2025 um 14:55:52 UTC+1: > A quite popular tradition among software engineers is to solve one small > programming task on each day of advent (for example, see Advent of Code). > Last year we did the same thing > <https://groups.google.com/g/metamath/c/S9zHruNKjAs/m/58OugIdnBwAJ> but > for formalizing small theorems about magmas in Metamath, and to a great > success! > > This year I propose a new set of problems for your entertainment, but this > time about modal logics: > > https://gist.github.com/savask/58dbbaf3612317231687ca95fe746bc6 > > The problems deal with the provability logic GL which can be used to > express some famous results like Godel's second theorem and its > implications. Although it might seem like an involved topic requiring deep > knowledge of logic and proof theory, one doesn't need to know any complex > mathematics at all - all one needs is a good enough grasp on usual > propositional proofs (let's say up to theorem wex in set.mm) and the rest > is explained in the file. > > Most proofs will be quite short (if not trivial), but I believe in some > cases one needs to show some wit to come up with the proofs on their own. > If you ever find yourself stuck, solutions to most of these puzzles can be > found in the book of Boolos "The logic of provability", chapters 1 and 3. > > I should also say that I know the proofs of all statements with the > exception of Day 20, about the reflection principle. I haven't been able to > figure it out myself, and Boolos proves it with a different method > (although he says that a usual proof "is not particularly difficult"), so I > would be glad if someone shares the proof with me. > -- 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/61524c71-1507-4053-a9bc-735d252ca9c7n%40googlegroups.com.
