A note on schematic validity and completeness in Prawitz's semantics

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.