A bound for Dickson's lemma

TL;DR

This paper provides a simple combinatorial bound for a special case of Dickson's lemma using the pigeonhole principle, and extracts a computational bound from the proof.

Contribution

It introduces a new combinatorial bound for a specific case of Dickson's lemma and formalizes the proof to extract computational bounds.

Findings

Constructed a simple bound using combinatorial arguments

Derived a descent lemma based on the pigeonhole principle

Extracted a computational bound via realizability from the proof

Abstract

We consider a special case of Dickson's lemma: for any two functions $f,g$ on the natural numbers there are two numbers $i<j$ such that both $f$ and $g$ weakly increase on them, i.e., $f_i\le f_j$ and $g_i \le g_j$. By a combinatorial argument (due to the first author) a simple bound for such $i,j$ is constructed. The combinatorics is based on the finite pigeon hole principle and results in a descent lemma. From the descent lemma one can prove Dickson's lemma, then guess what the bound might be, and verify it by an appropriate proof. We also extract (via realizability) a bound from (a formalization of) our proof of the descent lemma. Keywords: Dickson's lemma, finite pigeon hole principle, program extraction from proofs, non-computational quantifiers.