A note on schematic validity and completeness in Prawitz's semantics
Antonio Piccolomini d'Aragona
TL;DR
This paper compares two monotonic proof-theoretic semantic frameworks—SVA, which grounds consequence in valid arguments with explicit justifications for non-introduction rules, and Base Semantics, which omits structural justifications and derives consequence from an atomic base. It shows that Base Semantics yields classical validity (e.g., $A \\lor \\\neg A$) and exhibits intuitionistic incompleteness, while the transfer of these results to SVA depends crucially on how reductions and justifications are treated. A central claim is that the schematicity of reductions can undermine the validity of classical logic within SVA, revealing that how justifications are understood is a key distinguishing feature of proof-theoretic validity. The paper further explores strategies to restore desirable properties (e.g., relaxing open validity or imposing linearity constraints) and outlines directions for formalizing schematic notions and considering alternative frameworks like ToG.
Abstract
I discuss two approaches to monotonic proof-theoretic semantics. In the first one, which I call SVA, consequence is understood in terms of existence of valid arguments. The latter involve the notions of argument structure and justification for arbitrary non-introduction rules. In the second approach, which I call Base Semantics, structures and justifications are left aside, and consequence is defined outright over background atomic theories. Many (in)completeness results have been proved relative to Base Semantics, the question being whether these can be extended to SVA. By limiting myself to a framework with classical meta-logic, I prove correctness of classical logic on Base Semantics, and show that this result adapts to SVA when justifications are allowed to be choice-functions over atomic theories or unrestricted reduction systems of argument structures. I also point out that, however, if justifications are required to be more schematic, correctness of classical logic over SVA may fail, even with classical logic in the meta-language. This seems to reveal that the way justifications are understood may be a distinguishing feature of different accounts of proof-theoretic validity.