Post #1368984
2026-03-23 15:56 UTC
@jdw I guess this is related to "Dickson's lemma" which has an intuitionistic proof according to [1], with the caveat that [1] talks about infinite sequences rather than well-founded induction.
According to [2, Corollary 2.4], you can show that an ordering R is well-founded by showing that in the classifying topos of "an infinite R-decreasing chain", false holds. This *should* close the gap between your question and the claim in [1], but there is surely a more direct answer. There's quite a lot of literature on this type of "constructive Ramsey theory".
[1] W. Veldman, An intuitionistic proof of Kruskal’s theorem
[2] https://www.speicherleck.de/iblech/stuff/early-draft-modal-multiverse.pdf
Replies (1)
-
@jdw@mathstodon.xyz 2026-03-23 16:33
@dwarn Thanks! I couldn't yet connect everything, but using your keyword Dickson's lemma I found it interesting that Cox, Little, O'Shea in their very nice book Ideals, Varieties and Algorithms call Dickson's lemma the statement that every ideal generated by monomials in a polynomial ring over a field is finitely generated. They give a direct proof (not referring to Hilbert's basis theorem), but at first sight it doesn't seem to be fully constructive. (Btw, there is a recent 5th edition from 2025 of their book, as I just found out.)