Introduction to Logical Languages (2)

In my last post (earlier today), we defined a logical language. But we ended wondering how to give meaning to this language. Since we are looking at mathematical logic, we want a mathematical structure to talk about-- every logical statement fits inside of some logical structure: A group G, ZFC, N, the theory of groups, etc.
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

These x^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)).

These properties mean that s' preserves the structure we've defined on A (so s' is a homomorphism.) If the structure weren't preserved, then we'd run into the problem that if you evaluated f first, you might get something different than if you evaluated the arguments first. Also, you may be wondering why relations aren't included in this: remember that T is the set of terms, and relations aren't terms.

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.

Basically all we are saying is "The statement is true in a structure if and only if it makes sense to call it true in that structure." We've just jumped through some hurdles so that we can say "it makes sense" in a rigorous way.

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)