Church-Rosser property of a simple reduction for full first-order classical natural deduction. (English) Zbl 1016.03006

Andou, Y.

Ann. Pure Appl. Logic 119, No. 1-3, 225-237 (2003).

Summary: A system of typed terms which corresponds with the classical natural deduction with one conclusion and full logical symbols is defined. The Church-Rosser property of the system is proved using an extended method of parallel reduction.

MSC:

03B10	Classical first-order logic
03B40	Combinatory logic and lambda calculus
03F05	Cut-elimination and normal-form theorems

Keywords:

classical natural deduction; Church-Rosser property; parallel reduction

References:

[1]	Andou, Y., A normalization-procedure for the first order classical natural deduction with full logical symbols, Tsukuba J. math., 19, 153-162, (1995) · Zbl 0835.03021
[2]	Y. Andou, On a reduction-procedure for full first order classical natural deduction, Doctoral Thesis, University of Tsukuba, 1995. · Zbl 0835.03021
[3]	Andou, Y., A canonical extension of curry – howard isomorphism to classical logic, () · Zbl 1016.03006
[4]	K. Fujita, An interpretation of classical predicate logic in λμ-calculus, manuscript.
[5]	G. Gentzen, Untersuchungen über das logische Schliessen, Math. Z. 39 (1935) 176-210, 405-431. · Zbl 0010.14501
[6]	de Groote, P., On the strong normalization of natural deduction with premutation-conversions, (), 45-59 · Zbl 0939.03061
[7]	Hindley, J.R.; Seldin, J.P., Introduction to combinators and λ-calculus, (1986), Cambridge University Press Cambridge · Zbl 0614.03014
[8]	Parigot, M., λμ-calculus: an algorithmic interpretation of classical natural deduction, (), 190-201 · Zbl 0925.03092
[9]	Parigot, M., Classical proofs as programs, (), 263-277 · Zbl 0805.03012
[10]	M. Parigot, Strong normalization for second order classical natural deduction, in: Logic in Computer Science, LICS 1993, ed. M. Vardi, IEEE Computer Soci. Press, Silver Spring, MD, 1993, pp. 39-46.
[11]	Parigot, M., Proofs of strong normalization for second order classical natural deduction, J. symbolic logic, 62, 1461-1479, (1997) · Zbl 0941.03063
[12]	Prawitz, D., Natural deduction—A proof theoretical study, (1965), Almqvist & Wiksell Stockholm · Zbl 0173.00205
[13]	D. Prawitz, Ideas and results in proof theory, in: Proc. 2nd Scandinavian Logic Symp., North-Holland, Amsterdam, 1971, pp. 235-307. · Zbl 0226.02031
[14]	Takahashi, M., Parallel reduction in λ-calculus, Inform. comput., 118, 120-127, (1995) · Zbl 0827.68060
[15]	Troelstra, A.S.; Schwichtenberg, H., Basic proof theory, (1996), Cambridge University Press Cambridge · Zbl 0868.03024