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

Ordering properties of Catalan pairing function. We have

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

[CL] Remark. The membership predicate $xϵy$, where

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

Bounded quantification with membership predicate. Note that we have

Consequently, existential and universal quantifiers in contexts like

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

[CL] Syntax. Examples:

• bounded quantifiers $\exists yyϵx:\mathrm{R}$ and $\forall yyϵx:\mathrm{R}$

• explicit definitions of predicates

  Predicate $\mathrm{R}$
  $$\mathrm{R}\left(x\right)\leftrightarrow \exists yyϵx:\mathrm{Q}(x,y)$$
  Predicate $\mathrm{R}$
  $$\mathrm{R}\left(x\right)\leftrightarrow \forall yyϵx:\mathrm{Q}(x,y)$$