Reference no: EM132979928

Challenge

The notation we use for first-order predicate logic includes function symbols. This allows a very simple representation of the natural numbers. Namely, for natural numbers, we use terms built from a constant symbol (here we choose a, but any other symbol would do) and a function symbol of arity 1 (we will use s, for "successor"). The idea is that 0 is represented by a, 1 by s(a), 2 by s(s(a)), and so on. In general, s(x) represents the successor of x, that is, x+ 1. Logicians prefer this "successor" notation, because it uses so few symbols and supports recursive definition-a natural number is either ‘a' (the base case), or it is of the form ‘s(. . .)', where . . . is a term representing a natural number. (Of course, for practical use, we prefer the positional decimal system.)

With successor notation, we can capture the usual "less than or equal" ordering of N (the set of natural numbers) with these two axioms, where L(x, y) stands for x ≤ y:

∀y(L(a, y))

∀x∀y(L(x, y) ⇒ L(s(x), s(y)))

(1) says that 0 is smaller than or equal to any natural number, and (2) says that if x ≤ y then x + 1 ≤ y + 1. Similarly, we can capture addition by introducing a predicate symbol for the addition relation, letting P (x, y, z) stand for x + y = z:

∀y(P (a, y, y))
∀x∀y∀z(P (x, y, z) ⇒ P (s(x), y, s(z)))

Turning the conjunction of (1)-(4) into clausal form, we end up with this set of clauses:

{{L(s(v1), s(v2)), ¬L(v1, v2)}, {L(a, v3)}, {P (s(v4), v5, s(v6)), ¬P (v4, v5, v6)}, {P (a, v7, v7)}}

Task A. Use resolution to show that

∃x∃y(L(s(a), x) ∧ P (y, y, x)) (5)

is a logical consequence of the axioms (1)-(4).

Task B. Your resolution proof will not only establish the truth of (5). The resolution proof provides a sequence of most general unifiers, one per resolution step, and when these are composed, in the order they were generated, you have a substitution that solves the constraint 1 ≤ x∧y+y = x. Give that substitution and explain what it means in terms of natural numbers.