I don’t think my position is contradictory: I believe that (non-technical, unqualified/alone) “true” is a property that exists independently of whether we are able to formally prove something in some kind of logic. This is because we are making assertions about “real” objects (e.g. the naturals), and I believe that these statements are either true or false.

I think this is a philosophical disagreement that we’re unlikely to resolve.

It’s not clear to me which definition of (non-technical, unqualified/alone) “true” you are using.

We’ve had a few:

1. Your original definition, where we say P is true iff it holds in all compatible models (which I claim is highly nonstandard);

2. The definition you started using later, where we say P is true iff it holds in all models of ZFC (which I claim is still nonstandard);

3. The definition I suggested, where we say P is true iff it holds in some “standard model”;

4. Something else.

Let’s consider the naturals; what is your opinion on the truth of the Gödel sentence for ZFC (let’s assume consistency, otherwise definition 2 cannot possibly be useful)? Under definition 3 is is true, but under definition 2 it isn’t.

If you think it isn’t true then you are saying that we don’t really understand the naturals intuitively and we can only understand them by axiomatisation.

I cannot counter that position mathematically, only philosophically, but I will say that we have seemingly used and understood the naturals for a very long time before they were first effectively axiomatised, so it seems to be a bold claim.

This is very far away from my original point, however, which was purely about your position that “true” means “true in all models” (i.e. definition 1), however it seems you are no longer adopting this position (in favour of definition 2)?

When used in a technical sense, as far as I am aware “true” is always qualified with respect to some specific model, which may be obvious from context and thus not explicitly stated, but there is always a formal model in mind; truth is generally seen as a model-theoretic concept, not as proof-theoretic one.

Re. ABC and IUTT, I’m fully behind Buzzard et al. pushing for machine verified proofs, as I say, I have been a big user of Coq. I just don’t think we can ever say that proof is what determines truth given we know from Gödel that proof is fundamentally limited.

Proof is a good way of convincing ourselves something is true, indeed anything we prove true is in fact true by soundness, but it’s not the arbiter of truth.