To interpret a
function symbol f, we do the following. Define a
function σ as follows.
σ takes in a tuple of
equivalences classes (mi∈Π). From each
class it selects an arbitrary
vector xi∈mi. Now the situation looks like this:
From this setup we need to produce a
vector. Do so by walking along this grid horizontally, folding each column of values into one value by the interpretation of
f in the respective
model.
Expressely, define our
vector x as follows:
x(α)=fMα(x1(α) … xk(α))
Thus we have
σ:(mi)↦x. Define
σ′:(mi)↦[x]∼, and let
fM=σ′.
From this setup we need to produce a vector. Do so by walking along this grid horizontally, folding each column of values into one value by the interpretation of in the respective model.
Expressely, define our vector as follows:
Thus we have . Define , and let .