# Finitary character of definition of representing function in primitive recursion theory

I have been studying primitive recursive functions for a while now using Kleene's "Introduction to Metamathematics". He says in his book that "We say that a function $$\phi(x_1, ..., x_n)$$ is the representing function of a predicate $$P(x_1, ..., x_n)$$ if $$\phi$$ takes only values $$0$$ and $$1$$, and is $$0$$ when predicate is true and $$1$$ when predicate is false."

I have trouble understanding this definition. We want the theory of primitive recursive functions to be finitary just as metamathematics because we will apply this theory of primitive recursive functions to prove Godel's theorem (according to Kleene).

I have trouble understanding what does finitary means here and how it is the case that this definition is finitary. So, if I understand correctly, then predicate is some rule which for each of its variables gives values true or false depending on to each variable being a specific natural number. Now, if I want to show that predicate has representing function then for all possible values I should check whether when $$P$$ evaluates to true $$\phi$$ evaluates to $$0$$, and when $$P$$ evalutes to false, $$\phi$$ evaluates to $$1$$. But because the domain is not finite, that would require me infinite steps. Isn't that a deviation from the plan of this theory being finitary?

I would appreciate your help and suggestions. Probably I am not quite understanding the whole goal of primitive recursive functions and I am being confused by definitions.

• Not every predicate will have a "nice" representing function. The point, though, is that it will turn out that many predicates do happen to have primitive recursive representing functions. – Noah Schweber Oct 17 '18 at 1:09
• @NoahSchweber Can you please comment on apparent circularity in primitive recursive function theory? It seems that it uses number-theoretic functions, prime numbers and so forth which we want to axiomatize to prove some results in metatheory (Godel's theorem) which was supposed to be finitary. How is it okay to prove things about formal number theory using results from number theory such as prime number decomposition. – Daniels Krimans Oct 17 '18 at 3:14
• It is not circular to use number theory to prove things about a formal system describing the natural numbers. Any more than it is circular to refer to sets of logical operators and sets of sentences when we're talking about logic (even though set theory is built on logic). We are mathematicians, reasoning about strings of symbols obeying rules, etc. – spaceisdarkgreen Oct 17 '18 at 4:18
• There is a pertinent question in here "is it really finitistically acceptable to use prime factorization in this way?" (e.g. can it be formalized in PRA?) but unless you're an avowed finitist it's probably more instructive to convince yourself as an ordinary mathematical reasoner of the correctness of Godel's argument first before looking to the technical details of how strong a metatheory is necessary to carry it out formally. – spaceisdarkgreen Oct 17 '18 at 4:21