2022/04/24 by Iosif Petrakis, Petrakis, Iosif · 1 citation
Computer Science · Mathematics · #Cellular Automata and Applications #Combinatorics (math.CO) #Computability, Logic, AI Algorithms #FOS: Mathematics #Mathematical and Theoretical Analysis
paper · pdf · doi:10.48550/arxiv.2204.11298
openalex publication_date 2022/04/24 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.