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

TL;DR

This paper identifies specific decidable fragments within the Simple Theory of Types with Infinity and Quine's NF set theory, expanding understanding of their logical boundaries and decision procedures.

Contribution

It establishes that certain classes of sentences in TSTI and NF are decidable, providing explicit forms and stratification conditions for these fragments.

Findings

TSTI decides all sentences of specific quantified forms with quantifier-free parts.

NF decides stratified sentences with particular variable assignment patterns.

The results delineate the boundaries of decidability in these foundational theories.

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 $\phi$ in the language of type theory that is in one of the following forms: (A) $\phi= \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 > \ldots > s_l$ and $\theta$ is quantifier-free, (B) $\phi= \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 $\phi$ in the language of set theory that is in one of the following forms: (A') $\phi= \forall x_1 \cdots \forall x_k \exists y_1 \cdots \exists y_l \theta$ where $\theta$ is quantifier-free and $\phi$ admits a stratification that assigns distinct values to all of the variable $y_1, \ldots, y_l$, (B') $\phi= \forall x_1 \cdots \forall x_k \exists y_1 \cdots \exists y_l \theta$ where $\theta$ is quantifier-free and $\phi$ admits a stratification that assigns the same value to all of the variables $y_1, \ldots, y_l$.