Decreasing sentences in Simple Type Theory
Panagiotis Rouvelas · Mathematical logic quarterly · 2017
Abstract We present various results regarding the decidability of certain sets of sentences by Simple Type Theory ( ). 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 ( ); 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 . Namely, the decidability of (a subset of Σ1) and (the set of all sentences , 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” ( ) and its weak subtheory .