×

Remarks on the Church-Rosser property. (English) Zbl 0715.03025

By analogy with important results for lambda calculus and proof theory, the author shows that a reduction algebra is computable. E.g., a classical result of Church and Rosser on the uniqueness of the normal forms of the terms of the lambda calculus becomes: If a reduction algebra satisfies the Church-Rosser Property then it is semi-computable. Indeed, the author gives another proof of the strong normalization theorem for the impredicative second-order intuitionistic propositional calculus in a natural deduction scheme.
Reviewer: A.A.Mullin

MSC:

03F50 Metamathematics of constructive systems
03B40 Combinatory logic and lambda calculus
03F05 Cut-elimination and normal-form theorems
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Metamathematical investigation of intuitionistic arithmetic and analysis 344 (1973)
[2] Proceedings of the Second Scandinavian Logic Symposium pp 235– (1971) · Zbl 0219.02001
[3] Natural deduction. A proof theoretical study (1965) · Zbl 0173.00205
[4] The lambda calculus. Its syntax and semantics (1984)
[5] DOI: 10.1090/S0002-9947-1936-1501858-0 · JFM 62.0037.03
[6] Indagationes Mathematica 34 pp 381– (1972)
[7] Proceedings of the Second Scandinavian Logic Symposium pp 63– (1971)
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.