Strong normalization proofs for cut elimination in Gentzen’s sequent calculi. (English) Zbl 0945.03083

Tahhan Bittar, Elias

Niwiński, Damian (ed.) et al., Logic, algebra, and computer science. Helena Rasiowa in memoriam. Warszawa: Polish Academy of Sciences, Institute of Mathematics, Banach Cent. Publ. 46, 179-225 (1999).

A. G. Dragalin [Mathematical intuitionism (American Mathematical Society, Providence) (1988; Zbl 0634.03054); translation from the Russian original (Nauka, Moskva) (1979; Zbl 0439.03041)] gave a strong normalization proof for sequent L-systems when two cuts are never permuted. One of the proofs in the paper under review can be seen as a version of Dragalin’s proof for a more complicated but more uniform notation for derivations. The only information given for an inference rule in this notation is the number of premises and whether the rule is active or passive with respect to the cut. Another proof uses results from the theory of term rewriting systems.
For the entire collection see [Zbl 0913.00019].

Reviewer: G.Mints (Stanford)

MSC:

03F05

Cut-elimination and normal-form theorems

Keywords:

cut elimination; strong normalization; term rewriting systems