### 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 language | English |
---|---|

Pages (from-to) | 419-426 |

Number of pages | 8 |

Journal | Studia Logica |

Volume | 56 |

Issue number | 3 |

DOIs | |

Publication status | Published - Jan 1 1996 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Logic
- History and Philosophy of Science

### Cite this

*Studia Logica*,

*56*(3), 419-426. https://doi.org/10.1007/BF00372774

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

Research output: Contribution to journal › Article

*Studia Logica*, vol. 56, no. 3, pp. 419-426. https://doi.org/10.1007/BF00372774

}

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 -