Sophie Nagler | Searcharxiv

arXiv2026

Towards Automated Proof-Theoretic Semantics: Inference-Behaviour Semantics for 3-Dimensional K3 and LP

Inference-behaviour Semantics (I-bS) is a sequent calculus-based substructural approach to proof-theoretic semantics (P-tS), focussed on modelling the relationships of connective meanings across different logics. This paper provides a case study of how I-bS can be extended to any finitely multi-dimensional sequent calculus. To this end, we give I-bS for the 3-dimensional sequent calculi K3 (Strong Kleene) and LP (Logic of Paradox). We find that the K3 and LP connectives have the same meaning and that their meaning conservatively extends the meaning of the corresponding classical LK connectives. We situate this result within the wider project of integrating I-bS with MUltlog. The goal is to automate the generation of I-bS for arbitrary multi-valued logics using a MUltlog-style system, thus contributing towards the computational automation of P-tS approaches.

cs.LO↗

arXiv2026

Inference-Behaviour Semantics for All$^\ast$ Connectives in Two-Dimensional Sequent Calculi

Inference-behaviour semantics (I-bS) is a new approach to proof-theoretic semantics, grounded in two inferentialist principles: (1) the use of an expression in reasoning determines its meaning, and (2) a connective is defined by its operational rules. I-bS operationalises these ideas by measuring the syntactic use of a connective in the proof of its definability, against a substructurally minimal derivability relation. I-bS thereby gives the meaning of a connective in terms of its semantic clause, i.e. minimal substructural rule pair. This paper validates and verifies I-bS by applying it to all $10,816$ connective rule pairs that can be formulated in two-dimensional sequent calculi using at most two premiss sequents and at most two active formulae. As a result, we find semantic clauses for exactly $21$ meaningful connectives, namely bottom, top, two negations (intuitionistic and dual-intuitionistic), group and lattice conjunction, disjunction and implication, as well as their converses and inverses. We use these results to precisely map the semantic interrelations among the connectives, across linear, classical, intuitionistic, dual-intuitionistic, minimal, and lattice logic. Most notably, we find that intuitionistic negation, disjunction and implication each capture half of the meaning of their classical counterparts.

cs.LO↗