Minimal arithmetic proving a statement similar to a Gödel sentence

I will use $\textbf{Q}$ to denote minimal arithmetic for this post. (I suppose Robinson arithmetic would also suffice (?))

Suppose we have $F(x)$ be a formula defining, in $\textbf{Q}$ the primitive recursive relation "$x$ is a sentence of the language of arithmetic". Let $G$ be such that

$\textbf{Q}\vdash G \leftrightarrow F(\ulcorner G \urcorner)$

I am trying to determine whether or not $\textbf{Q} \vdash G$.

• Am I missing something? What if $G$ is simply false? – Hagen von Eitzen May 13 '16 at 6:19
• @HagenvonEitzen Is it simply that being a sentence in the language of arithmetic and being proven in the language of arithmetic are different things? – faux May 13 '16 at 6:28
• Suppose $Q \vdash G \leftrightarrow F(\ulcorner G \urcorner)$. Since $G$ is a sentence, $F(\ulcorner G \urcorner)$ is true, so by $\Sigma_0$-completeness of $Q$ we have $Q \vdash G$. Does that work? – Alex McKenzie May 14 '16 at 13:04
• @HagenvonEitzen: Not all sentences are fixed points of $F \square_Q$. – user21820 May 17 '16 at 2:15
• @AlexMcKenzie: Shouldn't your comment be an answer/hint? – user21820 May 17 '16 at 2:15

Here's how I see this problem (developed somewhat from my comment above): suppose we have $Q \vdash G \leftrightarrow F(\ulcorner G \urcorner)$. Clearly $G$ is a sentence, so $F(\ulcorner G \urcorner)$ holds (i.e. is true in the standard model).
As you point out, the relation "$x$ is a sentence of the language of arithmetic" is primitive recursive, so it has a $\Sigma_0$-formula expressing it. If $F$ is such a $\Sigma_0$ formula, then since $Q$ is $\Sigma_0$-complete, $Q \vdash F(\ulcorner G \urcorner)$, so by the biconditional above $Q \vdash G$.
However, if $F$ was not chosen to be $\Sigma_0$, I don't think we can automatically assume that $Q \vdash F(\ulcorner G \urcorner)$.
• Yup that looks right. We can see intuitively that it's quantifier-free because we only need bounded searches given $x$ to determine whether it is the code of an arithmetical sentence. Of course, we need the extra assumption that the encoding is reasonable, so if you want to be precise you could add that in. Using the code of the witness in the standard model $F$ can be $Σ_1$ and it is still fine, but not $Π_1$, for which a counterexample is $\neg □_Q$, since by the modal fixed point theorem there is a sentence $G$ such that $Q \vdash G \leftrightarrow \neg □_Q G$, but $Q \nvdash G$. – user21820 May 18 '16 at 11:24