Inference Behaviour Semantics (IBS) is a new approach to Proof-Theoretic Semantics, grounded in two core principles: (1) an expression’s use in reasoning determines its meaning, and (2) a connective is defined by its operational rules. IBS defines the meaning of a connective by measuring the structural resources needed to use it. This talk outlines the methodology for deriving IBS and presents results for all connectives definable in standard two-dimensional sequent calculi.

We begin by analysing and formalizing all parameters of operational rules. We then introduce inferential behaviour as a syntactic metric for connective use. By systematically restricting these parameters within minimal definability proofs, we identify the most compact combination that preserves a connective’s inferential behaviour. The operational rules derived from these parameters provide the semantic clauses for the connectives in IBS.

We prove IBS for all connectives definable in two-dimensional sequent calculi. Our findings paint a fine-grained, local, and modular understanding of connective meaning, shedding new light on the semantic relations among logics.