On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains
Author: Federico Aschieri
Paper Information
| Title: | On Natural Deduction for Herbrand Constructive Logics III: The Strange Case of the Intuitionistic Logic of Constant Domains |
| Authors: | Federico Aschieri |
| Proceedings: | CL&C Full papers and abstracts |
| Editor: | Stefano Berardi |
| Keywords: | Natural deduction, Curry-Howard, Intuitionistic logic of constant domains |
| Abstract: | ABSTRACT. The logic of constant domains is intuitionistic logic extended with the so-called forall-shift axiom, a classically valid statement which implies the excluded middle over decidable formulas. Surprisingly, this logic is constructive and so far this has been proved by cut-elimination for ad-hoc sequent calculi. Here we use the methods of natural deduction and Curry-Howard correspondence to provide a simple computational interpretation of the logic. |
| Pages: | 9 |
| Talk: | Jul 07 14:00 (Session 28A) |
| Paper: | ![]() |
