Reduction in first-order logic compared with reduction in implicational logic

  • Tigran M. Galoyan Institute for Informatics and Automation Problems, National Academy of Sciences, Yerevan, Armenia

Abstract

In 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.

Author Biography

Tigran M. Galoyan, Institute for Informatics and Automation Problems, National Academy of Sciences, Yerevan, Armenia
Published
2007-11-08
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: 21 sep. 2019. doi: https://doi.org/10.26686/ajl.v5i0.1785.