I have a formula $\psi(v_1)$ that is equivalent in $\mathrm{PA}$ to

$$\exists a\exists b\exists c\left[\neg\exists x\overline{\mathrm{Prf}}(x,c)\wedge\mathrm{Neg}(b,c)\wedge\mathrm{Sub}\left(a,\overline{\ulcorner\psi\urcorner},1,b\right)\wedge\mathrm{Num}\left(v_1+1,a\right)\right]\text{,}$$

where

  • $\mathrm{Neg}$ represents the function that assigns to $x$ the Gödel number $\ulcorner\neg\chi\urcorner$ if $x$ is the Gödel number of a formula $\chi$, and $0$ otherwise;
  • $\mathrm{Sub}$ provably represents the function that assigns to $(x,y,i)$ the value $\ulcorner\chi\left[t/v_i\right]\urcorner$ if $x$ is the Gödel number of some term $t$, and $y$ is the Gödel number of some formula $\chi$ such that $t$ is free for $v_i$ in $\chi$, and $0$ otherwise;
  • $\mathrm{Num}$ provably represents the function $n\mapsto\ulcorner\overline{n}\urcorner$;
  • $\overline{\mathrm{Prf}}$ provably represents the relation, "the proof with Gödel number $x$ proves the formula with Gödel number $c$."

Note that the representation $\mathrm{Neg}$ isn't assumed to be provable.

I'm then asked to show that

$$\mathrm{PA}\vdash\square\left(\forall v_1\neg\psi\left(v_1\right)\right)\rightarrow\forall v_1\neg\psi\left(v_1\right)\text{,}$$

so that I can apply Löb's theorem.

The question is easy enough in the standard model, since there we have that $\neg\psi\left(n\right)$ is equivalent to $\square\left(\neg\psi\left(n+1\right)\right)$, but to find that equivalence I've assumed that $c$ exists and does in fact code $\neg\psi\left(n+1\right)$, but I don't think I can assume anything like that in $\mathrm{PA}$.

Does anyone have any suggestions?

Edit: Actually I just realised that it's even more trivial than I thought for the standard model, since there we always have $\square\phi\rightarrow\phi$, so I should have said "it's easy enough for numerals because..."

(Also thank you to Git Gud for adding tags.)

Your Answer

 

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.