Decreasing sentences in Simple Type Theory

We present various results regarding the decidability of certain sets of sentences by Simple Type Theory ( TST ). First, we introduce the notion of decreasing sentence, and prove that the set of decreasing sentences is undecidable by Simple Type Theory with infinitely many zero‐type elements ( TST ∞ ); a result that follows directly from the fact that every sentence is equivalent to a decreasing sentence. We then establish two different positive decidability results for a weak subtheory of TST ∞ . Namely, the decidability of∃ ¯( ( ∀ b ∃ ¯ ) b∀ ¯ b ) ∧ , ∨(a subset of Σ 1 ) and∃ ¯ STDEC (the set of all sentences ∃ x ¯ φ ( x ¯ ) , where φ is strictly decreasing). Finally, we present some consequences for the set of existential‐universal sentences. All the above results have direct implications for Quine's theory of “New Foundations” ( NF ) and its weak subtheory NFO .