A normalization-procedure for the first order classical natural deduction with full logical symbols (Q1904467)

The author describes a normalization procedure for a natural deduction formulation of classical first-order logic [see \textit{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); \textit{B. R. Boričić}, J. Philos. Logic 14, 359-377 (1985; Zbl 0572.03033); \textit{J. P. Seldin}, Stud. Logica 48, 193- 217 (1989; Zbl 0692.03007); \textit{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.