Premium
Decreasing sentences in Simple Type Theory
Author(s) -
Rouvelas Panagiotis
Publication year - 2017
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.201500093
Subject(s) - decidability , undecidable problem , simple (philosophy) , mathematics , sentence , quine , type (biology) , set (abstract data type) , type theory , discrete mathematics , computer science , natural language processing , philosophy , epistemology , ecology , biology , programming language
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 .