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.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 74,429

External links

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

Through your library

Similar books and articles

Axiomatizability by {{\ Forall}{\ Exists}!}-Sentences.Miguel Campercholi & Diego Vaggione - 2011 - Archive for Mathematical Logic 50 (7-8):713-725.
Determinacy in Strong Cardinal Models.P. D. Welch - 2011 - Journal of Symbolic Logic 76 (2):719 - 728.
Power-Like Models of Set Theory.Ali Enayat - 2001 - Journal of Symbolic Logic 66 (4):1766-1782.
The Pure Part of $Mathrm{HYP}(Mathscr{M}$).Mark Nadel & Jonathan Stavi - 1977 - Journal of Symbolic Logic 42 (1):33-46.
The Consistency Strength of an Infinitary Ramsey Property.George Kafkoulis - 1994 - Journal of Symbolic Logic 59 (4):1158-1195.
Storage Operators and Forall-Positive Types of System TTR.Karim Nour - 1996 - Mathematical Logic Quarterly 42:349-368.
Conservative Fragments of {{S}^{1} {2}} and {{R}^{1} {2}}.Chris Pollett - 2011 - Archive for Mathematical Logic 50 (3-4):367-393.
A Small Reflection Principle for Bounded Arithmetic.Rineke Verbrugge & Albert Visser - 1994 - Journal of Symbolic Logic 59 (3):785-812.

Analytics

Added to PP
2017-04-21

Downloads
22 (#515,852)

6 months
1 (#417,143)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

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