zbMATH — the first resource for mathematics

A normalization-procedure for the first order classical natural deduction with full logical symbols. (English) Zbl 0835.03021
The author describes a normalization procedure for a natural deduction formulation of classical first-order logic [see D. Prawitz: Natural deduction – A proof theoretical study (1965; Zbl 0173.00205), and Proc. Second Scandinav. Logic Symp. 1970, Stud. Logic Found. Math. 63, 235-307 (1971; Zbl 0226.02031); B. R. Boričić, J. Philos. Logic 14, 359-377 (1985; Zbl 0572.03033); J. P. Seldin, Stud. Logica 48, 193- 217 (1989; Zbl 0692.03007); G. Stålmarck, J. Symb. Logic 56, 129-149 (1991; Zbl 0735.03028)]. The reduction procedure presented here can be considered as a natural extension of Prawitz’s reduction procedure, but on the full set of logical symbols.

03F05 Cut-elimination and normal-form theorems
03B10 Classical first-order logic
Full Text: DOI