## Berger, Josef and Schwichtenberg, Helmut - A bound for Dickson's lemma

lmcs:3954 - Logical Methods in Computer Science, September 26, 2017, Volume 13, Issue 3
A bound for Dickson's lemma

Authors: Berger, Josef and Schwichtenberg, Helmut

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.

Source : oai:arXiv.org:1503.03325
DOI : 10.23638/LMCS-13(3:30)2017
Volume: Volume 13, Issue 3
Published on: September 26, 2017
Submitted on: September 26, 2017
Keywords: Mathematics - Logic,03F60