Following all the rules: Intuitionistic completeness for generalised proof-theoretic validity

TL;DR

This paper introduces a refined notion called generalized proof-theoretic validity, demonstrating that its associated logic is precisely intuitionistic logic, correcting previous misconceptions about proof-theoretic validity.

Contribution

It proposes a minor modification to the definition of proof-theoretic validity and proves that the resulting logic aligns exactly with intuitionistic logic.

Findings

Generalized proof-theoretic validity is closed under substitution.

The logic of generalized proof-theoretic validity is intuitionistic.

Refinement resolves previous disprovals of Prawitz's conjecture.

Abstract

Prawitz conjectured that the proof-theoretically valid logic is intuitionistic logic. Recent work on proof-theoretic validity has disproven this. In fact, it has been shown that proof-theoretic validity is not even closed under substitution. In this paper, we make a minor modification to the definition of proof-theoretic validity found in Prawitz (1973) and refined by Schroeder-Heister (2006). We will call the new notion generalised proof-theoretic validity and show that the logic of generalised proof-theoretic validity is intuitionistic logic.