# 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.

#### If-Then-Else

ite(p,x,y) = if p then x else y

#### Function Update

f (a:=b)(x)

f ( (a,b) :=c)(x,y)

#### Sets

Set variables (not quantified).

Set operations , , , .

## Elimination of Extensions

f(a:=b)(x) =

f ( (a,b):=c )(x,y) =

z=ite(p,x,y)

F(ite(p,x,y))

f = g

becomes