# Proving $\square(\forall v_1\neg\psi(v_1))\rightarrow\forall v_1\neg\psi(v_1)$ for a particular $\psi$.

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