A Reduction Rule for Peirce Formula

Sachio Hirokawa, Yuichi Komori, Izumi Takeuti

Research output: Contribution to journalArticle

Abstract

A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a λ-calculus with a new constant p((α→β)→α)→α. It is shown that all terms with the same type are equivalent with respect to β-reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for βP-reduction. Weak normalization is shown for βP-reduction with another reduction rule which simplifies α of ((α → β) → α) → α into an atomic type.

Original languageEnglish
Pages (from-to)419-426
Number of pages8
JournalStudia Logica
Volume56
Issue number3
DOIs
Publication statusPublished - Jan 1 1996

Fingerprint

Figure
Strong Normalization
Classical Logic
Term
Normalization
Simplify
Calculus
Calculi

All Science Journal Classification (ASJC) codes

  • Logic
  • History and Philosophy of Science

Cite this

A Reduction Rule for Peirce Formula. / Hirokawa, Sachio; Komori, Yuichi; Takeuti, Izumi.

In: Studia Logica, Vol. 56, No. 3, 01.01.1996, p. 419-426.

Research output: Contribution to journalArticle

Hirokawa, S, Komori, Y & Takeuti, I 1996, 'A Reduction Rule for Peirce Formula', Studia Logica, vol. 56, no. 3, pp. 419-426. https://doi.org/10.1007/BF00372774
Hirokawa, Sachio ; Komori, Yuichi ; Takeuti, Izumi. / A Reduction Rule for Peirce Formula. In: Studia Logica. 1996 ; Vol. 56, No. 3. pp. 419-426.
@article{6fa7d07c80294f0ba0b69865167c63ec,
title = "A Reduction Rule for Peirce Formula",
abstract = "A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a λ-calculus with a new constant p((α→β)→α)→α. It is shown that all terms with the same type are equivalent with respect to β-reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for βP-reduction. Weak normalization is shown for βP-reduction with another reduction rule which simplifies α of ((α → β) → α) → α into an atomic type.",
author = "Sachio Hirokawa and Yuichi Komori and Izumi Takeuti",
year = "1996",
month = "1",
day = "1",
doi = "10.1007/BF00372774",
language = "English",
volume = "56",
pages = "419--426",
journal = "Studia Logica",
issn = "0039-3215",
publisher = "Springer Netherlands",
number = "3",

}

TY - JOUR

T1 - A Reduction Rule for Peirce Formula

AU - Hirokawa, Sachio

AU - Komori, Yuichi

AU - Takeuti, Izumi

PY - 1996/1/1

Y1 - 1996/1/1

N2 - A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a λ-calculus with a new constant p((α→β)→α)→α. It is shown that all terms with the same type are equivalent with respect to β-reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for βP-reduction. Weak normalization is shown for βP-reduction with another reduction rule which simplifies α of ((α → β) → α) → α into an atomic type.

AB - A reduction rule is introduced as a transformation of proof figures in implicational classical logic. Proof figures are represented as typed terms in a λ-calculus with a new constant p((α→β)→α)→α. It is shown that all terms with the same type are equivalent with respect to β-reduction augmented by this P-reduction rule. Hence all the proofs of the same implicational formula are equivalent. It is also shown that strong normalization fails for βP-reduction. Weak normalization is shown for βP-reduction with another reduction rule which simplifies α of ((α → β) → α) → α into an atomic type.

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

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

U2 - 10.1007/BF00372774

DO - 10.1007/BF00372774

M3 - Article

AN - SCOPUS:53349109377

VL - 56

SP - 419

EP - 426

JO - Studia Logica

JF - Studia Logica

SN - 0039-3215

IS - 3

ER -