3 papers
cs.LO2026
On the logical structure of choice and bar induction principles
Nuria Brede, Hugo Herbelin
We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an ''intensional'' or ''effective'' view of respe…
cs.LO2025
A parametricity-based formalization of semi-simplicial and semi-cubical sets
Hugo Herbelin, Ramkumar Ramachandra
Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alterna…
math.LO2024
An analysis of the constructive content of Henkin's proof of Gödel's completeness theorem
Hugo Herbelin, Danko Ilik
G{ö}del's completeness theorem for classical first-order logic is one of the most basic theorems of logic. Central to any foundational course in logic, it connects the notion of v…