CS245 regarding countability decidability

• Form a set of clauses Σ such that Σ r TIMES(t1, t2, t3) whenever n1 · n2 = n3;
• Show a resolution refutation of TIMES(s(s(0), s(0), s(s(0)))) w.r.t. Σ from above;
• Is the set of terms {f (t1, t2, t3) | n1 · n2 = n3} recursive?

For the first two parts you may use the clauses that define PLUS given in class.

Question 2 (10pt)
Let P be a ternary predicate symbol. Show that if ∀x.∀y.∃z.P (x, y, z) is satisfiable then also
∀x.∀y.P (x, y, f (x, y)) is satisfiable.
Question 3 (20pt)
Let Λ be a non-empty finite alphabet (set of symbols). Show that

(a) the set Λ∗ of all finite strings over Λ is countable ; and

Let P be a ternary predicate symbol. Show that if ∀x.∀y.∃z.P(x,y,z) is satisfiable, then also ∀x.∀y.P(x,y,f(x,y)) is satisfiable.

Assume ∀x.∀y.∃z.P(x,y,z) holds.
Then for arbitrary α,βϵD, there exists some γϵD such that a substitution θ makes P true.
The arbitrary substitution for I,θ[u∕α,v∕β,w∕γ]P(u,v,w) true, where u,v,w are subsituted and do not occur in P(x,y,z). Let θ′ be an arbitrary interpretation of domain D, such that θ′ agrees with θ, except for fθ′(α,β) = γ (where f is some function).
Since ∀x.∀y.∃z, by Skolemization method for removing existential quantifiers, a subsitution θ′ contains a function f based upon x and y, so that: I,θ′[u∕α,v∕β,w∕fθ′(α,β)]P(u,v,x).
Since f(u,v)θ′[u∕α,v∕β] = fθ′(α,β) = wθ′[u∕α,v∕β,w∕fθ′(α,β)] , meaning the arbituary w can be expressed in terms of a subsitution θ′. Thus I,θ′[u∕α,v∕β,w∕fθ′(α,β)]P(u,v,f(u,v)).
And it follows that ∀x.∀y.P(x,y,f(x,y)).

□

(Question 3)

Let Λ be a non-empty set of finite alphabets.

(a)

The set Λ* of all finite strings over Λ is countable.

We show there is an injection mapping f : Λ*→ ℕ to the naturals. Let k denote the size of the alphabet, k = |Λ|. To show countability, we introduce a method to inject the length of a string to the naturals. E.g.
strings of length 1 = k
strings of length 2 = k × k = k2
strings of length * = k × ... × k = k*
With this injection, any subset of strings can be counted and thus injected into the naturals. All of the Λ* sub-strings are countable, and the union of all countable subsets is also countable. Since Λ* is a set of finite strings, and the string length maps to a natural number, Λ* is countable.
□
(b)

The set of all countably-infinite sequences of alphabets from Λ is not countable.

By contradiction and Cantor’s diagonalization, a string τn, where n denotes the arbitrary length of the string, can be constructed such that it is not in the set S of all countably-infinite sequence of alphabets. We show that τn is a string constructed from the alphabets Λ, but it is not in the set S.
Suppose S is countable. Then there exists a one-to-one correspondence that the elements s1,s2,...ϵS has a corresponding partner n1,n2,...ϵℕ. We claim that such a correspondence does not exist by constructing a string τn to be different from every string in the set by at least one alphabet. We construct it in a diagonalization fashion:
In τn, we change 1st alphabet at the first position in string s1. Then change 2nd alphabet at the second position in string s2.
For example, let Γ be the English alphabet, and s1,s2,...ϵS be arbitrary. If s1 = ”abc”, and s2 = ”def”, then when constructing τn: we pick a character that is not a from s1, and from s2 a character that is not e. In general, the ith alphabet in τn at the ith position in string si is to be replaced by some other alphabet. Continuing in this fashion generates a string τn that differs from every subset string s1,s2,...ϵS. Hence the stringτn has no partner from S. Thus there is no one-to-one correspondence, and hence S is uncountable.
□
(Question 4)

Show that the satisfiability of first order logic (FOL) formula is undecidable.

Suppose it was decidable. Then that means given any FOL formula, there is an algorithm (another FOL formula) such that it can decide whether some formula is satisfiable. Okay, suppose such an algorithm exists. Let us denote it by SATISFIABLE(x), where x is any FOL formula. Hence ∀xSATISFIABLE(x) would return a true if the input x was satisfiable, false if unsatisfiable. Now we write a new FOL formula EV IL(x) that calls SATISFIABLE, and returns its validity as follows:
Call SATISFIABLE(x)
If (true): return false.
Otherwise: return true.
We feed the EV IL formula to SATISFIABLE. We claim that SATISFIABLE(EV IL) is a formula that cannot exist. Here is what a trace of the execution looks like:

SATISIFABLE looks at EV IL and tries to determine if EV IL is satisfiable.
However, EV IL bases its result on SATISFIABLE’s result.
Whatever the result is from SATISFIABLE, it makes EV IL unsatisfiable.
From this, we see that:

If EV IL is satisfiable, then SATISFIABLE(EV IL) is unsatisfiable. But this is a contradiction, because it implies EV IL is unsatisfiable.
If EV IL is unsatisfiable, then SATISFIABLE(EV IL) is satisfiable. Again, this is a contradiction, because SATISFIABLE says EV IL is satisfiable.
We can conclude that no matter what the result is of this execution, there are only contradictory results. This means the algorithm SATISFIABLE cannot form a valid conclusion - as the conclusions are all contradictory. Hence our assumption must be wrong, and hence the satisfiability of FOL formula is undecidable.
□
(Question 4) Bonus

For extra 10pt bonus show that satisfiability of first order formula is not recursively enumerable.

Suppose the set Σ of satisfiable first order formula is recursively enumerable. By definition, Σ is recursive if and only if Σ and its complement Σ are recursively enumerable. If we can tell if xϵΣ, we have to be able to decide if x is not a member of Σ.
Since Σ andΣ are recursive sets, then by definition there exist Turing machines that accept them. Let MΣ accept the set Σ and MΣ accept its compliment Σ. Now consider the following construction of such a machine:

M(x) returns 1 if MΣ(x) halts. M(x) returns 0 if MΣ(x) halts.