TY - JOUR
T1 - The first-order hypothetical logic of proofs
AU - Steren, Gabriela
AU - Bonelli, Eduardo
N1 - Publisher Copyright:
© The Author, 2016.
PY - 2017/6/1
Y1 - 2017/6/1
N2 - 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.
AB - 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.
KW - Curry howard isomorphism
KW - First-order logic of proofs
KW - Lambda calculus
KW - Natural deduction
UR - http://www.scopus.com/inward/record.url?scp=85026884902&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85026884902&partnerID=8YFLogxK
U2 - 10.1093/logcom/exv090
DO - 10.1093/logcom/exv090
M3 - Article
AN - SCOPUS:85026884902
SN - 0955-792X
VL - 27
SP - 1023
EP - 1066
JO - Journal of Logic and Computation
JF - Journal of Logic and Computation
IS - 4
ER -