Quick Logic: Reasoning and Semantics

Last time I wrote about logic, I talked about the idea of separating the calculus of first order predicate logic from the semantics of FOPL. The first order predicate calculus is a set of symbolic rules by which you can mechanically perform reasoning with a set of logical statements without any understanding of the meanings of any of those statements. The semantics of the logic are a way of taking the symbolic statements, and defining what, exactly, they mean.

What I'd like to do now is show you an example of what I mean by using purely mechanical reasoning. I'm going to do it very briefly, because frankly, I think taking you through the process in detail will bore you to tears. Don't worry, it won't last long, and then I'll be able to do some fun stuff. :-)

Remember, to use FOPL, you need to define the set of atoms (the objects that the logic can make statements about), and predicates (the basic things you can say about atoms). You may also have a set of basic facts, which are statements that are known to be true in the logic without needing to be proved.

For our example, we're going to use a very small set of atoms: BlueCar, GreenCar, Joe, Jane, and Jen. To work with those atoms, we're going to use three predicates: IsACar(x), IsADriver(x), IsDriving(x,y).

We have the following basic facts:

IsACar(BlueCar)
IsACar(GreenCar)
IsADriver(Joe)
IsADriver(Jane)
IsADriver(Jen)
IsDriving(Joe,GreenCar)
forall x : forall y : IsACar(x) and IsADriver(y) and ISDriving(y,x) => (not exist z : IsADriver(z) and IsDriving(z,x) and y != z)


Now, we'd like to know if the following can be true:
(exist a: IsACar(a) and IsDriving(Jane,a)) and (exist b : IsACar(b) and IsDriving(Jen, b))

We can do this mechanically:

1. First, we can split AND statement into two different statements.
   
2. Now, we can use our inference rules, and take the statements "IsACar(GreenCar), IsADriver(Joe), and IsDriving(Joe,GreenCar)", and instantiate the "x" and "y"'s from the universal statement, producing: "IsACar(BlueCar) and IsADriver(Joe) and IsDriving(Joe,GreenCar) => (not exist z : IsADriver(z) and IsDriving(z,GreenCar) and Joe != z)"
   
3. Again using an inference rule, we can say that since we know that the left side of the instantiated inference is true, the right side must be true, so we know: "not exist z : IsADriver(z) and IsDriving(z,GreenCar) and Joe != z".
   
4. Now, let's take one of the statements that we got from step 1: "exist a: IsACar(a) and IsDriving(Jane,a)". We can instantiate that as "IsACar(GreenCar) and IsDriving(Jane,GreenCar) or (IsACar(BlueCar) and IsDriving(Jane,BlueCar))".
   
5. Using the instantiated implication from step 3, we can show that "IsDriving(Jane,GreenCar)" cannot be true, so we can reduce the statement from step 5 to: "IsACar(BlueCar) and IsDriving(Jane,BlueCar))".
   
6. Now, we can repeat what we did in step 4, only using "Jen" instead of "Jane": "(IsACar(GreenCar) and IsDriving(Jen,GreenCar)) or (IsACar(BlueCar) and IsDriving(Jen,BlueCar))".
   
7. But by the rule we used in 5, we can show that neither case in this statement is true. Therefore, we have proven that the statement cannot be true.
   

This process is loosely based on a technique called semantic tableaus, or truth trees. It probably would be easier to follow drawn out as a truth tree, but it's very hard to do that in blog form.

Now - the remaining thing with this FOPL is semantics. For FOPL, semantics is basically pretty easy: each atom in the the set has to be "bound" or defined as some real entity: a person, a number, etc.

Each predicate is a statement; when the semantics of the logic are defined, each predicate must have a meaning assigned. For statements like the "IsDriving" in the example above, defining that mathematically is rather hairy; but informally, we can just say that in the example above, the predicate names clearly define what they're intended to mean. (If you're interested in seeing how to assign logical semantics to language, there's an excellent textbook by Ernest LePore called "Meaning and Argument". Professor LePore is the guy who taught me to love logic back in my undergraduate days at Rutgers. He's a terrific guy, a great teacher, and a great writer.)

The AND, OR, and NOT statements mean roughly what you would expect in english, except that in english, when we say "A or B", we generally really mean "A or B but not A and B"; in FOPL, "A or B" does not preclude "A and B".

"A implies B" means "If A is true, then B must be true".

"all x : P(x)" means that you can put any atom from the logic into P(x), and it will be true.

"exists x : P(x)" means that if you tried every possible atom from the logic into P(x), eventually you'd find at least one for which P(x) was true.

And that's pretty much it. FOPL is very intuitive; it's basically what we really understand as being logic, just presented in a very careful and formal way. It's not the only logic, and as I hope to show later, it's not necessarily the most interesting logic, but it's an easy one to understand, and a good starting place.