First-Order Logic with Sets and Update Expressions
Claim: we can add update operations, a well as operations of set algebra on sets and relations to first-order logic. These constructs do not change the expressive power and can be eliminated. Result is a first-order logic formula.
Syntactic extension of FOL with if-then-else, function update, sets.
ite(p,x,y) = if p then x else y
f ( (a,b) :=c)(x,y)
Set variables (not quantified).
Set operations , , , .