So, what is a structure and how does this relate to a logical language? A structure is just a set which has some additional material attached; since we have a language we're not using, we might as well attach it to the set.

For a set A, and a language L, an L-Structure is a non-empty set A, (called the universe of structure for A) such that:

- For each constant symbol c, we have a c
^{A}in A. - For each k-ary function symbol f, there is an f
^{A}:A^{k}->A. - For each k-ary relation symbol R, there is an R
^{A}in A^{k}

^{A}are called interpretations of x. You can think of an L-structure relating to L as a meaning for L. They just drop these symbols into this universe structured around A, and give them a home. But we still don't actually have a way to get from L to its "meaning" in A! Namely, our structure does not contain any information about variables.

A quick recap: we've taken a set A, and equipped it with a structure by dropping symbols from a logical language into it-- notice that constants are just members of A; this is a good thing. And k-ary functions (relations) are functions (relations) which take k elements of A; also a good thing. But we still haven't done anything with our variables So, what kind of variables do we have if we're looking at a set A? We have elements of A. So, let s be a function s:V->A, and let's call it an evaluation map [remember, V is the set of variables in our language]. So, we have a function which gives each variable a value. Good!

But right now, our function and our L-structure are kind of disjoint. We need a function which can take the value of our variables and push those through the interpretations of our functions and relations. So!

For s, let s':T->A with the following properties:

- s'(x)=s(x) [when x is a variable]
- s'(c)=c
^{A}[when x is a constant] - s' preserves function application: s'(f(t_1,...,t_k))=f
^{A}(s'(t_1),...,s'(t_k)).

So far, we've defined a logical language, and we've given our language a set to play in, and given our terms a meaning. Pulling back out, when our terms mean something, then we can ask whether a statement about our terms is true. So, truth:

For an L-structure X on A, and an evaluation map s:V->A (X is easier to write than a new font), a statement a is called true (with evaluation s)-- in symbols X|- a [s] if:

- When a: t=u, then X|- a [s] iff s'(t)=s'(u)
- When a: R(t_1,...,t_k), then X|- a [s] if and only if R
^{X}(s'(t_1),...s'(t_2)) holds. - Similarly for non atomic formulas.

I hope this was easier to follow than the lectures it came from (to be fair, I've left out some useful material about homomorphisms, which was almost as abstract as the evaluation maps)

## No comments:

Post a Comment