Enumerable predicate

An arithmetic predicate $P(x_1,\dots,x_n)$ is called enumerable relative to a given formal system $S$ of arithmetic if it has the following property: There is a formula $F(x_1,\dots,x_n)$ in the language of formal arithmetic (cf. Arithmetic, formal) such that for any natural numbers $k_1,\dots,k_n$,

1) if $P(k_1,\dots,k_n)$ is true, then $\vdash_SF(k_1,\dots,k_n)$;

2) if $P(k_1,\dots,k_n)$ is false, then $\vdash_S\neg F(k_1,\dots,k_n)$, where $\vdash_S$ means derivability in $S$ and $F(k_1,\dots,k_n)$ is the result of substituting in $F(x_1,\dots,x_n)$ for the variables $x_1,\dots,x_n$ terms representing the numbers $k_1,\dots,k_n$. In this case one says that the formula $F(x_1,\dots,x_n)$ is an enumerability predicate for $P(x_1,\dots,x_n)$. For a formal system $S$ of arithmetic the following proposition holds: All recursive predicates, and only they, are enumerability predicates in $S$.

An $n$-place arithmetic function $f$ is called enumerable if there is an arithmetic formula $F(x_1,\dots,x_n,y)$ such that for any natural numbers $k_1,\dots,k_n,l$,

1) if $f(k_1,\dots,k_n)=l$, then $\vdash_SF(k_1,\dots,k_n,l)$;

2) $\vdash_S\exists yF(k_1,\dots,k_n,y)\land\forall x\forall y(F(k_1,\dots,k_n,x)\land F(k_1,\dots,k_n,y)\supset x=y)$.

In the ordinary formal system of arithmetic all general recursive functions, and only they, are enumerable (cf. General recursive function).

References

[1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)

Comments

Predicates $P$ (functions $f$) satisfying 1), 2) are more commonly called definable in the system $S$.