Following all the rules: intuitionistic completeness for generalized proof-theoretic validity

Will Stafford; Victor Nascimento

doi:10.1093/analys/anac100

Following all the rules: intuitionistic completeness for generalized proof-theoretic validity

Will Stafford^*, Victor Nascimento^*

^*Corresponding author for this work

School of Mathematics

Research output: Contribution to journal › Article (Academic Journal) › peer-review

2 Citations (Scopus)

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’s 1973 paper ‘Towards a foundation of a general proof theory’ and refined by Schroeder-Heister in ‘Validity concepts in proof-theoretic semantics’ (2006 ). We will call the new notion generalized proof-theoretic validity and show that the logic of generalized proof-theoretic validity is intuitionistic logic.

Original language	English
Article number	anac100
Pages (from-to)	507-516
Number of pages	10
Journal	Analysis
Volume	83
Issue number	3
Early online date	19 Jul 2023
DOIs	https://doi.org/10.1093/analys/anac100
Publication status	E-pub ahead of print - 19 Jul 2023

Bibliographical note

Funding Information:
Dr Stafford was supported by a Lumina quaeruntur fellowship [LQ300092101] from the Czech Academy of Sciences. Mr Nascimento’s work was financed in part by the Coordenação de Aperfeiçoamento de Pessoal de Nível Superior – Brasil (CAPES) – [Finance Code 001].

Access to Document

10.1093/analys/anac100Licence: CC BY-NC-ND

https://academic.oup.com/analysis/advance-article/doi/10.1093/analys/anac100/7226592

Handle.net

Persistent link

Cite this

@article{a6808cf71320492ab8e3cfc9dd2c8648,

title = "Following all the rules: intuitionistic completeness for generalized proof-theoretic validity",

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{\textquoteright}s 1973 paper {\textquoteleft}Towards a foundation of a general proof theory{\textquoteright} and refined by Schroeder-Heister in {\textquoteleft}Validity concepts in proof-theoretic semantics{\textquoteright} (2006 ). We will call the new notion generalized proof-theoretic validity and show that the logic of generalized proof-theoretic validity is intuitionistic logic.",

author = "Will Stafford and Victor Nascimento",

note = "Funding Information: Dr Stafford was supported by a Lumina quaeruntur fellowship [LQ300092101] from the Czech Academy of Sciences. Mr Nascimento{\textquoteright}s work was financed in part by the Coordena{\c c}{\~a}o de Aperfei{\c c}oamento de Pessoal de N{\'i}vel Superior – Brasil (CAPES) – [Finance Code 001]. ",

year = "2023",

month = jul,

day = "19",

doi = "10.1093/analys/anac100",

language = "English",

volume = "83",

pages = "507--516",

journal = "Analysis",

issn = "0003-2638",

publisher = "Oxford University Press",

number = "3",

}

TY - JOUR

T1 - Following all the rules

T2 - intuitionistic completeness for generalized proof-theoretic validity

AU - Stafford, Will

AU - Nascimento, Victor

N1 - Funding Information: Dr Stafford was supported by a Lumina quaeruntur fellowship [LQ300092101] from the Czech Academy of Sciences. Mr Nascimento’s work was financed in part by the Coordenação de Aperfeiçoamento de Pessoal de Nível Superior – Brasil (CAPES) – [Finance Code 001].

PY - 2023/7/19

Y1 - 2023/7/19

N2 - 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’s 1973 paper ‘Towards a foundation of a general proof theory’ and refined by Schroeder-Heister in ‘Validity concepts in proof-theoretic semantics’ (2006 ). We will call the new notion generalized proof-theoretic validity and show that the logic of generalized proof-theoretic validity is intuitionistic logic.

AB - 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’s 1973 paper ‘Towards a foundation of a general proof theory’ and refined by Schroeder-Heister in ‘Validity concepts in proof-theoretic semantics’ (2006 ). We will call the new notion generalized proof-theoretic validity and show that the logic of generalized proof-theoretic validity is intuitionistic logic.

U2 - 10.1093/analys/anac100

DO - 10.1093/analys/anac100

M3 - Article (Academic Journal)

SN - 0003-2638

VL - 83

SP - 507

EP - 516

JO - Analysis

JF - Analysis

IS - 3

M1 - anac100

ER -

Following all the rules: intuitionistic completeness for generalized proof-theoretic validity

Abstract

Bibliographical note

Access to Document

Handle.net

Fingerprint

Cite this