{
  "id": "1705.05021",
  "version": "v1",
  "published": "2017-05-14T19:36:01.000Z",
  "updated": "2017-05-14T19:36:01.000Z",
  "title": "Algebraic New Foundations",
  "authors": [
    "Paul Gorbow"
  ],
  "categories": [
    "math.LO"
  ],
  "abstract": "New Foundations ($\\mathrm{NF}$) is a set theory obtained from naive set theory by putting a stratification constraint on the comprehension schema; for example, it proves that there is a universal set $V$. $\\mathrm{NFU}$ ($\\mathrm{NF}$ with atoms) is known to be consistent through its close connection with models of conventional set theory that admit automorphisms. A first-order theory, $\\mathrm{ML}_\\mathrm{CAT}$, in the language of categories is introduced and proved to be equiconsistent to $\\mathrm{NF}$ (analogous results are obtained for intuitionistic and classical $\\mathrm{NF}$ with and without atoms). $\\mathrm{ML}_\\mathrm{CAT}$ is intended to capture the categorical content of the predicative class theory of $\\mathrm{NF}$. $\\mathrm{NF}$ is interpreted in $\\mathrm{ML}_\\mathrm{CAT}$ through the categorical semantics. Thus, the result enables application of category theoretic techniques to meta-mathematical problems about $\\mathrm{NF}$ -style set theory. For example, an immediate corollary is that $\\mathrm{NF}$ is equiconsistent to $\\mathrm{NFU} + |V| = |\\mathcal{P}(V)|$. This is already proved by Crabb\\'e, but becomes intuitively obvious in light of the results of this paper. Just like a category of classes has a distinguished subcategory of small morphisms, a category modelling $\\mathrm{ML}_\\mathrm{CAT}$ has a distinguished subcategory of type-level morphisms. This corresponds to the distinction between sets and proper classes in $\\mathrm{NF}$. With this in place, the axiom of power objects familiar from topos theory can be appropriately formulated for $\\mathrm{NF}$. It turns out that the subcategory of type-level morphisms contains a topos as a natural subcategory.",
  "revisions": [
    {
      "version": "v1",
      "updated": "2017-05-14T19:36:01.000Z"
    }
  ],
  "analyses": {
    "subjects": [
      "03G30",
      "03E35",
      "18C50",
      "03C62"
    ],
    "keywords": [
      "foundations",
      "conventional set theory",
      "distinguished subcategory",
      "style set theory",
      "category theoretic techniques"
    ],
    "note": {
      "typesetting": "TeX",
      "pages": 0,
      "language": "en",
      "license": "arXiv",
      "status": "editable"
    }
  }
}