TR-2005002: The Basic Intuitionistic Logic of Proofs
Sergei Nikolaevich Artemov, Rosalie Iemhoff · CUNY Academic Works (City University of New York) · 2005
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.