Clausal Language (ver. 5.81.20, 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.

Chapter. Primitive Recursive Functions.

Section. Pairing Function and Arithmetization.

Subsection. Catalan Pairing Function. See the section 3.2 Course of Values Recursion in [2].

[CL] Remark. The Catalan pairing function $x, y$ is pre-defined in CL.

Basic properties of Catalan pairing function. We have

x_{1}, x_{2} = y_{1}, y_{2} \to x_{1} = y_{1} \land x_{2} = y_{2}

x < x, y \land y < x, y

x = 0 \lor \exists y \exists z x = y, z

Ordering properties of Catalan pairing function. We have

x_{1}, x_{2} < y_{1}, y_{2} \leftrightarrow | x_{1}, x_{2} |_{p} < | y_{1}, y_{2} |_{p} \lor | x_{1}, x_{2} |_{p} = | y_{1}, y_{2} |_{p} \land (x_{1} < y_{1} \lor x_{1} = y_{1} \land x_{2} < y_{2})

where $| x |_{p}$ is the pair size function defined in the module Standard.

[CL] Remark. The membership predicate $x &CLin; y$ , where

x &CLin; y \leftrightarrow \exists i (i < L (y) \land x = {(y)}_{i})

is pre-defined in CL. Notation for its negation is $x \notin y$ .

Bounded quantification with membership predicate. Note that we have

x &CLin; y \to x < y

Consequently, existential and universal quantifiers in contexts like

\exists x (x &CLin; y \land \dots)

\forall x (x &CLin; y \to \dots)

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

[CL] Syntax. Examples: