Constructive Combinatorics of Dickson's Lemma

TL;DR

This paper provides constructive proofs and bounds for Dickson's lemma, exploring finite and infinite cases within Bishop's constructive mathematics, and introduces new unprovability results.

Contribution

It offers novel constructive proofs with explicit bounds and investigates unprovability results for finite cases of Dickson's lemma.

Findings

Constructive proofs with extracted bounds for finite Dickson's lemma cases

New unprovability results for finite cases of Dickson's lemma

Analysis of infinite cases within Bishop's constructive mathematics

Abstract

We study constructively the relations between the finite cases of Dickson's lemma. Although there are many constructive proofs of them, the novel aspect of our proofs is the extraction of a corresponding bound. We provide some new one-step unprovability results i.e., results of the form "a finite case of Dickson's lemma does not prove in one step a stronger case of it". Moreover, we study the infinite cases of Dickson's lemma from the point of view of constructive reverse mathematics. We work within Bishop's informal system of constructive mathematics BISH.