Decidability in Proof-Theoretic Validity

Proof-theoretic validity has proven a useful tool for proof-theoretic semantics, because it explains the harmony found in the introduction and elimination rules for the intuitionistic calculus. However, the demonstration that a rule of proof is proof-theoretically valid requires checking an infinite number of cases, which raises the question of whether proof-theoretic validity is decidable. It is proven here that it is for the most prominent formulations in the literature for propositional logic.