As I said in the last post, Church came up with λ-calculus, which looks like it's a great formal model of computation. But - there was a problem. Church struggled to find a *model*. What's a model, and why would that matter? That's the point of this post. To get a quick sense of what a model is, and why it matters?

A model is basically a mapping from the symbols of a logical system to some set off objects, such that all statements that you can prove in the logical system will be true about the corresponding objects. Note that when I say object here, I don't necessarily mean real-world physical objects - they're just *something* that we can work with, which is well-defined and consistent.

Why does it matter? Because the whole point of a system like λ-calculus is because we want to use it for reasoning. When you have a logical system like λ-calculus, you've built this system with its rules for a reason - because you want to use it as a tool for understanding something. The model provides you with a way of saying that the conclusions you derive using the system are meaningful. If the model isn't correct, if it contains any kind of inconsistency, then your system is completely meaningless: it can be used to derive *anything*.

So the search for a model for λ-calculus is really important. If there's a valid model for it, then it's wonderful. If there isn't, then we're just wasting our time looking for one.

So, now, let's take a quick look at a simple model, to see how a problem can creep in. 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 \(forall x in P: mbox{em foo}\) to mean \(forall x : P(x) Rightarrow mbox{em 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 \({cal N}(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, \(mbox{em succ}(x,y)\), where \(mbox{em succ}(x,y)\) is true if and only if x = y + 1. To use that to define the ordering of the naturals, we can say: \(forall x in {cal N}: exists y: mbox{em succ}(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 similarly, with two statements:

- \(forall x in {cal N}: exists y in {cal N}: mbox{em pred}(x, y)\).
- \(forall x,y in {cal N}: mbox{em pred}(y,x) Leftrightarrow mbox{em succ}(x,y)\)

So every number has a predecessor, and every number has a successor, and x is the predecessor of y if y is the successor of x.

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".

- \(forrall x,y in {cal N}: exists z in {cal N} : Sum(x,y,z)\)
- \(forall x,y in {cal N}: Sum(x, 0, x)\)
- \(forall x,y,z in {cal N}: exists a,b in {cal N}: Sum(a,b,z) land mbox{em succ}(a,x) land mbox{em succ}(y,b) Rightarrow 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: \(forall x,y,z in {cal N} : diff(x,y,z) Leftrightarrow sum(z,y,x)\)

That's: x-y=z if and only if x=y+z.

We can also define greater than using addition:

\(forall x,y in {cal N} : x > y Leftrightarrow\)

- \(mbox{em succ}(x,y)) lor\)
- \(exists z in {cal N}: mbox{em succ}(x, z)) land exists z in {cal N}: mbox{em succ}(x,z) and 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 that every natural number has a successor *and a predecessor*, and we also said that a number x is greater than a number y if you can get from y to x using a sequence of successors. That means that 0 has a predecessor, and that the predecessor of 0 is less than 0. But we're supposed to be defining the natural numbers! And one of the standard axioms of the natural numbers is that \(forall x in {cal N}: 0 le x\). But we've violated that - we have both \(forall x in {cal N}: 0 le x\), and

\(exists x in {cal N}: 0 > x\). And with a contradiction like that in the system, we can prove *anything* we want, anything at all. We've got a totally worthless, meaningless system.

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.

You said that we have "for all x in N, 0 ≤ x" but I don't see it in the logic you've defined. We'll be in the shit if we apply the logic to the naturals, but we'd be okay applying the logic to the integers, so the problem isn't that the logic is inherently inconsistent but rather that we didn't find the right model for it...?

I'm missing something. Are the axioms of the naturals part of the logic or part of the model?

We're trying to build a logic we can use to reason about the naturals. The model is where we make sure that all the axioms of the naturals hold in this logic, and (IIRC) that known properties of the naturals either hold in this logic, or are beyond the logic's ability to prove or disprove.

In this case, as you say, we appear to have built a logic that describes the integers. Trying to use it for the naturals will result in us being able to prove things about the naturals that aren't actually true.

It's missing at least one thing for the integers. Sum(-1,-1, o) should be true but we can't prove it. The rules allows us to start with Sum(0, 0, 0) and from there get Sum(1, -1, -0) and Sum(2, -2, 0) but they never let us move in the other direction. So we need another rule e.g.

for all x, y in N: Sum(x, y, z) => Sum(y, x, z)

I'm curious though. If the error was removed, would the above be a model for the Naturals.

It seems like {0, succ(0), succ(succ(o)), ...} is the model and then it is required to show that it obeys the axioms. In the post there doesn't seem to be a clear distinction between the model and the axioms (note: I know nothing about model theory!).

Even if you don't put such an obvious contradiction into your set of axioms, you still can't be sure that it has a model because of GĂ¶del's incompleteness theorem.

Since this post is all about the (justified) pedantry, you typoed:

"Sub(a,b,z) ^ succ (a,x) ^ succ (y,b) => Sum(x,y,z)"

Should read

"Sum(a,b,z) ^ succ (a,x) ^ succ (y,b) => Sum(x,y,z)"

Took me half a minute to work out you weren't attemping to define subtraction!

Nice typo catch, thanks. I fixed it.

I think "where mbox{em succ}(x,y) is true if and only if x = y + 1." should read "where mbox{em succ}(x,y) is true if and only if x + 1 = y."

Indeed. At first I thought that this was going to be the deliberate error, since it turned the "every number has a successor" statement into "every number has a predecessor", but then predecessors were ostensibly put in explicitly.

This post is wrong in many ways. But nice try. I don't want to spend much time on elaborating now, perhaps later.

Nitpick:

"succ(x, y) iff x = y + 1

forall x exists y: succ(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."

That's not true. In english it would be: every number has a predecessor.

Besides, you can't really say "succ(x,y) iff x = y + 1" if you want to axiomatize the natural numbers. Bleh.

I do not see from your article what are the axioms and what is the model.