Correcting my models post; or, why MarkCC is a dummy

As someone pointed out in the comments, I really blew it in my logic models post on monday: the error in the logic relied on the mis-definition of "predecessor"; but the way that I demonstrated the error didn't use predecessor at all. :-(

This is a great example of what happens when you try to rush. I knew I wasn't going to be around monday afternoon or all day tuesday, due to a combination of work and family stuff, so I wanted to get a post out monday morning, and I rushed it. I knew what I wanted to write; unfortunately, that's not what I actually wrote.

Anyway - to make up for it, I'll explain the correction here, and answer a few of the questions that came up in the comments.

The model that I presented for numbers using logic actually contains two errors - the one that I included deliberately (the definition of "predecessor"), and one that I included accidentally (an error in the definition of successor). What I find impressive in my own warped way is that when I demonstrated how an error in the model can create invalid results, I did it using the model error that I did not include on purpose!

So - let's start by going back and looking at the successor definition:

all x in Natural : exists y : Successor(x,y)

I said that what this statement says in english is: every number has a successor. Alas, that is not what it actually says. What is says is that every natural number is the successor of some other natural number. And that's not true - zero is not the succesor of any natural numbers, which is the fact that I took advantage of in my demonstration of the bad conclusions you can reach using an invalid model.

That statement should read:

all x in Natural : exists y : Successor(y,x)

That is, the parameters of the successor predicate were in the wrong order - so it said "x is the successor of y" rather than "y is the successor of x". With that corrected, the problem goes away. But in fact, I think that the accidental error in that definition is a better example than the one I created deliberately: it's the same general sort of problem, but it involves fewer definitions, and it's subtler. With that error, we don't need the error in "predecessor" which, to be honest, is rather contrived. You generally see predecessor defined as:

all x, y in Natural : Predecessor(x,y) iff Successor(y,x)

The error in predecessor was created by adding an extra, unnecessary statement about predecessor.

Moving on to the comments, there was an interesting question about "one": Molybdenum1 asked:

This is just nitpicky, but didn't you also assume that the number 1 exists? You claim that we take one of the natrual numbers and call it zero and then define sucessor as a natural number plus 1. But we don't know that 1 exists, or that it is a natural number, unless you define it to be the sucessor of zero, which is circular.

The trick to how we defined the natural numbers in logic is that we only need to define zero and a successor function. The natural number one does not need to be defined beyond the fact that it's the successor to zero. In an informal description of what the successor of a natural number means means, we'll often say that it means the result of adding one to that number. But that's really an informal handwave. In fact, the fundamental property of the natural numbers is that they are a totally ordered sequence of numbers starting at zero.

The "totally ordered" bit there means that for any two numbers x and y, one of three things is true: either x > y, y < x, or x and y are the same. (There are a lot of sets which don't have that property - where you can have an x and y where neither x < y, nor y < x, but they're different. But that's a discussion for another day.)

"Successor" really just advances from one member of the set of naturals to the next in the ordering. Defining one isn't necessary - it's just the number that comes after zero.

One other thing from the comments: Thomas Winwood asked:

For completion's sake, could you prove using your flawed model that 1 > 1 and that 0 + 0 = 23?

DouglasG did a great job answering the question, so I want to promote his answer up here to the font page:

If you have two exact opposite assertions in a system, then any assertion you make must be true. In this case, we have the assertions:

There are no natural numbers less than zero

-and-

There exist a natural number less than zero.

Sometimes the proofs of some statements are not trivial...

Here would be a brief sketch of how 1 > 1 would look.

From the above proof, we know there exists a k where k+1=0. Since 0 < 1, k < 1. Suppose k does NOT equal 1. We know there are no numbers less than zero by definition, so k must be greater than 1 or equal to 0. k cannot be zero because k+1=0. Thus, k must be greater than 1. However, k cannot be greater than 1 because we showed that k < 1. Thus, k=1. Hence, 1 < 1.