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.
All Science Journal Classification (ASJC) codes