[mietek]

You are invoking a classical notion of existence.

This is not acceptable to a constructivist, for whom “a statement is true if we have a proof of it, and false if we can show that the assumption that there is a proof for the statement leads to a contradiction”[1]. The parent poster, whatshisface, may be a constructivist.

[1] Troelstra A., D. van Dalen (1988) “Constructivism in mathematics: an introduction”

[antidesitter]

In the case of True Arithmetic, the true statements are the axioms. Thus a proof of any true statement consists of just invoking the corresponding axiom, which is a valid proof in any formal system (constructive or otherwise).

The weirdness of True Arithmetic comes not from proofs (which are trivial) but from the axioms themselves. You can object that it’s not a “reasonable” or “proper” theory because it’s not recusively axiomatizable (i.e. there’s no effective procedure for even deciding whether a statement is an axiom), but I don’t think that objection is specifically constructivist.

[mietek]

Indeed, the objection is against the method by which this system is supposed to be defined. As you say, we start with an implicit assumption that we don’t have an effective procedure to construct the set of statements that are true in the ambient metatheory. And so, this set exists in a classical sense, or “weakly exists”, and not in a constructive sense.