Federico Aschieri (Institut für Logic and Computation Technische Universität Wien) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.281.1 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |