Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Recursive Functions. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Lecture Notes in Theory of Computability. 2001.
[3] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
[4] I. Korec. Úvod do teórie algoritmov. Skriptá MFF UK, 1981.

[CL] CL-TeX.

[CL] Membership predicate. The predicate $x ϵ y$ is built into CL. Recall that we have

x ϵ y \leftrightarrow \exists i (i < L (y) \land x = {(y)}_{i})

We write $x \notin y$ as an abbreviation for $\neg x ϵ y$ .

Bounded quantification with membership predicate. Note that we have

x ϵ y \to x < y

Consequently, existential and universal quantifiers in contexts like

\exists x (x ϵ y \land \dots)

\forall x (x ϵ y \to \dots)

are in fact bounded. Such quantifiers can be used in explicit definitions of predicates with bounded formulas.

Syntax. Examples:

bounded quantifiers $\exists y y ϵ x : R$ and $\forall y y ϵ x : R$
explicit definitions of predicates

Predicate $R$
$R (x) \leftrightarrow \exists y y ϵ x : Q (x, y)$

Predicate $R$
$R (x) \leftrightarrow \forall y y ϵ x : Q (x, y)$

Chapter. General Recursive Functions.

Section. Beyond Primitive Recursion: Ackermann Function.

Subsection. Ackermann-Péter Function.

Ackermann-Péter function.

A (0, y) = y + 1

A (x + 1, 0) = A (x, 1)

A (x + 1, y + 1) = A (x, A (x + 1, y))

Course of values sequences. The sequence $s$ is said to be a course of values sequence for the Ackermann-Péter function if we have

$s$ consists solely of triples of the form $x, y, A (x, y)$ , i.e.
$\forall a (a ϵ s \to \exists x \exists y a = x, y, A (x, y))$
if $x, y, A (x, y) ϵ s$ then $s$ contains all earlier triples $x_{1}, y_{1}, A (x_{1}, y_{1})$ that are needed to calculate $A (x, y)$

Course of values predicate. By $Cvs (s)$ we denote the predicate holding of course of values sequences for the Ackermann-Péter function. Note that the predicate satisfies the following existence and uniqueness conditions:

\forall x \forall y \exists s (Cvs (s) \land \exists z x, y, z ϵ s)

Cvs (s_{1}) \land x, y, z_{1} ϵ s_{1} \land Cvs (s_{2}) \land x, y, z_{2} ϵ s_{2} \to z_{1} = z_{2}

Exercise. Show that the course of values predicate $Cvs (s)$ is primitive recursive.

Hint. Note that we have

A (x, y) = z \to x < z \land y < z

A (0, y) = z \leftrightarrow z = y + 1

A (x + 1, 0) = z \leftrightarrow A (x, 1) = z

A (x + 1, y + 1) = z \leftrightarrow \exists v v < z : (A (x + 1, y) = v \land A (x, v) = z)

Cvs (s) \leftrightarrow ?

Exercise. (4 bonus points) Show that the graph $G (x, y, z)$ of the Ackermann-Péter function

G (x, y, z) \leftrightarrow A (x, y) = z

is primitive recursive.

b (z) = ?

G (x, y, z) \leftrightarrow ?