On the elimination of some higher type quantifiers
Yasuwo Ikeda, Kohji Tomita, Chiharu Hosono · Mathematical Structures in Computer Science · 2001
This paper concerns the elimination of higher type quantifiers and gives two theorems. The first theorem shows that quantifiers in formulae of a specific form can be eliminated. The second theorem shows that quantifiers in formulae of a similar form cannot be eliminated, that is, such formulae do not have an equivalent first-order formula. The proof is based on the Ehrenfeucht game. These theorems are important for design of an interpreter of a ν act, which is a representation of mathematical action. Moreover, even if the universe is assumed to be finite, these theorems hold.