Decidable Fragments of the Simple Theory of Types with Infinity and $mathrm{NF}$

Notre Dame Journal of Formal Logic 58 (3):433-451 (2017)
  Copy   BIBTEX

Abstract

We identify complete fragments of the simple theory of types with infinity and Quine’s new foundations set theory. We show that TSTI decides every sentence ϕ in the language of type theory that is in one of the following forms: ϕ=∀x1r1⋯∀xkrk∃y1s1⋯∃ylslθ where the superscripts denote the types of the variables, s1>⋯>sl, and θ is quantifier-free, ϕ=∀x1r1⋯∀xkrk∃y1s⋯∃ylsθ where the superscripts denote the types of the variables and θ is quantifier-free. This shows that NF decides every stratified sentence ϕ in the language of set theory that is in one of the following forms: ϕ=∀x1⋯∀xk∃y1⋯∃ylθ where θ is quantifier-free and ϕ admits a stratification that assigns distinct values to all of the variables y1,…,yl, ϕ=∀x1⋯∀xk∃y1⋯∃ylθ where θ is quantifier-free and ϕ admits a stratification that assigns the same value to all of the variables y1,…,yl.

Other Versions

No versions found

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 98,169

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2017-04-21

Downloads
51 (#341,896)

6 months
11 (#271,177)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Thomas Forster
Cambridge University

Citations of this work

Increasing sentences in Simple Type Theory.Panagiotis Rouvelas - 2017 - Annals of Pure and Applied Logic 168 (10):1902-1926.

Add more citations

References found in this work

New Foundations for Mathematical Logic.W. V. Quine - 1937 - Journal of Symbolic Logic 2 (2):86-87.
The strength of Mac Lane set theory.A. R. D. Mathias - 2001 - Annals of Pure and Applied Logic 110 (1-3):107-234.
Term models for weak set theories with a universal set.T. E. Forster - 1987 - Journal of Symbolic Logic 52 (2):374-387.

Add more references