Virtual Evidence: A Constructive Semantics for Classical Logics

TL;DR

This paper develops a constructive semantics for classical logic using refinement types and virtual evidence, bridging the gap between classical and constructive reasoning with computational meaning.

Contribution

It introduces a new axiom for virtual evidence that preserves constructive semantics within classical logic using refinement types.

Findings

Provides a formal semantics for classical logic in constructive type theory.

Shows that classical truth can be explained through constructive evidence without oracles.

Demonstrates the computational meaning of classical logical operators.

Abstract

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