The First-Order Hypothetical Logic of Proofs

GABRIELA STEREN; EDUARDO BONELLI

JOURNAL OF LOGIC AND COMPUTATION

OXFORD UNIV PRESS

Lugar: Oxford; Año: 2017 vol. 27 p. 1023 - 1066

0955-792X

The Propositional Logic of Proofs (LP) is a modal logic in which the modality $Box A$ is revisited as alid{t}{A}, $t$ being an expression that bears witness to the validity of $A$. It enjoys arithmetical soundness and completeness, can realize all SIV theorems and is capable of reflecting its own proofs ($dash A$ implies $dash [![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 alid{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 normalisation is given.