# 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)