Proof-theoretic Semantics for Second-order Logic

TL;DR

This paper introduces a proof-theoretic semantics for second-order logic that offers an inferentialist alternative to traditional model-theoretic interpretations, emphasizing meaning through inferential roles rather than set-theoretic commitments.

Contribution

It develops a modular, inferentialist semantics for second-order logic based on base-extension semantics, unifying classical and intuitionistic variants and aligning with Henkin's approach.

Findings

Provides soundness and completeness results for Hilbert-style calculi

Reframes second-order quantification as substitution rather than set-theoretic commitment

Offers a lightweight, expressive semantics grounded in inferential roles

Abstract

We develop a proof-theoretic semantics (P-tS) for second-order logic (S-oL), providing an inferentialist alternative to both full and Henkin model-theoretic interpretations. Our approach is grounded in base-extension semantics (B-eS), a framework in which meaning is determined by inferential roles relative to atomic systems -- collections of rules that encode an agent's pre-logical inferential commitments. We show how both classical and intuitionistic versions of S-oL emerge from this set-up by varying the class of atomic systems. These systems yield modular soundness and completeness results for corresponding Hilbert-style calculi, which we prove equivalent to Henkin's account of S-oL. In doing so, we reframe second-order quantification as systematic substitution rather than set-theoretic commitment, thereby offering a philosophically lightweight yet expressive semantics for higher-order logic. This work contributes to the broader programme of grounding logical meaning in use rather than reference and offers a new lens on the foundations of logic and mathematics.