4 papers
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 va…
Applications of the analogy between formulas and exponential polynomials to equivalence and normal forms
Danko Ilik
We show some applications of the formulas-as-polynomials correspondence: 1) a method for (dis)proving formula isomorphism and equivalence based on showing (in)equality; 2) a constr…
Perspectives for proof unwinding by programming languages techniques
Danko Ilik
In this chapter, we propose some future directions of work, potentially beneficial to Mathematics and its foundations, based on the recent import of methodology from the theory of…
An Intuitionistic Formula Hierarchy Based on High-School Identities
Taus Brock-Nannestad, Danko Ilik
We revisit the notion of intuitionistic equivalence and formal proof representations by adopting the view of formulas as exponential polynomials. After observing that most of the i…