Postponement of raa and Glivenko’s Theorem, Revisited

Giulio Guerrieri, Alberto Naibo

Research output: Contribution to journalArticle

Abstract

We study how to postpone the application of the reductio ad absurdum rule ((Formula presented.)) in classical natural deduction. This technique is connected with two normalization strategies for classical logic, due to Prawitz and Seldin, respectively. We introduce a variant of Seldin’s strategy for the postponement of (Formula presented.), which induces a negative translation (a variant of Kuroda’s one) from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.

Original languageEnglish
Pages (from-to)1-36
Number of pages36
JournalStudia Logica
DOIs
Publication statusE-pub ahead of print - 9 Mar 2018

Keywords

  • Natural deduction
  • Negative translation
  • Proof theory
  • Reductio ad absurdum.

ASJC Scopus subject areas

  • Logic
  • History and Philosophy of Science

Cite this

Postponement of raa and Glivenko’s Theorem, Revisited. / Guerrieri, Giulio; Naibo, Alberto.

In: Studia Logica, 09.03.2018, p. 1-36.

Research output: Contribution to journalArticle

@article{c758f405df7f466ba2629c95e323cfc1,
title = "Postponement of raa and Glivenko’s Theorem, Revisited",
abstract = "We study how to postpone the application of the reductio ad absurdum rule ((Formula presented.)) in classical natural deduction. This technique is connected with two normalization strategies for classical logic, due to Prawitz and Seldin, respectively. We introduce a variant of Seldin’s strategy for the postponement of (Formula presented.), which induces a negative translation (a variant of Kuroda’s one) from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.",
keywords = "Natural deduction, Negative translation, Proof theory, Reductio ad absurdum.",
author = "Giulio Guerrieri and Alberto Naibo",
year = "2018",
month = "3",
day = "9",
doi = "10.1007/s11225-017-9781-5",
language = "English",
pages = "1--36",
journal = "Studia Logica",
issn = "0039-3215",
publisher = "Springer Verlag",

}

TY - JOUR

T1 - Postponement of raa and Glivenko’s Theorem, Revisited

AU - Guerrieri, Giulio

AU - Naibo, Alberto

PY - 2018/3/9

Y1 - 2018/3/9

N2 - We study how to postpone the application of the reductio ad absurdum rule ((Formula presented.)) in classical natural deduction. This technique is connected with two normalization strategies for classical logic, due to Prawitz and Seldin, respectively. We introduce a variant of Seldin’s strategy for the postponement of (Formula presented.), which induces a negative translation (a variant of Kuroda’s one) from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.

AB - We study how to postpone the application of the reductio ad absurdum rule ((Formula presented.)) in classical natural deduction. This technique is connected with two normalization strategies for classical logic, due to Prawitz and Seldin, respectively. We introduce a variant of Seldin’s strategy for the postponement of (Formula presented.), which induces a negative translation (a variant of Kuroda’s one) from classical to intuitionistic and minimal logic. Through this translation, Glivenko’s theorem from classical to intuitionistic and minimal logic is proven.

KW - Natural deduction

KW - Negative translation

KW - Proof theory

KW - Reductio ad absurdum.

UR - http://www.scopus.com/inward/record.url?scp=85043385720&partnerID=8YFLogxK

U2 - 10.1007/s11225-017-9781-5

DO - 10.1007/s11225-017-9781-5

M3 - Article

SP - 1

EP - 36

JO - Studia Logica

JF - Studia Logica

SN - 0039-3215

ER -