Decidable fragments of the Simple Theory of Types with Infinity and NF

Anuj Dawar, Thomas Forster, Zachiri McKenzie

We identify complete fragments of the Simple Theory of Types with Infinity ($\mathrm{TSTI}$) and Quine's $\mathrm{NF}$ set theory. We show that $\mathrm{TSTI}$ decides every senten…