Prawitz's Conjecture is False; So What?

TL;DR

This paper examines the implications of recent results challenging Prawitz's conjecture, arguing that superintuitionistic inferences remain valid due to limitations in current treatments of atomic formulas, and proposes a resolution.

Contribution

It critically analyzes recent findings against proof-theoretic validity and offers a solution to preserve the validity of superintuitionistic inferences.

Findings

Recent results challenge Prawitz's conjecture

Superintuitionistic inferences are valid despite these results

A proposed resolution addresses the treatment of atomic formulas

Abstract

Several recent results bring into focus the superintuitionistic nature of most notions of proof-theoretic validity, but little work has been done evaluating the consequences of these results. Proof-theoretic validity claims to offer a formal explication of how inferences follow from the definitions of logic connectives (which are defined by their introduction rules). This paper explores whether the new results undermine this claim. It is argued that, while the formal results are worrying, superintuitionistic inferences are valid because the treatments of atomic formulas are insufficiently general, and a resolution to this issue is proposed.