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] Remark. Clausal form of function definitions is allowed.

Chapter. General Recursive Functions.

Section. General Recursive Functions.

Definition of general recursive functions.

Theorem. The class of general recursive functions is primitively recursively closed.

Corollary.

Every primitive recursive function is general recursive.
Every primitive recursive predicate is general recursive.
General recursive predicates are closed under explicit definitions of predicates with bounded formulas.

Subsection. Regular Minimalization.

Definitions of functions with regular minimalization.

[CL] Syntax. Example(s):

f (x) = μ y [R (x, y)]

provided the following condition of regularity is satisfied:

\forall x \exists y R (x, y)

Exercise. (1 points) Show that general recursive functions are closed under regular minimalization.

Remark. Prove the claim for the special case in the following theory.

Show that if $R (x, y)$ is a general recursive predicate such that

\forall x \exists y R (x, y)

then so is the function $f (x)$ defined by regular minimalization:

f (x) = μ y [R (x, y)]

Proof.

f (x) = ?

[CL] Remark. You can test your solution by interpreting the theory. Choose non-local interpretation.

Theorem. The class of general recursive functions is closed under definitions of functions with regular minimalization.