带无穷公理的简单类型论与 NF 的可判定片段

我们识别了带无穷公理的简单类型论 ($\mathrm{TSTI}$) 和 Quine 的$\mathrm{NF}$集合论的完备片段。我们证明了$\mathrm{TSTI}$可判定类型论语言中具有以下形式之一的每个句子$\phi$：(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$，其中上标表示变量的类型，$s_1 > \ldots > s_l$且$\theta$无量词；(B) $\phi= \forall x_1^{r_1} \cdots \forall x_k^{r_k} \exists y_1^{s} \cdots \exists y_l^{s} \theta$，其中上标表示变量的类型且$\theta$无量词。这表明$\mathrm{NF}$可判定集合论语言中具有以下形式之一的每个分层句子$\phi$：(A') $\phi= \forall x_1 \cdots \forall x_k \exists y_1 \cdots \exists y_l \theta$，其中$\theta$无量词且$\phi$允许一种分层，该分层为所有变量$y_1, \ldots, y_l$分配不同的值；(B') $\phi= \forall x_1 \cdots \forall x_k \exists y_1 \cdots \exists y_l \theta$，其中$\theta$无量词且$\phi$允许一种分层，该分层为所有变量$y_1, \ldots, y_l$分配相同的值。