English

Uniform validity of atomic Split rule in monotonic proof-theoretic semantics

Logic 2026-02-17 v2

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 the atomic Split rule logically valid over miP-tV, thus implying the incompleteness of IL over a Prawitzian (monotonic, introduction-based) framework strictly understood.

Keywords

Cite

@article{arxiv.2503.19930,
  title  = {Uniform validity of atomic Split rule in monotonic proof-theoretic semantics},
  author = {Antonio Piccolomini d'Aragona},
  journal= {arXiv preprint arXiv:2503.19930},
  year   = {2026}
}
R2 v1 2026-06-28T22:34:14.662Z