Intuitionistic Logic of Proofs with dependent proof terms
Title | Intuitionistic Logic of Proofs with dependent proof terms |
Publication Type | Technical Report |
Year of Publication | 2012 |
Authors | Primiero, G |
Series Title | Preprint Series of the Isaac Newton Institute for Mathematical Sciences |
Abstract | The basic logic of proofs extends the usual propositional language by expressions of the form "s is a proof of A", for any proposition A. In this paper we explore the extension of its intuitionistic fragment to a language including expressions of the form "t is a proof of B, dependent from sbeing a proof of A". We aim at laying down a ground comparison with equivalent constructions present in theories of dependent types, especially those similarly based on the Brouwer-Heyting-Kolmogorov semantics. We further translate this extended language to a natural deduction calculus which allows for a double interpretation of the construction on which a proof term may depend: as actually proven, or valid assumption, or as possibly proven, locally true assumption. We show meta-theoretical properties for this calculus and explain normalisation to a language with only unconditional proofs. We conclude by stating the characterization of our calculus with standard intutionistic logic of proofs |
Citation Key | Prim_Intu_lo |