{
  "id": "1406.4384",
  "version": "v1",
  "published": "2014-06-17T14:34:35.000Z",
  "updated": "2014-06-17T14:34:35.000Z",
  "title": "Decidable fragments of the Simple Theory of Types with Infinity and NF",
  "authors": [
    "Anuj Dawar",
    "Thomas Forster",
    "Zachiri McKenzie"
  ],
  "comment": "19 pages",
  "categories": [
    "math.LO"
  ],
  "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$.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2014-06-17T14:34:35.000Z"
    }
  ],
  "analyses": {
    "keywords": [
      "simple theory",
      "decidable fragments",
      "set theory",
      "quantifier-free",
      "superscripts denote"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 19,
      "language": "en",
      "license": "arXiv",
      "status": "editable",
      "adsabs": "2014arXiv1406.4384D"
    }
  }
}