Abstract
The logic of proofs is a refinement of modal logic introduced by Artemov in 1995 in which the modality {white medium square}A is revisited as?t?A where t is an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness and is capable of reflecting its own proofs ({assertion}A implies {assertion}?t?A, for some t). We develop the Hypothetical Logic of Proofs, a reformulation of LP based on judgemental reasoning.
Original language | English |
---|---|
Pages (from-to) | 103-140 |
Number of pages | 38 |
Journal | Logica Universalis |
Volume | 8 |
Issue number | 1 |
DOIs | |
State | Published - Mar 2014 |
Keywords
- Curry-Howard isomorphism
- Modal logic
- lambda Mu-calculus
- lambda calculus
- logic of proofs
- natural deduction