Post #785488

2026-03-23 15:15 UTC

A monomial ordering is a total order on ℕ^r making ℕ^r into an ordered monoid, i.e. 0 &lt;= m for all m and m &lt;= m&#39; implies m + n &lt;= m&#39; + n for all m, m&#39;, n. Classically, every monomial ordering is a well-ordering (algebra people like to deduce this from Hilbert&#39;s basis theorem). Is it true constructively that every monomial ordering is well-founded, i.e. allows well-founded induction? Feel free to boost if you have constructive people in your bubble 😅

Replies (4)

@jdw@mathstodon.xyz 2026-04-09 06:04

@soaproot @antoinechambertloir @dwarn It appears that my question has a positive answer as per Proposition 3.13 in this paper: https://www.sciencedirect.com/science/article/pii/S074771710880154X?via%3Dihub

Open ##1368979
@antoinechambertloir@mathstodon.xyz 2026-03-23 15:31

@jdw that would be true for all of the specific monomial orderings I know of, but I'm not sure about the general case.

Open ##1368980
@dwarn@mathstodon.xyz 2026-03-23 15:56

@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

Open ##1368984
@soaproot@sfba.social 2026-03-23 23:58

@jdw I'm a bit over my head on this one. https://en.wikipedia.org/wiki/Monomial_order seems to be.... uh wrong or about a different topic?

Open ##1368986