More logic: models and why they matter
If you haven't read my earlier posts on logic, and you have trouble understanding this one, you might one to go back and take a look at them:
As I said quite a while ago, when you want to use logic to describe something, it's crucial to have a valid model. A model is a way of showing that the meaning of statements in your logic are valid, by demonstrating the connection between your logic, and something concrete that your logic is talking about. The reason that models are so important is because it's easy to build logical systems that look correct, but which will allow you to prove invalid statements.
Today, I'm going to show you how that works. I'm going to build a logic for talking about the natural numbers - that is, integers greater than or equal to zero. Then I'll show you how invalid results can be inferred using it; and finally show you how it fails by using the model.
One quick thing, to make the notation easier to read: I'm going to use a simple notion of types. A type is a set of atoms for which some particular one-parameter predicate is true. For example, if P(x) is true, I'll say that x is a member of type P. In a quantifier, I'll say things like "all x in P: foo" to mean "all x : P(x) implies foo". Used this way, we can say that P is a type predicate.
How do we define natural numbers using logic?
First, we need an infinite set of atoms, each of which represents one number. We pick one of them, and call it zero. To represent the fact that they're natural numbers, we define a predicate "Natural(x)", which is true if and only if x is one of the atoms that represents a natural number.
Now, we need to start using predicates to define the fundamental properties of numbers. The most important property of natural numbers is that they are a sequence. We define that idea using a predicate, successor(x,y), where successor(x,y) is true if and only if x = y + 1. To use that to define the ordering of the naturals, we can say:
all x in Natural : exists y : Successor(x,y)
Or in english: every natural number has a successor - you can always add one to a natural number and get another natural number.
We can also define predecessor:
all x in Natural : exists y in Natural : Predecessor(y,x)
all x,y in Natural : Predecessor(y,x) iff Successor(x,y)
To be able to define things like addition and subtraction, we can use successor. Let's define addition using a predicate Sum(x,y,z) which means "z = x + y".
all x,y in Natural : exists z in Natural : Sum(x,y,z)
all x,y in Natural : Sum(x, zero, x)
all x,y,z in Natural : (exists a,b in Natural : (Sum(a,b,z) and Successor(a,x) and Successor(y,b) implies Sum(x,y,z)))
Again, in english: for any two natural numbers, there is a natural number that it their sum; x + 0 always = x; and for any natural number, x + y = z is true if (x + 1) + (y - 1) = z.
Once we have addition, subtraction is easy:
all x,y,z in Natural : Difference(x,y,z) iff Sum(z,y,x)
That's: x-y=z if and only if x=y+z.
We can also define greater than using addition:
all x,y in Natural : Greater(x,y) iff Successor(x,y) or (exists z in Natural : Successor(x,z) and Greater(z,y))
That's x > y if you can get to x from y by adding one repeatedly.
So, we've got a nice definition of natural numbers here, right?
Almost. There's one teeny little mistake.
That doesn't work. The problem is all the way back in the definition of predecessor. It includes: "all x in Natural : exists y in Natural : Predecessor(y,x)", or every number has a predecessor. Zero doesn't have a predecessor. Our logical statements assert something which is not true of the things we're modeling the logic: our logic is invalid. And once we have that error, that there's a natural number less that zero, we can use it to prove anything: 1 > 1, 0 + 0 = 23, anything. All because of one little error in the model.
That's why mathematicians are so particular about proving the validity of their models: because the tiniest error can mean that anything you proved with the logic might not be true - your proofs are worthless.
As I said quite a while ago, when you want to use logic to describe something, it's crucial to have a valid model. A model is a way of showing that the meaning of statements in your logic are valid, by demonstrating the connection between your logic, and something concrete that your logic is talking about. The reason that models are so important is because it's easy to build logical systems that look correct, but which will allow you to prove invalid statements.
Today, I'm going to show you how that works. I'm going to build a logic for talking about the natural numbers - that is, integers greater than or equal to zero. Then I'll show you how invalid results can be inferred using it; and finally show you how it fails by using the model.
One quick thing, to make the notation easier to read: I'm going to use a simple notion of types. A type is a set of atoms for which some particular one-parameter predicate is true. For example, if P(x) is true, I'll say that x is a member of type P. In a quantifier, I'll say things like "all x in P: foo" to mean "all x : P(x) implies foo". Used this way, we can say that P is a type predicate.
How do we define natural numbers using logic?
First, we need an infinite set of atoms, each of which represents one number. We pick one of them, and call it zero. To represent the fact that they're natural numbers, we define a predicate "Natural(x)", which is true if and only if x is one of the atoms that represents a natural number.
Now, we need to start using predicates to define the fundamental properties of numbers. The most important property of natural numbers is that they are a sequence. We define that idea using a predicate, successor(x,y), where successor(x,y) is true if and only if x = y + 1. To use that to define the ordering of the naturals, we can say:
all x in Natural : exists y : Successor(x,y)
Or in english: every natural number has a successor - you can always add one to a natural number and get another natural number.
We can also define predecessor:
all x in Natural : exists y in Natural : Predecessor(y,x)
all x,y in Natural : Predecessor(y,x) iff Successor(x,y)
To be able to define things like addition and subtraction, we can use successor. Let's define addition using a predicate Sum(x,y,z) which means "z = x + y".
all x,y in Natural : exists z in Natural : Sum(x,y,z)
all x,y in Natural : Sum(x, zero, x)
all x,y,z in Natural : (exists a,b in Natural : (Sum(a,b,z) and Successor(a,x) and Successor(y,b) implies Sum(x,y,z)))
Again, in english: for any two natural numbers, there is a natural number that it their sum; x + 0 always = x; and for any natural number, x + y = z is true if (x + 1) + (y - 1) = z.
Once we have addition, subtraction is easy:
all x,y,z in Natural : Difference(x,y,z) iff Sum(z,y,x)
That's: x-y=z if and only if x=y+z.
We can also define greater than using addition:
all x,y in Natural : Greater(x,y) iff Successor(x,y) or (exists z in Natural : Successor(x,z) and Greater(z,y))
That's x > y if you can get to x from y by adding one repeatedly.
So, we've got a nice definition of natural numbers here, right?
Almost. There's one teeny little mistake.
- We said: all x in Natural : exists y : Successor(x,y)
- And we also said: all x,y in Natural : Greater(x,y) iff Successor(x,y) or (exists z in Natural : Successor(x,z) and Greater(z,y))
- We can instantiate (1) with x = 0, as "exists k : Successor(0,k)".
- And then we can instantiate (2) with x=0 and the k from (3): Greater(0,k) iff Successor(0,k) or ..."
- Because we know that Successor(0,k), we can conclude Greater(0,k)
- So, exists k in natural : Greater(0,k)
That doesn't work. The problem is all the way back in the definition of predecessor. It includes: "all x in Natural : exists y in Natural : Predecessor(y,x)", or every number has a predecessor. Zero doesn't have a predecessor. Our logical statements assert something which is not true of the things we're modeling the logic: our logic is invalid. And once we have that error, that there's a natural number less that zero, we can use it to prove anything: 1 > 1, 0 + 0 = 23, anything. All because of one little error in the model.
That's why mathematicians are so particular about proving the validity of their models: because the tiniest error can mean that anything you proved with the logic might not be true - your proofs are worthless.
posted by MarkCC at
1:17 PM
RSS
3 Comments:
I see a few problems here:
1. As you point out, the Predecessor is true for integers, not natural numbers, but this is not relevant to the contradiction below because you don't use it.
2. Sum is similarly flawed, because it does not allow for x being zero. And in passing, the y is unnecessary in the second Sum axiom.
3. Your definition of Greater does not correspond to the English explanation. Your axioms are equivalent to saying "y > x", not "x > y". There is, in fact, no flaw in being able to prove that there exists a number greater than zero.
By
Anonymous, at 7:11 PM
Sometimes a logical system can have localized logical errors, but still be useful in general. The standard application program on a computer is an example of this. It might crash on rare occasions, but as long as it's generally stable enough for everyday tasks, it's still useful.
By
Anonymous, at 5:54 AM
Mr. Winwood,
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.
By
Anonymous, at 11:00 AM
Post a Comment
<< Home