Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question
up vote 1 down vote accepted

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

share|cite|improve this answer
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.

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.