Repository | Journal | Volume | Articles
(2006) Synthese 148 (3).
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.
Publication details
DOI: 10.1007/s11229-004-6298-z
Full citation:
Sundholm, G. (2006). Semantic values for natural deduction derivations. Synthese 148 (3), pp. 623-638.
This document is unfortunately not available for download at the moment.