As usual, we’ll start with a language, and that language will be based on first order logic. This language is described by the following phrase structure grammar.
statement : bool_exp
bool_exp | "[" "¬" bool_exp "]" | "[" bool_exp b_operator bool_exp "]"
| "[" quantifier variable "." bool_exp "]"
| "[" quantifier variable "∈" set_exp : bool_exp "]"
| "[" variable relation variable "]"
b_operator : "∧" | "∨" | "⊃"
quantifier : "∀" | "∃"
relation : "∈" | "=" | "⊆"
set_exp : "∅" | variable | "[" "⋂" set_exp "]" | "[" "⋃" set_exp "]"
| "[" set_exp "∩" set_exp "]" | "[" set_exp "∪" set_exp "]"
| "[" set_exp "∖" set_exp "]" | "[" set_exp "×" set_exp "]"
| "[" "P" set_exp "]" | "{" list "}" | "(" list ")"
| "{" variable "∈" set_exp : bool_exp "}"
list : | sequence
sequence : set_exp | set_exp "," sequence
variable : letter | variable "!"
letter : "v" | "w" | "x" | "y" | "z" | "A" | "B" | "C" | "D" | "E"
| "F" | "G" | "H" | "I" | "J" | "R" | "S" | "T" | "U" | "V"Some of these symbols and rules are familiar from earlier chapters while others are new, or are used in new ways. The following remarks refer to the intended interpretation of the language and are not strictly part of the language.
The symbols (, ), {, and } are no longer used for grouping expressions but have special meanings. Only [ and ] are used for grouping expressions as in previous chapters. { and } are used in two different ways of constructing sets. We write \({ \{ x , y , z \} }\) for the set whose only members are \({ x }\), \({ y }\) and \({ z }\), for example, and \({ \{ x ∈ A \colon [ ¬ [ x ∈ B ] ] \} }\) for the set of \({ x }\) which are members of \({ A }\) but not of \({ B }\). The ∈ sign denotes set membership. ( and ) are used in two ways. One is to construct lists. \({ ( x , y , z ) }\) is the list whose first element is \({ x }\), whose second element is \({ y }\) and whose third element is \({ z }\). This is unlike \({ \{ x , y , z \} }\), where \({ x }\) happens to have been written first, \({ y }\) happens to have been written second, and \({ z }\) happens to have been written third, but the ordering is not significant. \({ \{ x , y , z \} }\) is the same set as \({ \{ y , z , x \} }\) but \({ ( x , y , z ) }\) is not the same list as \({ ( y , z , x ) }\) unless \({ x }\), \({ y }\) and \({ z }\) are all equal.
In addition to the old notation for quantifiers there is a new notation. We have expressions like \({ [ ∀ x ∈ A : [ [ x ∈ B ] ∨ [ x ∈ C ] ] ] }\). This is to understood as a shorthand for \({ [ ∀ x . [ [ x ∈ A ] ⊃ [ [ x ∈ B ] ∨ [ x ∈ C ] ] ] ] }\). This, and the corresponding notation for ∃, are convenient because we often want to state that all members of a set have some property or that some member has that property. Such quantifiers are called bounded quantifiers. We met similar bounded quantifiers in constructive elementary arithmetic.
It’s possible to do first order logic with bounded quantifiers as if they were ordinary quantifiers, provided all quantifiers are over the same set, at least with the version of first order logic we’re using, one without existential presuppositions. In a logic with existential presuppositions we would need to add the additional requirement that the set is known in advance to be non-empty. It’s easy, but dangerous, to forget the non-emptiness requirement.
We have a new relation ⊆ as well. This is the subset relation. Note that this is not necessarily a proper subset. Each set is a subset of itself. The distinction between ∈ and ⊆ was a source of confusion in the early development of set theory. It’s still often a source of confusion for students. \({ A ∈ B }\) means that \({ A }\) is a member of \({ B }\) while \({ A ⊆ B }\) means that every member of \({ A }\) is a member of \({ B }\).
∅ is the empty set, i.e. the set with no members. There are two versions of the intersection and union operators. The unary operators ⋂ and ⋃ indicate intersection and union, respectively, and are not preceded by a set expression. ⋃ takes a set and gives you its union, i.e. the set whose members are the members of its members. In other words, \({ [ x ∈ [ ⋃ A ] ] }\) if and only if there is some \({ B }\) such that \({ x }\) is a member of \({ B }\) and \({ B }\) is a member \({ A }\). The most common case of unions is one where the set of sets has two member so we have a special notation for this. We write \({ [ B ∪ C ] }\) to mean \({ [ ⋃ \{ B , C \} ] }\), i.e. the set of all members of \({ B }\) which are in \({ C }\). Similar remarks apply to the intersection. If \({ A }\) is a non-empty set then \({ [ x ∈ [ ⋂ A ] ] }\) if and only if \({ x }\) is a member of \({ B }\) for every \({ B }\) in \({ A }\). The restriction to non-empty sets will be explained later. Again we have a special notation for the intersection of a pair of sets. \({ [ B ∩ C ] }\) means \({ [ ⋂ \{ B , C \} ] }\). If you have trouble visually distinguishing \({ ⋂ }\) from \({ ∩ }\), or \({ ⋃ }\) from \({ ∪ }\), or if you’re using a screen reader which reads them the same, you needn’t worry too much. The grammar is designed in such a way that they can always be distinguished by context, specifically by whether or not they are preceded by a set expression.
Our other two set operations are \({ ∖ }\) for the relative complement and \({ × }\) for the Cartesian product. \({ [ A ∖ B ] }\) is the set of members of \({ A }\) which are not in \({ B }\), i.e. \({ \{ x ∈ A \colon [ ¬ [ x ∈ B ] ] \} }\). \({ [ A × B ] }\) is the set of pairs \({ ( x , y ) }\) where \({ x }\) is an member of \({ A }\) and \({ y }\) is a member of \({ B }\). \({ [ P A ] }\) is the power set of \({ A }\), i.e. the set of all subsets of \({ A }\), while \({ [ L A ] }\) is the set of lists all of whose elements are members of \({ A }\).
You may notice that I’ve dropped practice of using separate symbols, outside the language, for expressions of various types. Occasionally it will be convenient to introduce an ad hoc notation but I’ll mostly do what I’ve done above, and use a particular variable to stand for any variable, or sometimes any set expression. Hopefully this will not cause confusion.