2018/03/31 by Federico Aschieri
Mathematics · Computer Science · #math.LO #cs.LO
paper · pdf · doi:10.4204/eptcs.281.1
published as EPTCS 281, 2018, pp. 1-9 · In Proceedings CL&C 2018, arXiv:1810.05392
arxiv created 2018/10/18 · arxiv updated 2018/10/19
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.