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