Reduction in first-order logic compared with reduction in implicational logic
AbstractIn this paper we discuss strong normalization for natural deduction in the →∀-fragment of first-order logic. The method of collapsing types is used to transfer the result (concerning strong normalization) from implicational logic to first-order logic. The result is improved by a complement, which states that the length of any reduction sequence of derivation term r in first-order logic is equal to the length of the corresponding reduction sequence of its collapse term rc in implicational logic.
How to Cite
GALOYAN, Tigran M.. Reduction in first-order logic compared with reduction in implicational logic. The Australasian Journal of Logic, [S.l.], v. 5, nov. 2007. ISSN 1448-5052. Available at: <https://ojs.victoria.ac.nz/ajl/article/view/1785>. Date accessed: 18 july 2019. doi: https://doi.org/10.26686/ajl.v5i0.1785.