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)]$