Decidable fragments of the simple theory of types with infinity and NF

Abstract: We identify complete fragments of the Simple Theory of Types with Infinity (

m a t h r m T S T I

) and Quine's

m a t h r m N F

set theory. We show that

m a t h r m T S T I

decides every sentence

p h i

in the language of type theory that is in one of the following forms: (A)

p h i = f o r a l l x_{1}^{r_{1}} c d o t s f o r a l l x_{k}^{r_{k}} e x i s t s y_{1}^{s_{1}} c d o t s e x i s t s y_{l}^{s_{l}} h e t a

where the superscripts denote the types of the variables,

s_{1} > l d o t s > s_{l}

and

h e t a

is quantifier-free, (B)

p h i = f o r a l l x_{1}^{r_{1}} c d o t s f o r a l l x_{k}^{r_{k}} e x i s t s y_{1}^{s} c d o t s e x i s t s y_{l}^{s} h e t a

where the superscripts denote the types of the variables and

h e t a

is quantifier-free. This shows that

m a t h r m N F

decides every stratified sentence

p h i

in the language of set theory that is in one of the following forms: (A')

p h i = f o r a l l x_{1} c d o t s f o r a l l x_{k} e x i s t s y_{1} c d o t s e x i s t s y_{l} h e t a

where

h e t a

is quantifier-free and

p h i

admits a stratification that assigns distinct values to all of the variable

y_{1}, l d o t s, y_{l}

, (B')

p h i = f o r a l l x_{1} c d o t s f o r a l l x_{k} e x i s t s y_{1} c d o t s e x i s t s y_{l} h e t a

where

h e t a

is quantifier-free and

p h i

admits a stratification that assigns the same value to all of the variables

y_{1}, l d o t s, y_{l}

.

Cited In (6)

This page was built for publication: Decidable fragments of the simple theory of types with infinity and NF