Arbtirary thoughts on nearly everything from a modernist poet, structural mathematician and functional programmer.

Wednesday, September 16, 2009

Introduction to Logical Languages (1)

This is mostly to clarify in my mind the material from the first 2 lectures of the (mathematical) logic class I'm taking. Hopefully it will also help someone else.

So. We want to be able to look at logic from a formal, rigorous perspective-- which means we need to define logic formally. The guiding question when defining it should be: What does a logic look like? We want variables and all the fun logical connectives, and we want them to mean something, and we want all the meanings (eventually) to boil down to the question "Is this statement true?".

So, let's make each of those happen, one at a time;
First, we need some symbols. We will call S our alphabet-- the set of symbols. This may be tediously formal, but it must be done. Since we want to create a logic, we need the logical symbols: So S contains the connectives and quantifiers, (I'm not going to list them) and just as importantly: variables. These are our logical symbols. Since this is mathematical logic, we need some mathy non-logical symbols; these will be constant symbols, relation symbols and function symbols (these will also "look like" variables, but we want to distinguish between them for reasons we will see shortly). We will also consider '=' to be a logical symbol-- I know it's a relation, but it's a special one, and we want to keep it special.

So, we have a bunch of symbols; that doesn't do us much good, so let's let S* be the set of finite sequences from S. Namely, the empty sequence (I'll use _|_) is in S*, S is a subset of S*, and if a and be are in S, ab (the concatenation of a and b) is in S*.
We want to define a language, L, as a subset of S*, but while any subset is a language, we don't want just any subset: it has to be something that we can "read" in a meaningful way. We have to define our language inductively, and piece by piece. I'll let you know when we get there.

Let the set of L-terms (or just terms) be the smallest T such that:
  • V (the set of variables) is in T.
  • C (the set of constant symbols) is in T.
  • Whenever t_1,...t_k are in T, and f is a k-ary function symbol, f(t_1,...,t_k) is in T.
Notice that this definition is recursive: any t_i in the last condition may have the form f'(t_1',...,t_k').
A term is an object which we can equip with some non-logical value, which may need some sort of context (a value for a variable). But a term does us no good on its own, if we are interested in logical values. So, an atomic formula is:
  • if t, u are terms, then "t=u" is an atomic formula.
  • if t_1,...,t_k are terms, and R is a k-ary relation symbol, then R(t_1,...,t_k) is an atomic formula
So, like any set of "atoms", atomic formulas are the building blocks for formulas.
The set of L-formulas (or just formulas) is defined inductively:
Base case: Atomic formulas are formulas.
Closure: The set of formulas is closed under logical connectives, and quantifiers.
(What this means is that if you have two formulas, p and q, you can connect them using a logical connective, and you can quantify them, and the sequence of symbols you create will also be a formula.)

So, we now have something that looks like the logic we know. But there is a problem: if x and y are variables, "x=y" is a valid formula. But what are x and y?
In that formula, both x and y are free variables. For a given formula the free variables are :
  • (for s, t terms) FV(s=t)= var(s)Union var(t) [var(t) means the variabls in t]
  • (for R a k-ary relation) FV(R(t_1,...,t_k))= Union(t_i)(over 1≤i≤k)
  • (for ~ a logical connective, a,b formulas) FV(a~b)= FV(a)UnionFV(b)
  • (for x a var, b a formula) FV(forall x, b)= FV(there exists x, b)= FV(b)\{x}
(Sorry for the formatting...) All this says is that anytime a variable is introduced, it is "free" until it has been quantified.
So finally, we have: A sentence is a formula with no free variables, and our logical language, L, is the set of all sentences from S*.

Cool! We have a logical language. Looking back at our list of things we want, we've got connectives, and we've got quantifiers and just a little bit more. Unfortunately, this means we're not quite done: this language is meaningless. We haven't once said what these symbols actually mean. And we will learn how to do that next time.

No comments:

Creative Commons License Cory Knapp.