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

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...

Full description

Bibliographic Details
Main Author: Federico Aschieri
Format: Article
Language:English
Published: Logical Methods in Computer Science e.V. 2017-04-01
Series:Logical Methods in Computer Science
Subjects:
Online Access:https://lmcs.episciences.org/2048/pdf