Church–Rosser property of a simple reduction for full first-order classical natural deduction Original Research Article

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