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.
Download data is not yet available.
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: 24 jan. 2020. doi: https://doi.org/10.26686/ajl.v5i0.1785.