Whenever you have a structure M of some language L you can take the so called complete theory of the structure, denoted Th(M), which is just the set of all L-sentences true in M. In particular if L is the language of PA and M are the standard natural number with the standard operations Th(M) is a theory called true arithmetic. This theory is complete (that's because Th(M) is always complete) and clearly enough to talk about the integers, but it escapes Gödel's theorem since it's axioms are not recursively axiomatizable.
You seem to be confusing "true" and "provable", as far as first order logic is concerned those are equivalent (by another theorem of Gödel, the completeness theorem), but the first in defined in terms of models and the second is purely syntactic
Informally speaking we can take the set of all real numbers. Assuming we are using standard mathematics that most working mathematicians use then this includes non-computable numbers. Sets don’t have to be computable to be used unless you are someone who works with non-standard models of set theory.
I specified I'm working in standard first order logic. And I'm not sure what do you mean with the informal take.
Also intuitionist logic is not my area, but isn't it divided in inference rules for provability and (Heyting or Kripke) semantic for model theory and truth just like FOL?
You may be working in classical logic, but that doesn’t mean the parent poster is. You asserted the parent poster seems to be confused, but what the parent poster said makes sense in a constructive setting. Please see my other comment:
The point is that the set of all true statements about arithmetic [1] exists “out there” (and thus as a “theory” in a very general sense) even if we can’t identify it.
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”
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.
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.
You seem to be confusing "true" and "provable", as far as first order logic is concerned those are equivalent (by another theorem of Gödel, the completeness theorem), but the first in defined in terms of models and the second is purely syntactic