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/ee55ece1-c83e-4cad-a94b-c11855803824n%40googlegroups.com.
