Decidable fragments of the simple theory of types with infinity and NF
Dawar, Anuj Forster, Thomas McKenzie, Zachiri
Dawar, Anuj
Forster, Thomas
McKenzie, Zachiri
Advisors
Editors
Other Contributors
Affiliation
EPub Date
Publication Date
2017-04-21
Submitted Date
Collections
Other Titles
Abstract
We identify complete fragments of the simple theory of types with infinity (TSTI) and Quine's new foundations (NF) set theory. We show that TSTI decides every sentence φ in the language of type theory that is in one of the following forms: (A) φ = ∀x r11 ⋯ ∀xrkk ∃ys11 ⋯ ∃ys11 θ where the superscripts denote the types of the variables, s1 > ⋯ > s1, and θ is quantifier-free, (B) φ = ∀x r11 ⋯ ∀xrkk ∃ys11 ⋯ ∃ys11 θ 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: (A′) φ = ∀x1 ⋯ ∀xk ∃y1 ⋯ ∃yl θ where θ is quantifier-free and φ admits a stratification that assigns distinct values to all of the variables y1,⋯, yl, (B′) φ = ∀x1 ⋯ ∀xk ∃y1 ⋯ ∃yl θ where θ is quantifier-free and <p admits a stratification that assigns the same value to all of the variables y1,⋯, yl.
Citation
Dawar, A., Forster, T., & McKenzie, Z. (2017). Decidable fragments of the simple theory of types with infinity and NF. Notre Dame Journal of Formal Logic, 58(3), 433-451. https://doi.org/10.1215/00294527-2017-0009
Publisher
Duke University Press
University of Notre Dame
University of Notre Dame
Journal
Notre Dame Journal of Formal Logic
Research Unit
DOI
10.1215/00294527-2017-0009
PubMed ID
PubMed Central ID
Type
Article
Language
Description
This article is not available on ChesterRep
Series/Report no.
ISSN
0029-4527
EISSN
1939-0726
ISBN
ISMN
Gov't Doc
Test Link
Sponsors
Unfunded