Search

• < Previous
• 1
• Next >

---

Interactive Learning-Based Realizability for Heyting Arithmetic with EM1

Federico Aschieri ; Stefano Berardi.

We apply to the semantics of Arithmetic the idea of ``finite approximation'' used to provide computational interpretations of Herbrand's Theorem, and we interpret classical proofs as constructive proofs (with constructive rules for $\vee, \exists$) over a suitable structure $\StructureN$ for the&nbsp;[&hellip;]

---

On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC

Federico Aschieri.

Dummett's logic LC is intuitionistic logic extended with Dummett's axiom: for every two statements the first implies the second or the second implies the first. We present a natural deduction and a Curry-Howard correspondence for first-order and second-order Dummett's logic. We add to the lambda&nbsp;[&hellip;]

---