Strong Normalization for First-order Logic

Abstract

logic. The use of the method of collapsing types to transfer the result concerning strong normalization (that is, any derivation r is strongly normalizable) from implicational logic to first-order logic is illustrated (ref [1]). The considered result is improved by a complement, which states that for any derivation r and its collapse rc we need the same number of one-step reductions (the !1 rule) to bring them to their normal forms. Our basic logic calculus is the!8-fragment of minimal natural deduction for first-order logic over simply typed lambda-terms. This restriction regarding the minimal fragment does not mean a loss in generality, since the full classical first-order logic can be embedded in this system by adding stability axiom. The method of collapsing types developed in [2] is used to get some results concerning the strong normalization of derivations in first-order logic.