×

Decidable fragments of the simple theory of types with infinity and NF. (English) Zbl 1417.03271

Summary: 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 \(\phi\) in the language of type theory that is in one of the following forms:
(A)
\(\phi=\forall x_{1}^{r_{1}}\dots \forall x_{k}^{r_{k}}\exists y_{1}^{s_{1}}\dots \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)
\(\phi=\forall x_{1}^{r_{1}}\dots \forall x_{k}^{r_{k}}\exists y_{1}^{s}\dots \exists y_{l}^{s}\theta\) where the superscripts denote the types of the variables and \(\theta\) is quantifier-free.
This shows that 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}\dots \forall x_{k}\exists y_{1}\dots \exists y_{l}\theta\) where \(\theta\) is quantifier-free and \(\phi\) admits a stratification that assigns distinct values to all of the variables \(y_{1},\dots,y_{l}\),
(B\('\))
\(\phi=\forall x_{1}\dots \forall x_{k}\exists y_{1}\dots \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},\dots,y_{l}\).

MSC:

03E70 Nonclassical and second-order set theories
03B25 Decidability of theories and sets of sentences
03B15 Higher-order logic; type theory (MSC2010)
PDFBibTeX XMLCite
Full Text: DOI arXiv Euclid