|
|
Introduction to Logic
|
Tools for Thought
|
|
In this example, we show how to characterize Modular Arithmetic in Relational Logic. In Modular Arithmetic, there are only finitely many objects. For example, in Modular Arithmetic with modulus 4, we would have just four integers - 0, 1, 2, 3 - and that's all. Our goal here to define the addition relation. Admittedly, this is a modest goal; but, once we see how to do this; we can use the same approach to define other arithmetic relations.
|
Let's start with the same relation, which is true of every number and itself and is false for numbers that are different. We can completely characterize the same relation by writing ground relational sentences, one positive sentence for each number and itself and negative sentences for all of the other cases.
| same(0,0) |
|
¬ | same(0,1) |
|
¬ | same(0,2) |
|
¬ | same(0,3) |
¬ | same(1,0) |
|
| same(1,1) |
|
¬ | same(1,2) |
|
¬ | same(1,3) |
¬ | same(2,0) |
|
¬ | same(2,1) |
|
| same(2,2) |
|
¬ | same(2,3) |
¬ | same(3,0) |
|
¬ | same(3,1) |
|
¬ | same(3,2) |
|
| same(3,3) |
|
Now, let's axiomatize the next relation, which, for each number, gives the next larger number, wrapping back to 0 after we reach 3.
next(0,1) |
next(1,2) |
next(2,3) |
next(3,0) |
Properly, we should write out the negative literals as well. However, we can save that work by writing a single axiom asserting that next is a functional relation, i.e., for each member of the Herbrand base, there is just one successor.
∀x.∀y.∀z.(next(x,y) ∧ next(x,z) ⇒ same(y,z))
In order to see why this saves us the work of writing out the negative literals, we can write this axiom in the equivalent form shown below.
∀x.∀y.∀z.(next(x,y) ∧ ¬same(y,z) ⇒ ¬next(x,z))
|
The addition table for Modular Arithmetic is the usual addition table for arbitrary numbers except that we wrap around whenever we get past 3. For such a small arithmetic, it is easy to write out the ground relational sentences for addition, as shown below.
plus(0,0,0) |
|
plus(1,0,1) |
|
plus(2,0,2) |
|
plus(3,0,3) |
plus(0,1,1) |
|
plus(1,1,2) |
|
plus(2,1,3) |
|
plus(3,1,0) |
plus(0,2,2) |
|
plus(1,2,3) |
|
plus(2,2,0) |
|
plus(3,2,1) |
plus(0,3,3) |
|
plus(1,3,0) |
|
plus(2,3,1) |
|
plus(3,3,2) |
As with next, we avoid writing out the negative literals by writing a suitable functionality axiom for plus.
∀x.∀y.∀z.∀w.(plus(x,y,z) ∧ ¬same(z,w) ⇒ ¬plus(x,y,w))
|
That's one way to do things, but we can do better. Rather than writing out all of those relational sentences, we can use Relational Logic to define plus in terms of same and next and use that axiomatization to deduce the ground relational sentences. The definition is shown below. First, we have an identity axiom. Adding 0 to any number results in the same number. Second we have a successor axiom. If z is the sum of x and y, then the sum of the successor of x and y is the successor of z. Finally, we have our functionality axiom once again.
∀y.plus(0,y,y) |
∀x.∀y.∀z.∀x2.∀z2.(plus(x,y,z) ∧ next(x,x2) ∧ next(z,z2) ⇒ plus(x2,y,z2)) |
∀x.∀y.∀z.∀w.(plus(x,y,z) ∧ ¬same(z,w) ⇒ ¬plus(x,y,w)) |
One advantage of doing things this way is economy. With these sentences, we do not need the ground relational sentences about plus given above. They are all logically entailed by our sentences about next and the definitional sentences. A second advantage is versatility. Our sentences define plus in terms of next for arithmetic with any modulus, not just modulus 4.
|
Use the arrow keys to navigate.
Press the escape key to toggle all / one.
|
|