Arithmetical Completeness of the Intuitionistic Logic of Proofs
Evgenij Vladimirovich Dashkov · Journal of Logic and Computation · 2009
Classical logic of proofs LP naturally extends propositional calculus to the language enriched with formulas meaning t is a proof of formula F. Intuitionistic logic of proofs iLP introduced by Artemov and Iemhoff was conjectured to be complete with respect to intuitionistic arithmetic HA. The article presents a proof of this conjecture.