I'm finding it somewhat fun to work out the "reverse mathematics" for this: I get that ax-mp, ax-1, ax-2, ax-3, ax-necess, ax-distrb, and ax-gl are all independent from each other, and the theorems axk4, puzzlelem, and puzzle require all the axioms. (In particular, puzzlelem and puzzle require the full ax-gl, axk4 is insufficient.)
The most intriguing part to me is how the axk4 proof requires ax-3, despite the fact that neither it nor the modal-logic axioms reference negation in any way. Matthew House On Wed, Dec 3, 2025 at 8:27 PM savask <[email protected]> wrote: > > There you go: (solution of Day 20) > > Thanks! I haven't been able to find this proof anywhere in the literature, > so this might be a useful reference for some other people as well. There > seems to be ongoing work on formalizing modal logics in HOL Light, in > particular, they have an automatic prover for GL > https://link.springer.com/article/10.1007/s10817-023-09677-z Maybe in the > worst case one could try to extract the proof from this utility, though I'm > not sure if it's possible. > > > So far, I made almost all proofs by hand (in metamath.exe) without any > help. ... > > I've been using metamath lamp to formalize the proofs, and I've been > sometimes wondering if its proof searching utility is missing some short > arguments. I haven't tried comparing it with metamath.exe's improve > command, though. > > > Note: I believe ~puzzlelem requires ~ax-gl for its proof, even tho > there was no "now you can use ~ax-gl again" in the comment. > > Yes, days 21 - 24 are "ax-gl free", and at day 25 you're allowed to use > ax-gl again. > > -- > 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/b6b66bbe-298a-405a-a59c-c997629513b9n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/b6b66bbe-298a-405a-a59c-c997629513b9n%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/CADBQv9Y8yoBYz%3D7e9pNO%3D6e6Fz0D-omW_qxx9dLeBvbZqNPfEw%40mail.gmail.com.
