Consistency Checking and Countermodels
In formal logic, we

define consistency to mean that something has a model; see the

wikipedia entry on this. This is the common definition employed by most modern logicians. So under this definition, if a sentence is consistent it

must have a model. In this entry in the Formal Philosophy tutorial, I'll

show you how to have a computer automatically generate a model of a consistent theory.

In another thread, another author wrote:

Hardstreet wrote:Previously I've used the example of time and color: "I leave for work at 9AM and my favorite color is green." The two parts of that statement are true (for the purposes of example), and they are perfectly consistent...

We shall now formally verify that they are consistent. The easiest way to check is to formalize "I leave for work at 9AM and my favorite color is green." There's always a variety of ways to do this, so proper formalization is occasionally something people argue about. But in a computer system you are of course free to play around with a variety of formalizations at your leisure. I'll do a simple one. Fire up prover9 and input the following into Assumptions:

- Code: Select all
`Leaves_for_work_at_9AM(me).`

Favorite_color_is(me,green).

Now go to "Model/Countermodel Search" and hit "Start". In a second, prover9 will come up with a model, probably like this one:

- Code: Select all
`interpretation( 2, [number = 1,seconds = 0], [`

function(green, [0]),

function(me, [0]),

relation(Leaves_for_work_at_9AM(_), [1,0]),

relation(Favorite_color_is(_,_), [

1,0,

0,0])]).

Obviously, the output is a bit technical. Many computer scientists think of first order models like computer databases, which is how I am going to think about what we are seeing. You can use the "Reformat" button to change this into other forms which make it clearer what is going on. I shall interpret this output for you, however.

Essentially what mace did was make a model with two two mathematical objects, 0 and 1. It declared two constants,

me and

green, to denote the number 0. As a peculiarity of prover9's design, it denotes constants as

nullary functions, ie functions that take no argument.

Anyway, mace also invented a predicate and a relation,

Leaves_for_work_at_9AM(x) and

Favorite_color_is(x,y). In this case

Leaves_for_work_at_9AM(x) takes one argument and

Favorite_color_is(x,y) takes two arguments. In both cases, the argument is suppose to be a term, like

me or

green. Mace says that in the model it made,

Leaves_for_work_at_9AM(x) is true when it's input is 0, and false when it is 1. It also says that that

Favorite_color_is(x,y) is only true when both x and y are 0.

We could jot this down and verify that this model makes true the assumptions we said, but in this case, we can make prover9 verify it for us. Go to the reformat button and hit "Cooked", it should give the following output:

- Code: Select all
`green = 0.`

me = 0.

Leaves_for_work_at_9AM(0).

- Leaves_for_work_at_9AM(1).

Favorite_color_is(0,0).

- Favorite_color_is(0,1).

- Favorite_color_is(1,0).

- Favorite_color_is(1,1).

Copy this, and go back to the "Assumptions" and "Goals" window in prover9. Clear the assumptions, and paste this output into assumptions. Now paste our original assumptions in goals, ie, copy this and past it into goals:

- Code: Select all
`Leaves_for_work_at_9AM(me).`

Favorite_color_is(me,green).

We are going to have prover9 logically derive our premises, from it's own logical specification of the model of our premises it made. Go over to "Proof Search" and hit start. In a second it will have a proof (it also gives me a weird error, I don't know what that's about).

You are probably thinking "This is crazy! I'm not a number, I'm a free man! And neither is green! And even if we were numbers, we wouldn't be identical!" Mace, and like a typical logician, doesn't really care if the models it generates are sensible. They are just intended to be little databases that make true all of the assumptions. There's nothing,

logically, that says that you, 0, and green can't be identical.

A better way to understand what is going on is to understand that while Mace makes models, which are good for proving your assumptions are consistent, but it also makes

countermodels. A countermodel in this program is something that makes all of the premises true and the goal false.

Here's an example. Suppose I put in the old premises about going to work at 9AM and favorite colors, and put in my goal

- Code: Select all
`Rocks_out_to_Iron_Maiden(me).`

Now, suppose I sat down to prove that if I go to work at 9AM and my favorite color is green, then I rock out to Iron Maiden. I'd be at the task until my grave, and the logicians would write "Idiot" on my tombstone.

'Cause you can't prove if this conclusion from it's premises. Why can't you? I certainly rock out to Iron Maiden in real life. But the reason you can't deduce it from the premises because there is a counter example. How do I know there is a counter-example? ...I just made MACE make me one. You can too! Go over to "Model/Counterexample search" and hit start, and in a second it will come up with a counter-example. You can interpret its output yourself.

Hardstreet wrote:Or think of a physical model. I want to build a model of a vehicle, and the pieces I've got so far are a wheel, a carburetor, and the Statue of Liberty. What are you going to do with that?

Well, in mathematical modeling like I just described, our universe consists of integers (that is to say, we have an infinite number of objects to build with). Mace rarely has a dearth of mathematical objects to work with; it only has trouble when my premises state I have an

infinite number of objects. This is a real technical limitation for Mace; I shall write on it sometime.

That's all for now!