TY - JOUR

T1 - Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms

AU - Gabbay, Murdoch

AU - Mulligan, Dominic P.

PY - 2010/3

Y1 - 2010/3

N2 - The Curry-Howard correspondence connects derivations in natural deduction with the lambda-calculus. Predicates are types, derivations are terms. This supports reasoning from assumptions to conclusions, but we may want to reason backwards; from the desired conclusion towards the assumptions. At intermediate stages we may have a partial derivation, with holes. This is natural in informal practice but it can be difficult to formalise. The informal act of filling holes in a partial derivation suggests a capturing substitution, since holes may occur in the scope of quantifier introduction rules. As other authors have observed, this is not immediately supported by the lambda-calculus. Also, universal quantification requires a 'fresh name' and it is not immediately obvious what formal meaning to assign to this notion if derivations are incomplete. Further issues arise with proof-normalisation; this corresponds with lambda-calculus reduction, which can require alpha-conversion to avoid capture when beta-reducing, and it is not immediately clear how to alpha-convert a name in an incomplete derivation. We apply a one-and-a-half level technique based on nominal terms to construct a Curry-Howard correspondence for first-order logic. This features two levels of variable, but with no lambda-abstraction at the second level. Predicates are types, derivations are terms, proof-normalisation is reduction - and the two levels of variable are, respectively, the assumptions and the holes of an incomplete derivation. We give notions of proof-term, typing, alpha-conversion and beta-reduction for our syntax. We prove confluence, we exhibit several admissible rules including a proof that instantiation of level two variables is type-safe - this corresponds with the act of filling holes in an incomplete derivation, and can be viewed as a form of Cut-rule - and we explore the connection with traditional Curry-Howard in the case that the derivation is in fact complete. Our techniques are not specifically tailored to first-order logic and the same ideas should be applicable without any essential new difficulties to similar logical systems. © 2009 Elsevier Inc. All rights reserved.

AB - The Curry-Howard correspondence connects derivations in natural deduction with the lambda-calculus. Predicates are types, derivations are terms. This supports reasoning from assumptions to conclusions, but we may want to reason backwards; from the desired conclusion towards the assumptions. At intermediate stages we may have a partial derivation, with holes. This is natural in informal practice but it can be difficult to formalise. The informal act of filling holes in a partial derivation suggests a capturing substitution, since holes may occur in the scope of quantifier introduction rules. As other authors have observed, this is not immediately supported by the lambda-calculus. Also, universal quantification requires a 'fresh name' and it is not immediately obvious what formal meaning to assign to this notion if derivations are incomplete. Further issues arise with proof-normalisation; this corresponds with lambda-calculus reduction, which can require alpha-conversion to avoid capture when beta-reducing, and it is not immediately clear how to alpha-convert a name in an incomplete derivation. We apply a one-and-a-half level technique based on nominal terms to construct a Curry-Howard correspondence for first-order logic. This features two levels of variable, but with no lambda-abstraction at the second level. Predicates are types, derivations are terms, proof-normalisation is reduction - and the two levels of variable are, respectively, the assumptions and the holes of an incomplete derivation. We give notions of proof-term, typing, alpha-conversion and beta-reduction for our syntax. We prove confluence, we exhibit several admissible rules including a proof that instantiation of level two variables is type-safe - this corresponds with the act of filling holes in an incomplete derivation, and can be viewed as a form of Cut-rule - and we explore the connection with traditional Curry-Howard in the case that the derivation is in fact complete. Our techniques are not specifically tailored to first-order logic and the same ideas should be applicable without any essential new difficulties to similar logical systems. © 2009 Elsevier Inc. All rights reserved.

UR - http://www.scopus.com/inward/record.url?scp=75449107729&partnerID=8YFLogxK

U2 - 10.1016/j.ic.2009.09.003

DO - 10.1016/j.ic.2009.09.003

M3 - Article

VL - 208

SP - 230

EP - 258

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 3

ER -