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

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

Authors
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.
Keywords Quine’s $\mathrm{NF}$   universal-existential sentences  simple theory of types
Categories (categorize this paper)
DOI 10.1215/00294527-2017-0009
Options
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive


Upload a copy of this paper     Check publisher's policy     Papers currently archived: 45,629
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

The Strength of Mac Lane Set Theory.A. R. D. Mathias - 2001 - Annals of Pure and Applied Logic 110 (1-3):107-234.
New Foundations for Mathematical Logic.W. V. Quine - 1937 - Journal of Symbolic Logic 2 (2):86-87.

Add more references

Citations of this work BETA

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

Add more citations

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 index
2017-04-21

Total views
16 ( #551,742 of 2,280,617 )

Recent downloads (6 months)
4 ( #316,679 of 2,280,617 )

How can I increase my downloads?

Downloads

My notes

Sign in to use this feature