This is an old revision of the document!
Deciding a Language of Sets (and Relations)
Consider a simple language of sets:
\[ \begin{array}{l}
S ::= V \mid S \cup S \mid S \cap S \mid S \setminus S \mid \mathbf{U} \mid \emptyset \\
A ::= (S = S) \mid (S \subseteq S) \mid card(S){=}c \mid card(S) \leq c \mid card(S) \geq c \\
F ::= F \lor F \mid F \land F \mid \lnot F \\
c ::= 0 \mid 1 \mid 2 \mid ...
\end{array} \]
We show that this language is decidable.