Logics of Proof-Theoretic Validity

Abstract In proof-theoretic semantics, the validity of atomic formulas is defined as their derivability in systems of atomic rules. We distinguish two types of such systems and two variants of semantics of formulas, one based on introduction rules for logical constants and one based on elimination rules. We thus define four semantics with their respective consequence relations. As these are not necessarily closed under substitution of arbitrary formulas for atoms, we consider the substitution-closed subsets of these four consequence relations in addition. We show which logics, in the sense of formal systems, are complete for seven of these notions. This systematizes in one place four previous results with three new results. For the semantics based on elimination rules intuitionistic or classical logic is complete, depending on the type of atomic rules, whereas the semantics based on introduction rules characterize intermediate logics. This answers several open questions about the main notions of proof-theoretic validity, although for one semantics of the introduction rule type we can only make a conjecture about possible logics. Further notions of proof-theoretic validity are suggested by considering alternative systems of atomic rules from the perspective of logic programming.