Semantic values for natural deduction derivations

Göran Sundholm

pp. 623-638

in: Proof-theoretic semantics, Synthese 148 (3), 2006.

Abstract

Drawing upon Martin-Löf’s semantic framework for his constructive type theory, semantic values are assigned also to natural-deduction derivations, while observing the crucial distinction between (logical) consequence among propositions and inference among judgements. Derivations in Gentzen’s (1934–5) format with derivable formulae dependent upon open assumptions, stand, it is suggested, for proof-objects (of propositions), whereas derivations in Gentzen’s (1936) sequential format are (blue-prints for) proof-acts.