Processing math: 100%
Communication Dans Un Congrès Année : 2021

On the logical structure of choice and bar induction principles

Résumé

We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an "intensional" or "effective" view of respectively ill-and well-foundedness properties to an "extensional" or "ideal" view of these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain A, a codomain B and a "filter" T on finite approximations of functions from A to B, a generalised form GDCA,B,T of the axiom of dependent choice and dually a generalised bar induction principle GBIA,B,T such that: - GDCA,B,T intuitionistically captures the strength of • the general axiom of choice expressed as aβR(a,b)αaR(α,(aα(a))) when T is a filter that derives point-wise from a relation R on A×B without introducing further constraints, • the Boolean Prime Filter Theorem / Ultrafilter Theorem if B is the two-element set B (for a constructive definition of prime filter), • the axiom of dependent choice if A=N, • Weak König’s Lemma if A=N and B=B (up to weak classical reasoning) - GBIA,B,T intuitionistically captures the strength of • Gödel’s completeness theorem in the form validity implies provability for entailment relations if B=B, • bar induction when A=N, • the Weak Fan Theorem when A=N and B=B. Contrastingly, even though GDCA,B,T and GBIA,B,T smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when A is BN and B is N.
Fichier principal
Vignette du fichier
lics.pdf (354.81 Ko) Télécharger le fichier
Origine Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03144849 , version 1 (17-02-2021)
hal-03144849 , version 2 (15-03-2021)
hal-03144849 , version 3 (12-05-2021)
hal-03144849 , version 4 (18-06-2021)
hal-03144849 , version 5 (05-07-2022)

Identifiants

Citer

Nuria Brede, Hugo Herbelin. On the logical structure of choice and bar induction principles. LICS 2021 - 36th Annual Symposium on Logic in Computer Science, Jun 2021, Rome / Virtual, Italy. ⟨hal-03144849v5⟩
419 Consultations
603 Téléchargements

Altmetric

Partager

More