Classical logic as limit completion
Stefano Berardi · Mathematical Structures in Computer Science · 2005
We define a constructive model for -maps, that is, maps recursively definable from a map deciding the halting problem. Our model refines an existing constructive interpretation for classical reasoning over one-quantifier formulas: it is compositional (Modus Ponens is interpreted as an application) and semantical (rather than translating classical proofs into intuitionistic ones, we define a mathematical structure intuitionistically validating excluded middle for one-quantifier formulas).