A Reduction Rule for Peirce Formula
Source: Studia Logica, Volume 56, Number 3, May 1996 , pp. 419-426(8)
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.
Document Type: Regular Paper
Affiliations: 1: Computer Science Laboratory, Faculty of Science, Kyushu University, Ropponmatsu 4-2-1, Fukuoka 810 Japan, email@example.com 2: Department of Mathematics, Shizuoka University, Shizuoka 422 Japan, firstname.lastname@example.org 3: Department of Mathematics, Tokyo Metropolitan University, Minami-Ohsawa 1-1, Hachioji-shi, Tokyo 192-03 Japan, email@example.com
Publication date: May 1, 1996