Logical Metainferentialism

Logical inferentialism is the view that the meaning of logical constants is implicitly defined by the operational rules that govern their behaviour in proofs—particularly in sequent calculus proofs, according to an increasingly dominant tendency. A tenable articulation of this view presupposes a clarification of certain crucial aspects, such as the criteria for rule harmony and what constitutes a normal proof. Sequent calculus inferentialists typically frame these aspects in terms of proofs from axioms, rather than derivations from assumptions. Logical metainferentialism calls into question this dogma, building on the idea, advocated in “The original sin of proof-theoretic semantics” (Dicher & Paoli 2021), that meaning determination is relative to sequent-to-sequent derivability relations of Gentzen systems. We advance a suggestion towards a metainferentially appropriate reformulation of harmony, and explore its potential by focussing on a case study, the calculi for FDE and its extensions.