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

### All Science Journal Classification (ASJC) codes

- Logic
- History and Philosophy of Science

## Fingerprint Dive into the research topics of 'A Reduction Rule for Peirce Formula'. Together they form a unique fingerprint.

## Cite this

Hirokawa, S., Komori, Y., & Takeuti, I. (1996). A Reduction Rule for Peirce Formula.

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