Specifically, "mathematical truths" here meams statements that, while logically independent from ZFC, are not independent from e.g. ZFC plus Con(ZFC). Or Con(Con(ZFC)), or Con(for any n, Con^n(ZFC)), or even more elaborate varieties. AIUI, part of what Recursion theory does is characterize these "true" consistency statements. The field is closely related to, e.g. halting oracles in TCS.

True propositions of sets are those that hold in the up to unique isomorphism model of the theory Ordinals defined here:

https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3457802

> some things are indeed undecidable (even if they must be true or false).

What does it mean 'even if they must be true or false'? What does truth and falsehood mean if you cannot in theory prove/disprove a proposition?

You are suggesting the existence of some sort of Platonic realm, where propositions have definite truth/falsehood values, while at the same time being inaccessible to us.

The propositions themselves are not inaccessible, but there is no way to automate the process of testing their truthiness in a way that always works. That is the usual menaning of undecidability.

> The propositions themselves are not inaccessible

Yes, I know. I meant that their truth value is inaccessible. What I'm saying is that claiming 'some things are indeed undecidable (even if they must be true or false)' suggests the existence of a Platonic realm with an existing truth value.

If a proposition is undecidable, it makes no sense to talk about whether 'it actually is true/false', because truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition.

> truth/falsehood is attached to a proposition by virtue of proving/disproving the proposition.

The thing is, this isn't necessarily the case. "Proving/disproving" a proposition can only be done starting from a set of axioms that are independently thought of as "true". But if you think of, e.g. ZFC as true, you'll also think of Con(ZFC) as true, even though the statement of Con(ZFC) can't be proven from ZFC. Similarly for Con(Con(ZFC)) and many sorts of increasingly-complex "consistency" statements.

Ok, now I see your point. It seems you're advocating for intuititionistic logic: you only consider a proposition "true" if you can build a proof for it. Classical logics (and, therefore, classical mathematics) assumes that it makes perfect sense to talk about the truth value of a proposition without computing/proving it. Even undecidable ones are either true or false.

The law of the excluded middle says that for all propositions, either it or its negation must be true.

But Godel showed that there exist propositions for which neither can be proven.

The Law of Excluded Middle says:

   ⊢(Ψ or ~Ψ)

In inferential incompleteness says that there is a proposition Ψ such that:

  (⊬Ψ) and (⊬~Ψ)

> the existence of a Platonic realm with an existing truth value.

This is a standard assumption by mathematicians.

For the [Dedekind 1888] axiomatization of the Natural Numbers, a proposition is true if and only if it holds in the unique up to isomorphism model of the axioms.