Advent of Metamath 2025

[savask]

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 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.

[samiro.d...@rwth-aachen.de]

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]

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.

> "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?

[Discher, Samiro]

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: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von savask <sav...@yandex.ru>
Gesendet: Montag, 1. Dezember 2025 14:01:03
An: Metamath
Betreff: [Metamath] Re: Advent of Metamath 2025

 

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/a59931d7-5724-4a11-950c-84f4aeac64c8n%40googlegroups.com.

[Matthew House]

To be fair, set.mm doesn't really ever use the term "valid" in the logical sense. At best, it talks about wffs being "universally true", "unconditionally true" (in ax-gen), or "provable" (when explaining the turnstile symbol), and in some descriptions (e.g., idi, ax-mp) imprecisely abbreviates this to "true". Perhaps avoiding that terminology was in the interest of accessibility, or perhaps it may have been a particular habit of NM, who in his paper uses "valid" to mean "syntactically well-formed".

If I were writing it, I'd likely just steal "unconditionally true" from the ax-gen description.

Matthew House

To view this discussion visit https://groups.google.com/d/msgid/metamath/aa62e696d6bd4d1c827e72d779391311%40rwth-aachen.de.

[Gino Giotto]

>  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.

There you go:

$( Day 20.  Formula ` []. ph -> ph ` is called the reflection principle for
   ` ph ` , in particular, ~ ax-gl means that ` ph ` is provable if the
   reflection principle for ` ph ` is provable.  The following result means
   that there's no single reflection principle which implies
   ` -. []. []. F. ` .  See Boolos p. 63 for more context. $)
norefl $p |- ( []. ( ( []. ph -> ph ) -> -. []. []. F. ) -> []. []. F. ) $=
  ( cbox wi wfal wn wa wo imor imbi1i jaob monrule distrconj axk4 ax-distrb syl
  sylbb con4 a1d ja 3syl pm2.21 pm2.24 com12 cdiam notnotr con3i df-diam kurbis
  biimpri imp monimpconj syl2anr sylbi ax-gl ) ABZACZDBZBZEZCZBUOEZUSCZAUSCZFZB
  ZURUQCZBZURUTVDUTVAAGZUSCVDUPVHUSUOAHIVAUSAJPKVEVBBZVCBZFVGVBVCLVJUOUSBZCZBZU
  RUOCZBVGVIVJVJBVMVCMVJVLAUSNKOVBVNUOURQKVLVNVFVLVNVFUOVKVNVFCVNVAVFURUOVAVFCU
  SVFVAURUQUARUOVFUBSUCVKVFVNVKUQURVKUQEZEZBZEZBVOUDZBUQUSVRVQURVPUQUQUEKUFKVRV
  SVSVRVOUGUIKVODUHTRRSUJUKULUMUQUNT $.

I made this proof on my own. I almost completed the other ones too, but maybe I'll post them all together if I finish. In my opinion, this proof was a bit difficult (contrary to what Boolos says), especially since I've never heard of this logic before this challenge.

[Gino Giotto]

My current progress here: https://github.com/metamath/set.mm/commit/4ea74c3d42b6f6fc8087b9fd2323285dedf76869

So far, I made almost all proofs by hand (in metamath.exe) without any help. The only exception is ~axk4, where after making a number of unsuccessful attempts I quickly peeked at Boolos book. I have the impression that there is basically only one idea that derives ~axk4 from ~ax-gl, and if you don't find that idea then you're lost. Interestingly, the proof is pretty short once you get the right track. Some of the long ones were not easy too, but I got them in the end. I have not compared my proofs with the ones in the book (except for ~axk4), so maybe there are original ideas in here.

[Gino Giotto]

Challenge completed: https://github.com/GinoGiotto/set.mm/blob/adv2025/adv2025.mm

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.

[savask]

> 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.

[Matthew House]

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

--

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 metamath+u...@googlegroups.com.

To view this discussion visit https://groups.google.com/d/msgid/metamath/b6b66bbe-298a-405a-a59c-c997629513b9n%40googlegroups.com.

[Gino Giotto]

> 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.

I don't know about metamath lamp, but the search power of the metamath.exe 'improve' command is very minimal. For the most part, I use it in the form of 'improve last /depth 1' to fill in some basic propositional logic steps. It isn't really much useful beyond that (it has more options which can be consulted by typing 'help improve', although they considerably slow down the proof search and I rarely have success with them). I'd say that the minimizer is probably the most advanced piece of automation that metamath.exe has (I put the minimized proof of Day 20 in adv2025.mm).

The thing I like metamath.exe isn't automation, but rather that it's fast to create proofs once you get confident with the commands. Since it's a CLI, you avoid many mouse movements, and so far I've preferred this design over editor-based proof assistants.

> 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.

Depending on the decidability of GL (which I don't know), one could attempt writing tactics in Rumm as well. However, the resulting proofs would likely be longer than the ones done by hand (and they might need work variables, which Rumm doesn't have).

> 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.

Perhaps I can explain my way of thinking a bit, since sources for a proof of Day 20 seem to be scarce (spoilers start here):

Statement of Day 20: |- ( []. ( ( []. ph -> ph ) -> -. []. []. F. ) -> []. []. F. )

In general, when I approach propositional logic statements, I reduce them to what's called 'implicational normal form'. It doesn’t seem to be as popular as the conjunctive and disjunctive counterparts, but it's probably more efficient for statements that already use primitive symbols. In case someone is interested in learning this strategy, I made a propositional theorem prover that uses it https://groups.google.com/g/metamath/c/Dlc-Lf7MF1A (it can also be used as a SAT solver). Any pure propositional logic statement can be reduced to a set of statements in implicational normal form, and while it does not guarantee success when we go beyond that, it's still worth trying in some cases.

The first step of this strategy is to attempt to "split" nested hypotheses, in this case we have ( ( []. ph -> ph ) -> -. []. []. F. ) which can be split into a conjunction of two expressions ( ( -. []. ph -> -. []. []. F. ) /\ ( ph -> -. []. []. F. ) ). Such step is equivalent to applying ~jaob, but using implication instead of disjunction. We also know that the box operator distributes over conjunction (theorem ~distrconj), so we can fully split the hypothesis of Day 20 into two simpler ones:

|- ( []. ( -. []. ph -> -. []. []. F. ) -> ( []. ( ph -> -. []. []. F. ) -> []. []. F. ) )

With ~axk4 and ~ax-distrb we can change the second hypothesis to:

|- ( []. ( -. []. ph -> -. []. []. F. ) -> ( []. ( []. ph -> []. -. []. []. F. ) -> []. []. F. ) )

Why did I do this to the second hypothesis? Two reasons: the first is that we now have '[]. -. []. []. F.', which is an instance of  '[]. -. []. ph'. The latter is known to be "strong" because we can prove any other boxed expression from it. This property is expressed by ~kurbis, and for Day 20 we use the equivalent variant: |- ( []. -. []. ph -> []. ps ). Of course, gaining strong hypotheses is something we usually want to see in our proof developement. The second reason is that we get '[]. ph' on one hypothesis and '-. []. ph' on another, which could be combined to obtain a contradiction (ending with ~luk-3) if we manage to pair them together.

Now we reduce the goal to a set of statements in implicational normal form. The straightforward way of doing it would be to apply ~ex and ~monimpconj to first eliminate external boxes:

|- ( ( ( -. []. ph -> -. []. []. F. ) /\ ( []. ph -> []. -. []. []. F. ) ) -> []. F. )

And then split hypotheses with ~ja to get 4 statements in implicational normal form:

|- ( -. -. []. ph -> ( -. []. ph -> []. F. ) ) ----> ~com12 and ~luk-3

|- ( -. -. []. ph -> ( []. -. []. []. F. -> []. F. ) ) ----> ~a1i and ~kurbis

|- ( -. []. []. F. -> ( -. []. ph -> []. F. ) ) ----> ????
|- ( -. []. []. F. -> ( []. -. []. []. F. -> []. F. ) ) -----> ~a1i and ~kurbis

Unfortunately, one of those four statements cannot be proved (all of them need to be provable), so something went wrong. This was the step that took me the longest to figure out, but the basic principle is that we need to insert another step before arriving at the implicational normal form. The fix is to apply ~syl and ~ax-gl to the conclusion before applying ~monimpconj. The reason of doing that is that we gain another hypothesis (which is []. []. F.):

|- ( ( []. ( -. []. ph -> -. []. []. F. ) /\ []. ( []. ph -> []. -. []. []. F. ) ) -> []. ( []. []. F. -> []. F. ) )

We apply ~monimpconj to eliminate external boxes:

|- ( ( ( -. []. ph -> -. []. []. F. ) /\ ( []. ph -> []. -. []. []. F. ) ) -> ( []. []. F. -> []. F. ) )

And finally, we split the hypotheses with ~ja:

|- ( -. -. []. ph -> ( -. []. ph -> ( []. []. F. -> []. F. ) ) ) -----> ~com12 and ~luk-3.

|- ( -. -. []. ph -> ( []. -. []. []. F. -> ( []. []. F. -> []. F. ) ) ) ----> ~a1i, ~a1d and ~kurbis.

|- ( -. []. []. F. -> ( -. []. ph -> ( []. []. F. -> []. F. ) ) ) ----> ~a1d, ~com12 and ~luk-3.

|- ( -. []. []. F. -> ( []. -. []. []. F. -> ( []. []. F. -> []. F. ) ) ) -----> ~a1i, ~a1d and ~kurbis.

All statements in implicational normal form are now provable, so we have a proof of Day 20.

[savask]

> I don't know about metamath lamp, but the search power of the metamath.exe 'improve' command is very minimal.

Lamp uses depth 4 by default, but I'm not sure whether it corresponds to metamath's depth 4. It is able to fill in some basic steps occasionally, though often it doesn't behave as I expect it to behave.

> Depending on the decidability of GL (which I don't know), one could attempt writing tactics in Rumm as well.

It is decidable, some sort of procedure is described in Boolos' chapter 10, though I haven't looked at it in detail. As for Rumm, I would love to contribute some tactics but my general feeling is that we no longer have a "widely accepted" and actively-developed proof assistant: mmj2 is abandoned, metamath-exe is also almost abandoned, metamath-knife seems to be stagnant as well with many pull requests lying around for years. This is probably a theme for another topic, but does anyone uses Rumm in their set.mm work?

> Perhaps I can explain my way of thinking a bit, since sources for a proof of Day 20 seem to be scarce (spoilers start here):

Thanks a lot!

[Igor Ieskov]

> Lamp uses depth 4 by default, but I'm not sure whether it corresponds to metamath's depth 4.

You can change this value on the Settings tab. For example, I usually use 100 as the default value for depth. The value to use depends on your browser settings and Metamath database you are working with. If you start getting out-of-memory errors or your browser becomes unresponsive, then you should decrease the default depth. But if this doesn’t happen, then you are fine to use bigger values of depth. Usually bigger values of depth don’t make much difference, but occasionally you can find a proof which would be impossible to find with smaller values of depth. So, I would recommend using bigger values of depth if this doesn’t cause any issues with your browser.

> It is able to fill in some basic steps occasionally, though often it doesn't behave as I expect it to behave.

Can you describe one or few such cases when lamp doesn't behave as you expect? I will try to find an explanation to lamp’s behavior, and check if it is not a bug.

[Antony Bartlett]

On Fri, Dec 5, 2025 at 2:22 AM Gino Giotto <ginogiott...@gmail.com> wrote:

> The thing I like metamath.exe isn't automation, but rather that it's fast to create proofs once you get confident with the commands. Since it's a CLI, you avoid many mouse movements, and so far I've preferred this design over editor-based proof assistants.

Which reminds me, I started learning Vim Motions to avoid mouse movements, and would like to persist but haven't got around to it.  In terms of writing proofs, that would probably then be done in Visual Studio Code with the Yamma, and Vim (vscodevim, 8 million downloads) extensions installed and enabled.

The advantages of this is that I'd be learning a way to avoid mouse movements when editing any kind of text file, not just for proof writing activities, and I'd be able to start my proofs at the beginning or middle.

The disadvantage is that you're already very comfortable with metamath.exe as a proof assistant, and I wouldn't contemplate a change either under those circumstances! :-)

I don't really feel any particular discomfort when I'm crashing around with a mouse and keyboard, but I've made a live coding video or two, and re-watching myself crashing around *is* rather painful ;-)

    Best regards,

        Antony

[savask]

> Can you describe one or few such cases when lamp doesn't behave as you expect? I will try to find an explanation to lamp’s behavior, and check if it is not a bug.

Usually lamp wouldn't be able to figure out some step which uses a theorem from christmas25.mm. Once I do that step manually, it is able to fill in the rest of the proof (of course I tried switching the "Less" and "LessEq" settings to "unrestricted"). Now in hindsight I think that I should have saved a couple of proofs like that to serve as an example for you :-( I'll make sure to open an issue if I stumble upon such a proof again.