In classical logic, Godel shows that there are true statements undecidable for arithmetic, and consequently, that truth goes beyond a system of axioms ability for proof. My question is, given that intuitionists hold that a true statement is just one we have constructed in a given language, and given that the incompleteness theorems hold in intuitionistic logic, can the intuitionist agree that the Godel sentence for their logic is true?
Obviously, the Godel sentence cannot be constructively proven and so they cannot hold it to be true in that sense, but our proof that it is indeed true is metatheoretical, so I'm struggling to see whether they are able to agree that it is true but unprovable, or whether they must regard it undetermined.
Thanks.
Heyting arithmetic (HA) is the Peano Axioms under constructive logic, while Peano Arithmetic (PA) is Heyting Arithmetic + every instance of excluded middle.
Let's start with the version for an arbitrary potentially constructive theory $T$ with a Godel numbering system that extends HA. Let $\DeclareMathOperator{provable}{provable}$$\provable$ be a provability predicate, phrased as a statement in HA, satisfying the Hilbert-Barnays conditions. Note here that we must constructively prove the meta-thereoretic parts of these three conditions, but for various reasons a classical proof of these three conditions almost always can be translated algorithmically into a constructive proof in practice.
Using the Diagonal Lemma (which is constructive), take some $\phi$ such that $T \vdash \phi \iff \neg \provable(\ulcorner \phi \urcorner)$. In particular, $T \vdash \phi \to \neg \provable(\ulcorner \phi \urcorner)$, and thus $T \vdash \provable(\ulcorner \phi \to \neg \provable(\ulcorner \phi \urcorner) \urcorner)$ by Hilbert-Barnays 1.
Working within $T$:
Suppose that $\provable(\ulcorner \phi \urcorner)$. Then $\provable(\ulcorner \provable(\ulcorner \phi \urcorner) \urcorner)$ by Hilbert-Barnays condition 2.
Also, since we have $\provable(\ulcorner \phi \urcorner)$ and $\provable(\ulcorner \phi \to \neg \provable(\ulcorner \phi \urcorner) \urcorner)$, we have $\provable(\ulcorner \neg \provable(\ulcorner \phi \urcorner) \urcorner)$.
Recalling that $\neg P$ is "syntactic sugar" for $P \to \bot$. Since we have $\provable(\ulcorner \provable(\ulcorner \phi \urcorner) \urcorner)$ and $\provable(\ulcorner \provable(\ulcorner \phi \urcorner) \to \bot \urcorner)$, we again apply Hilbert-Barnays 2 to get $\provable(\ulcorner \bot \urcorner)$.
So we have proved in $T$ that $\provable(\ulcorner \phi \urcorner) \to \provable(\ulcorner \bot \urcorner)$. $\square$
In other words, $T$ proves that if $\phi$ is provable, then $T$ is inconsistent. Taking the contrapositive, we see that $T$ proves that if $T$ is consistent, then $\neg \provable(\ulcorner \phi \urcorner)$. In other words, if $T$ is consistent, then $\phi$.
Now let's say we're working in a metatheory which (1) interprets HA in a canonical way, (2) proves $T$ is consistent, and (3) proves that all HA statements provable in $\phi$ hold in the canonical interpretation of HA. Then this metatheory proves that the HA interpretation of $\phi$ is true.
So there is no constructive problem with dealing with the truth of Godel statements (any more than there is a classical problem).
Note that an alternate tactic is proving that $\provable$ is a Hilbert-Barnays predicate for HA. Then as long as $\provable$ actually corresponds to $T$-provability, the proof goes through. This allows us to prove, for instance, the Godel sentence for PA.