Problem 1

Let Σ = {R, f, g, co, c₁} be a first-order signature, where R is a binary relation symbol, f is a

unary function symbol, g is a binary function symbol, and ₁ and ₁ are constant symbols. In

this exercise you are asked to revisit parts of the proof of Theorem 58 relative to a particular

E-structure A. More precisely, you have to show below that, given an arbitrary WFF ZOL (Σ, Ø):

A = 4 ⇒ H = 4,

where H is the Herbrand E-structure induced by A. We define A (A, RA, JA, GA, C4, C₁4)

where A = Nand:

RA =

fA

g-A

=

{(m, n) | m, n € N with m

{(m, m + 2) | m €N}

{(m, n, m+n) | m, n {N}

(R is the binary less-than relation on N)

(fA is the two-successor function on N)

(g4 is the addition function on N)

and c = 0 and ₁ = 1. More succintly, we can therefore write A (N,<, fA, +, 0, 1)

where we use < and + in infix position. There are four parts:

1. We want you to write an inductive definition of Terms(E, 0) in a particular way. The set

Terms(E, ) is the smallest such that:

Terms(Σ, Ø) 2 {co, c₁} U {f(t)|te Terms(Σ, Ø)} U ...

You have to complete the definition.

2. Define the Herbrand E-structure H induced by A:

H(Terms(Σ, Ø), R², f, g, co, c₁)

As in the proof of Theorem 58, you only need to define the relation RH.

3. Let t₁,12 € Terms(E, Ø) be arbitrary terms. Define an algorithm that decides whether

HRH (t₁, 1₂) or HR (t1, t2) depending on the syntactic structure of t1 and 12.

Hint 1: An initial part of your algorithm transforms an arbitrary t Terms(Σ, Ø) into a

term u of the form f(P) co or fe such that t = u, for some p>0, where we write f(P)

to denote that f is applied p times.

Hint 2: The rest of your algorithm decides whether HR (₁, 2) or H = R¹ (U₁, 1₂)

where each of u₁ and u₂ is of the form fp) co or f()c₁.

H

by structural induction on the

4. Prove, for every WFF (E, Ø), that A

201

definition of p.