# Proving the free occurrence of a variable is primitive recursive

Show that FreeOcc$(m,n,i)$, which holds when $m$ is the godel number of a wff $\varphi$ and the $i^{th}$ symbol of $\varphi$ is a free occurrence of the variable $x_{n}$, is primitive recursive.

This is a homework question for a Logic III class and I am looking for a suggestion for finishing off the last part. I will show what I have come up with thus far and I am looking for an answer that consists of a hint in the right direction for how to solve my problem with finishing the question. Please no full solutions, I consider it cheating!

Let the standard Godel numbering codes be used where variables are even numbers ($v_{1}: 2, v_{2}: 4,...$) and $\forall: 11$ and $\exists: 13$. FreeOcc$(m,n,i)$ will have three conjunctions, which must all hold true, in order to be satisfied. These three conjunctions will ensure that $(1)$ $m$ is the Godel number of $\varphi$; $(2)$ the $i^{th}$ symbol of $\varphi$ is a variable; and $(3)$ the $n^{th}$ variable is a free occurrence in $\varphi$. For $(1)$, we simply have $\overline{m}=\ulcorner \varphi \urcorner$. For $(2)$, we want to ensure that the $i^{th}$ exponent of the prime fractorization of $\ulcorner m \urcorner$ is the $n^{th}$ variable. This can be accomplished by $\text{exp}(m,i)=2n$, where exp$(m,i)$ returns the exponent of $\pi_{i}$ in the prime factorization of $m$. For $(3)$, we want to ensure that $n$ is in fact a free occurrence in $\varphi$; that is, either $\varphi$ consists of no quantifiers or there are no quantifiers over $n$. This will consist of a disjunction for whether or not the first or second of these two cases occur. In the first case, we have $\forall y ((\text{exp}(m,y) \neq 11) \wedge (\text{exp}(m,y) \neq 13))$. For the second case, we require that $\neg \exists k((\ulcorner \forall \urcorner \star \ulcorner k \urcorner ... \ulcorner k \urcorner = \ulcorner 2n \urcorner) \vee (\ulcorner \exists \urcorner \star \ulcorner k \urcorner ... \ulcorner k \urcorner = \ulcorner 2n \urcorner))$, where $a \star b$ is the concatenation function.

My problem is with what to do with the $"..."$ in the last disjunct of the third conjunct. I want to have it say that there cannot exist a quantifier over $k$ such that $k=2n$ is bounded by it, and I cannot figure it out! I have tried doing so many different concatentations and combinations of cases but there just seems to be too much structure to tame.

Does anyone have any ideas on how I could finish the last disjunct of the third conjunct?

I actually came up with this while I was dreaming and woke up and scribbled it down, but it works like this where $len(m)$ returns the length of the wff defined by godel number $n$, $\lambda$ is a string of arbitrary quantifiers and variables, ie. $\forall x_{n+1} \forall x_{n-1} \exists x_{n} \forall x_{n+4}$, and $exp(m,n)$ returns the $n^{th}$ exponent of the godel number $m$ in it's prime factorization.

Copy into LaTeX: $$\text{FreeOcc}(m,n,i) = &(\text{Wff}(m)) \wedge (\text{exp}(m,i)=2n) \wedge \\ &(\text{exp}(m,i-1)\neq 11) \wedge (\text{exp}(m,i-1)\neq 13) \wedge (\psi) \\ &[(\forall j < i)(((\text{exp}(m,j)=17) \wedge (\exp(m,j-1)=2n) \wedge \\ &((\text{exp}(m,j-2)=11) \vee (\text{exp}(m,j-2)=13))))] \Rightarrow \\ &[(\forall j < i)(\exists k < i)(\text{exp}(m,k)=19)] \\ &[(\forall j < i)(((\text{exp}(m,j)=17) \wedge (\exp(m,j-3)=2n) \wedge \\ &((\text{exp}(m,j-4)=11) \vee (\text{exp}(m,j-4)=13))))] \Rightarrow \\ &[(\forall j < i)(\exists k < i)(\text{exp}(m,k)=19)] \\ &\wedge \cdot \cdot \cdot \wedge \\ &[(\forall j < i)(((\text{exp}(m,j)=17) \wedge (\exp(m,j-\text{len}(\ulcorner \lambda \urcorner) +1)=2n) \wedge \\ &((\text{exp}(m,j-\text{len}(\ulcorner \lambda \urcorner))=11) \vee (\text{exp}(m,j-\text{len}(\ulcorner \lambda \urcorner)=13))))] \Rightarrow \\ &[(\forall j < i)(\exists k < i)(\text{exp}(m,k)=19)]$$

-

Your thoughts on part (3) of your solution appear to be slightly incorrect. It is not true that an occurrence of a variable $x_i$ in a formula $\varphi$ is free only in the case of there being no quantification of $x_n$ in $\varphi$, but only if no subformula of $\varphi$ beginning with a quantification of $x_n$ contains that occurrence of $x_n$.

With this in mind, you could attempt to model the following in a formula: for all $j < i$, if the $j$th symbol of $\varphi$ begins a quantification over $x_n$ (i.e., the $j$th symbol s either $\exists$ or $\forall$ and the $(j+1)$st symbol is $x_n$, or something similar depending on the use of parentheses in the definition of formulae), then the subformula of $\varphi$ determined by the quantification has length $< i-j$ (or, perhaps, there is a $k < i$ such that the subexpression of $\varphi$ obtained by taking the $j$th through $k$th symbols of $\varphi$ is a formula).

-
Thanks for the suggestion I ended up doing something similar to what you suggested although it ended up being a ton more complicated. If you are interested I edited the question to include the final answer. – Samuel Reid Mar 22 '12 at 3:40

I would start by proving that the relation

• $R(m,n,i,\ell)\equiv{}$ "$m$ is the Gödel number of a wff such that the $i$th symbol is the beginning of a sub-wff at level $\ell$ in the parse tree that is not in the scope of a binding of $x_n$".

is primitive recursive. This should be fairly easy by recursion on $\ell$, and afterwards you can eliminate $\ell$ by bounded quantification.

-
I am not very familiar with parse trees, are there any other methods that you would suggest? – Samuel Reid Mar 19 '12 at 3:41