Journal of Logic and Computation Advance Access published online on August 17, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp041
Original Papers |
Arithmetical Completeness of the Intuitionistic Logic of Proofs
Department of Mathematical Logic and Theory of Algorithms, Faculty of Mechanics and Mathematics, Lomonosov Moscow State University, Moscow 119992, Russia.
E-mail: edashkov{at}gmail.com
Received 3 February 2009.
| Abstract |
|---|
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.
Keywords: Logic of proofs; intuitionistic arithmetic; admissible rules