Uniform validity of atomic Kreisel-Putnam rule in monotonic proof-theoretic semantics
Antonio Piccolomini d'Aragona
TL;DR
The paper investigates whether the known intuitionistic incompleteness results of base-extension semantics ($miB ext{-}eS$) extend to the monotonic, introduction-based proof-theoretic semantics ($miP ext{-}tV$). It distinguishes between primacy of consequence in $miB ext{-}eS$ and the derived nature of validity in $miP ext{-}tV$, exploring constructivity and uniformity of reductions. By constructing two uniform, constructive reductions, it establishes the logical validity of atomic Kreisel-Putnam within $miP ext{-}tV$, thereby demonstrating incompleteness of $IL$ in the strict Prawitzian framework. The work also analyzes the role of substitution-closure and admissibility conditions, arguing that while $aKP$ can be forced to be valid under certain constructions, a general closure under substitutions does not hold in this setting. Overall, the results illuminate fundamental differences between proof-theoretic validity and standard semantic completeness and offer concrete reductions that witness incompleteness under Prawitz-style semantics.
Abstract
Proof-theoretic semantics (PTS) is normally understood today as Base-Extension Semantics (B-eS), i.e., as a theory of proof-theoretic consequence over atomic proof systems. Intuitionistic logic (IL) has been proved to be incomplete over a number of variants of B-eS, including a monotonic one where introduction rules play a prior role (miB-eS). In its original formulation by Prawitz, however, PTS consequence is not a primitive, but a derived notion. The main concept is that of argument structure valid relative to atomic systems and assignments of reductions for eliminating generalised detours of inferences in non-introduction form. This is called Proof-Theoretic Validity (P-tV), and it can be given in a monotonic and introduction-based form too (miP-tV). It is unclear whether, and under what conditions, the incompleteness results proved for IL over miB-eS can be transferred to miP-tV. As has been remarked, the main problem seems to be that the notion of argumental validity underlying the miB-eS notion of consequence is one where reductions are either forced to be non-uniform, or non-constructive. Building on some Prawitz-fashion incompleteness proofs for IL based on the notion of (intuitionistic) construction, I provide in what follows a set of reductions which are surely uniform (however uniformity is defined) and constructive, and which make atomic Kreisel-Putnam rule logically valid over miP-tV, thus implying the incompleteness of IL over a Prawitzian (monotonic, introduction-based) framework strictly understood.