Room 206 (2nd floor, badged access)
25 November 2026 - 15h00
Constructive Substitutes for Kőnig’s Lemma
by Dominique Larchey-Wendling from LORIA - CNRS
invited by Jean-Francois MONIN
25 November 2026 - 15h00
Constructive Substitutes for Kőnig’s Lemma
by Dominique Larchey-Wendling from LORIA - CNRS
invited by Jean-Francois MONIN
Abstract: We propose weaker but constructively provable variants of the contrapositive of Kőnig’s lemma. We derive those from a generalization of the FAN theorem for inductive bars to inductive covers, for which we give a concise proof. We compare the positive, negative and sequential characterizations of covers and bars in classical and constructive contexts, giving precise accounts of the role played by the axioms of excluded middle and dependent choice. As an application, we discuss some examples where the use of Kőnig’s lemma can be replaced by one of our weaker variants to obtain fully constructive accounts of results or proofs that could otherwise appear as inherently classical.
See https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2024.2
