Classical Brouwer-Heyting-Kolmogorov Interpretation

Abstract

The Brouwer-Heyting-Kolmogorov interpretation explains the meaning of logical operations as operators that construct proofs from proofs of the operands. The BHK interpretation is usually understood as giving intuitionistic interpretation for the logical operators, but, as pointed out by Troelstra and van Dalen [12], it is possible to understand the BHK interpretation classically. We elaborate this idea and develop a classical theory of proofs as abstract mathematical entities where the truth of a proposition becomes equivalent to the existence of proofs of the proposition. We develop a first order theory of arithmetic, equivalent to PA, and give a classical BHK interpretation for the theory. We show the soundness of the interpretation by showing that if a derivation P of a formula. A is given, then the interpretation of P is a proof of the interpretation of A. We also show that the interpreted value of derivations is preserved under reductions of derivations. We also present a system of catch/throw calculus and develop a classical BHK interpretation for it. Since the calculus in non-deterministic, we interpret a derivation by a set of proofs. We show the soundness of the interpretation, and show that if a derivation reduces to another derivation, then the associated set of proofs for the latter derivation is smaller than that for the former derivation.