In CTT truth of a proposition, indeed, is expressed as the instantiation of its set of proofs: (1) A is true = Proof(A) exists, where the existence is the Brouwer-Weyl constrcutive notion of existence, defined by the assertion condition: a is an ALPHA. Therefore: ALPHA exists. Consider now what we may call the "arithmetical fragment" of CTT, given in the language that comprises the connectives and quantifiers, and the natural numbers, plus the appropriate constructors, with the usual introdcution and elimination rules for the connectives and quantifiers, and the definition by recursion as elimination rule for the set N. Gödel's theorem then takes the form: there is an an arithemtical proposition G, for which we can construct a proof-object, but this cannot be done using just the constructors pertaining only to the artimetical fragment. This takes care of question 1. Question 2: The set Proof(G) is instantiated by a proof-object t, but this cannot be given just by using the "arithmetical constructors". Question 3: the standard CTT notion of propositional truth given by (1). I have dealt with these matters in some detail in my 'Antirealism and the Roles of Truth' in the Handbook of Epistemology. The article can be found here https://openaccess.leidenuniv.nl/bitstream/handle/1887/12024/9_054_043.pdf?sequence=1 and § 8, pp. 456-459, spells out the Gödel issues for CTT.

In CTT truth of a proposition, indeed, is expressed as the instantiation of its set of proofs:

$$ A \text{ is true } = \mathsf{Proof}(A) \text{ exists} \tag{1} $$

where the existence is the Brouwer-Weyl constrcutive notion of existence, defined by the assertion condition:

$$a \text{ is an } \alpha \implies \alpha \text{ exists} $$

Consider now what we may call the "arithmetical fragment" of CTT, given in the language that comprises the connectives and quantifiers, and the natural numbers, plus the appropriate constructors, with the usual introdcution and elimination rules for the connectives and quantifiers, and the definition by recursion as elimination rule for the set $\mathbb{N}$.

Question 1: Gödel's theorem then takes the form: there is an an arithmetical proposition $G$, for which we can construct a proof-object, but this cannot be done using just the constructors pertaining only to the arithmetical fragment. This takes care of question 1.

Question 2: The set $\mathsf{Proof}(G)$ is instantiated by a proof-object $t$, but this cannot be given just by using the "arithmetical constructors".

Question 3: the standard CTT notion of propositional truth given by $(1)$. I have dealt with these matters in some detail in my 'Antirealism and the Roles of Truth' in the Handbook of Epistemology. The article can be found here and §8, pp. 456-459, spells out the Gödel issues for CTT.