Josef Berger ; Helmut Schwichtenberg - A bound for Dickson's lemma

lmcs:3954 - Logical Methods in Computer Science, September 26, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:30)2017
A bound for Dickson's lemmaArticle

Authors: Josef Berger ; Helmut Schwichtenberg

    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.


    Volume: Volume 13, Issue 3
    Published on: September 26, 2017
    Accepted on: September 26, 2017
    Submitted on: September 26, 2017
    Keywords: Mathematics - Logic,03F60

    Consultation statistics

    This page has been seen 1610 times.
    This article's PDF has been downloaded 423 times.