The basic intuitionistic logic of proofs

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.

• Type: Journal
• Year: 2007
• Where: JSYML
• Authors: Sergei N. Artëmov, Rosalie Iemhoff
• Keywords: Basic Logic, JSYML 2007, Sentence F, Usual Propositional Language