Virtual evidence: A constructive semantics for classical logics
RL Constable - arXiv preprint arXiv:1409.0266, 2014 - arxiv.org
RL Constable
arXiv preprint arXiv:1409.0266, 2014•arxiv.orgThis article presents a computational semantics for classical logic using constructive type
theory. Such semantics seems impossible because classical logic allows the Law of
Excluded Middle (LEM), not accepted in constructive logic since it does not have
computational meaning. However, the apparently oracular powers expressed in the LEM,
that for any proposition P either it or its negation, not P, is true can also be explained in terms
of constructive evidence that does not refer to" oracles for truth." Types with virtual evidence …
theory. Such semantics seems impossible because classical logic allows the Law of
Excluded Middle (LEM), not accepted in constructive logic since it does not have
computational meaning. However, the apparently oracular powers expressed in the LEM,
that for any proposition P either it or its negation, not P, is true can also be explained in terms
of constructive evidence that does not refer to" oracles for truth." Types with virtual evidence …
This article presents a computational semantics for classical logic using constructive type theory. Such semantics seems impossible because classical logic allows the Law of Excluded Middle (LEM), not accepted in constructive logic since it does not have computational meaning. However, the apparently oracular powers expressed in the LEM, that for any proposition P either it or its negation, not P, is true can also be explained in terms of constructive evidence that does not refer to "oracles for truth." Types with virtual evidence and the constructive impossibility of negative evidence provide sufficient semantic grounds for classical truth and have a simple computational meaning. This idea is formalized using refinement types, a concept of constructive type theory used since 1984 and explained here. A new axiom creating virtual evidence fully retains the constructive meaning of the logical operators in classical contexts. Key Words: classical logic, constructive logic, intuitionistic logic, propositions-as-types, constructive type theory, refinement types, double negation translation, computational content, virtual evidence
arxiv.org
Showing the best result for this search. See all results