On Natural Deduction for Herbrand Constructive Logics I: Curry-Howard Correspondence for Dummett's Logic LC
Logical Methods in Computer Science, Volume abs/1609.03190, 2017.
Dummettu0027s logic LC is intuitionistic logic extended with Dummettu0027s 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 Dummettu0027s logic. We add to the lambda calculus an operator which repr...More
PPT (Upload PPT)