zbMATH — the first resource for mathematics

Church-Rosser property of a simple reduction for full first-order classical natural deduction. (English) Zbl 1016.03006
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.

03B10 Classical first-order logic
03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
Full Text: DOI
[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
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.