eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2024-02-07
16:1
16:17
10.4230/LIPIcs.CSL.2024.16
article
A General Constructive Form of Higman’s Lemma
Berardi, Stefano
1
https://orcid.org/0000-0001-5427-0020
Buriola, Gabriele
2
Schuster, Peter
2
Dipartimento di Informatica, Università di Torino, Italy
Dipartimento di Informatica, Università di Verona, Italy
In logic and computer science one often needs to constructivize a theorem ∀ f ∃ g.P(f,g), stating that for every infinite sequence f there is an infinite sequence g such that P(f,g). Here P is a computable predicate but g is not necessarily computable from f. In this paper we propose the following constructive version of ∀ f ∃ g.P(f,g): for every f there is a "long enough" finite prefix g₀ of g such that P(f,g₀), where "long enough" is expressed by membership to a bar which is a free parameter of the constructive version.
Our approach with bars generalises the approaches to Higman’s lemma undertaken by Coquand-Fridlender, Murthy-Russell and Schwichtenberg-Seisenberger-Wiesnet. As a first test for our bar technique, we sketch a constructive theory of well-quasi orders. This includes yet another constructive version of Higman’s lemma: that every infinite sequence of words has an infinite ascending subsequence. As compared with the previous constructive versions of Higman’s lemma, our constructive proofs are closer to the original classical proofs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol288-csl2024/LIPIcs.CSL.2024.16/LIPIcs.CSL.2024.16.pdf
intuitionistic logic
constructive mathematics
formal proof
inductive predicate
bar induction
well quasi-order
Higman’s lemma