A reduction rule for Peirce formula (Q1919985): Difference between revisions

It is well known that, via the Curry-Howard isomorphism, SK-combinators and their types also represent, respectively, proofs and theorems in intuitionistic implicational logic. The reduction rules for the combinators can be motivated by proof reductions. The authors of this paper introduce a new ``combinator'' P, with a type that corresponds to Peirce's Law, so that proofs of classical implicational logic can be represented using SKP-combinators. A reduction rule for P is motivated by a proof reduction in classical implicational logic. The addition of P and its reduction rule to untyped combinatory logic implies the equality of all combinators, so only the addition of typed Ps to typed combinatory logic is proposed. Even so, this system is neither Church-Rosser nor strongly normalizing and, in it, all combinators with the same type (such as the Church numerals) are provably equal. A weak normalization theorem can be proved when an additional reduction rule for P is added. Most of the paper uses lambda calculus notation, which can be translated into combinators. When this is done this new rule becomes particularly complicated.