Justif ication logic and type theory as formalizations of intuitionistic propositional logic

摘要

We explore two ways of formalizing Kreisel’s addendum to the Brouwer–Heyting–Kolmogorov interpretation. To do this, we compare Artemov’s justification logic with simply typedλcalculus. First, we provide a completeness result for Kripke style semantics of the implicational fragment of the intuitionistic logic of proofs. Then we introduce a map from justification terms intoλterms, which can be viewed as a method of extracting the computational content of the justification terms. Then we examine the interpretation of Kreisel’s addendum in justification logic along with the image of the resulting justification terms under our map.