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

Abstract

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 sentence $\varphi$ in the language of type theory that is in one of the following forms: (A) $\varphi =\forall x_1^{r_1}\cdots \forall x_k^{r_k}\exists y_1^{s_1}\cdots \exists y_l^{s_l}\theta$ where the superscripts denote the types of the variables, $s_1>\dots >s_l$ and $\theta$ is quantifier-free, (B) $\varphi =\forall x_1^{r_1}\cdots \forall x_k^{r_k}\exists y_1^s\cdots \exists y_l^s\theta$ where the superscripts denote the types of the variables and $\theta$ is quantifier-free. This shows that $\mathrm{NF}$ decides every stratified sentence $\varphi$ in the language of set theory that is in one of the following forms: (A') $\varphi =\forall x_1\cdots \forall x_k\exists y_1\cdots \exists y_l\theta$ where $\theta$ is quantifier-free and $\varphi$ admits a stratification that assigns distinct values to all of the variable $y_1,\dots ,y_l$, (B') $\varphi =\forall x_1\cdots \forall x_k\exists y_1\cdots \exists y_l\theta$ where $\theta$ is quantifier-free and $\varphi$ admits a stratification that assigns the same value to all of the variables $y_1,\dots ,y_l$.

arXiv comment19 pages