The basic intuitionistic logic of proofs
Sergei Nikolaevich Artemov, Rosalie Iemhoff · Journal of Symbolic Logic · 2007
Abstract The language of the basic logic of proofs extends the usual propositional language by forming sentences of the sort x is a proof of F for any sentence F. In this paper a complete axiomatization for the basic logic of proofs in Heyting Arithmetic HA was found.