Why is Form$(x)$ a Primitive recursive relation?

Question

I need help with a question regarding primitive recursion and Gödel's incompleteness theorem. I am really confused right now and I hope you can help me.

Problem:

Let $FR(x)$ denote the primitive recursive relation that says that $x$ is the Gödel code of a sequence of (Gödel codes of) formulas each of which is atomic or has been obtained from previous elements in the sequence through the operations of disjunction, negation or generalization.

1. Let: $$\text{Form}(x)\Leftrightarrow\exists n(n\leq(Pr(l(x)^2))^{xl(x)^2}\land FR(n)\land x=l(n)GLn)$$

Where $Pr(n)$ is the $n$-th prime number, $l(x)$ is the length of $x$ and $nGLx$ is the $n$-th number in the sequence coded by $x$.

1. By using that all these functions are primitive recursive, I want to prove that Form$(x)$ is a primitive recursive relation.

2. I want to understand why, if the bound on $n$ is correct, Form$(x)$ if and only if $x$ is the Gödel code of a formula.

---

1. I might be totally lost, but from here:

https://www.encyclopediaofmath.org/index.php/Primitive_recursive_function

I can read

The class of primitive recursive relations is closed under the application of logical connectives (including negation) and bounded quantifiers.

$n$ is bounded and other than that we only use logical connectives. Since all functions are primitive recursive, the relation must be primitive recursive. I am not sure if this is a legit argument :(

2. Assume Form$(x)$. Then we know from $n\leq(Pr(l(x)^2))^{xl(x)^2}$ that $n$ is finite (?) (is this all it tells us?). $FR(n)$ means that $n$ is the Gödel code to a sequence. Hence $n=2^{e_1}\cdot 3^{e_2}\cdots p_m^{e_m}$. So clearly $l(n)GL_n=e_m$ is also the Gödel code to a sequence. But we have that $x=e_m$ which means that $x$ is the Gödel code to a sequence.

Assume $x$ is the Gödel code to a sequence. I don't really know how to go from this side and conclude $Form(x)$. Not even how to begin.

---

I would be really happy if you could explain 1. and 2. to me. That would, hopefully, make me understand these concepts better. Thank you.

Answer 1

1. $Form(x)$ is a primitive recursive relation because it is the logical conjunction of several relations, each of which is primitive recursive, and, as you found out yourself, the logica conjunction of primitive recursive relations is a primitive recursion relaion itself. Now, why are the other relations primitive recursive?

   • $FR(x)$) we are simply told is primitive recursive ( though I am sure the text you got this from will show it is primitive recursive)

   • $\exists n(n\leq(Pr(l(x)^2))^{xl(x)^2}$ is the bounded quantification of a known primitive recursive relation ($\le$) into which we have substituted the composition of well some known primitive recursive functions, and since substitution and bounded quantification retains primitive recursiveness, the whole thing is therefore primitive recursive

   • $x=l(n)GLn)$ is another known primitive recursive relation ($=$) into which we have substituted a primitive recursive function, and is therefore a primitive recursive relation

2. The importance of $n\leq(Pr(l(x)^2))^{xl(x)^2}$ is that here we have an upper bound to the possible Godel number of any expression of length $l(x)$. And $FR(x)$ holds when $x$ is the result of sequentially applying logical operators on atomic formulas ... which is exactly how a formula in logic is recursively defined