Decidable Fragments of the Simple Theory of Types with Infinity and NF
Anuj Dawar, Thomas Forster, Zachiri McKenzie · Notre Dame Journal of Formal Logic · 2017
We identify complete fragments of the simple theory of types with infinity (TSTI) and Quine’s new foundations (NF) set theory. We show that TSTI decides every sentence ϕ in the language of type theory that is in one of the following forms: (A) ϕ=∀x1r1⋯∀xkrk∃y1s1⋯∃ylslθ where the superscripts denote the types of the variables, s1>⋯>sl, and θ is quantifier-free, (B) ϕ=∀x1r1⋯∀xkrk∃y1s⋯∃ylsθ where the superscripts denote the types of the variables and θ is quantifier-free. This shows that NF decides every stratified sentence ϕ in the language of set theory that is in one of the following forms: (A′) ϕ=∀x1⋯∀xk∃y1⋯∃ylθ where θ is quantifier-free and ϕ admits a stratification that assigns distinct values to all of the variables y1,…,yl, (B′) ϕ=∀x1⋯∀xk∃y1⋯∃ylθ where θ is quantifier-free and ϕ admits a stratification that assigns the same value to all of the variables y1,…,yl.