Thomas Forster

Applications of game-theoretic semantics à la Hintikka can be extended from Lower Predicate Calculus to languages with branching quantifiers. When one does this, issues which in the LPC could be swept under the carpet suddenly cause unwelcome subtleties. It turns out that which formulae of the branching quantifier logic one accounts true comes to depend on whether one requires that the winning strategies for Team Eloïse in the Hintikka game be deterministic (or allows them to be nondeterministic). The set of valid formulae is affected similarly. © 2011 Elsevier B.V., All rights reserved.

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.