Abstract
The Propositional Logic of Proofs (LP) is a modal logic in which the modality □A is revisited as [[t]]A, t being an expression that bears witness to the validity of A. It enjoys arithmetical soundness and completeness, can realize all S4 theorems and is capable of reflecting its own proofs (⊢A implies ⊢[[t]]A, for some t). A presentation of first-order LP has recently been proposed, FOLP, which enjoys arithmetical soundness and has an exact provability semantics. A key notion in this presentation is how free variables are dealt with in a formula of the form [[t]]A(i). We revisit this notion in the setting of a Natural Deduction presentation and propose a Curry-Howard correspondence for FOLP. A term assignment is provided and a proof of strong normalization is given.
| Original language | English |
|---|---|
| Pages (from-to) | 1023-1066 |
| Number of pages | 44 |
| Journal | Journal of Logic and Computation |
| Volume | 27 |
| Issue number | 4 |
| DOIs | |
| State | Published - Jun 1 2017 |
ASJC Scopus subject areas
- Software
- Theoretical Computer Science
- Logic
- Arts and Humanities (miscellaneous)
- Hardware and Architecture
Keywords
- Curry howard isomorphism
- First-order logic of proofs
- Lambda calculus
- Natural deduction