Sundholm's explanation of meaning: logical atavism and the nature of proofs

TL;DR

Sundholm's semantics rejects the traditional object-language/metalevel distinction and treats formal languages as meaningful from the outset, extending this contentful stance to proof formalisms. The paper develops a constructive, Martin-Löf-inspired interpretation that connects BHK-style notions of proof with Gentzen's Natural Deduction, distinguishing 1935 derivations as gestures toward proof-objects and 1936 derivations as proof-traces of proof-acts. A key contribution is the Curry-Howard-compatible account linking derivations to dependent proof-objects and showing how extraction procedures allow moving between objects and acts, thereby illuminating the syntax-semantics relationship in proof theory. The work highlights the philosophical payoff of a contentful, atavistic approach for understanding meaning in logic and its practical implications for interpreting formal proofs and their normalization.

Abstract

I provide an overview of some of Sundholm's remarks on the history and philosophy of logic. In particular, I focus on Sundholm's proposal to explain meaning with no object-language/metalanguage distinction, and to provide a consequently contentual approach to formalisms for proofs. When applied to Gentzen's Natural Deduction in its two 1935 and 1936 variants, this triggers a reading of each variant as pointing to one of the poles in the distinction between proof-objects and proof-acts, also introduced by Sundholm. I suggest that the basis of this picture is given by a Martin-Loefian reading of the notion of analytic assertion.