[loicd]

Exactly. A statement is true by definition if and only if it is satisfied in every model. Also, Gödel also proved the completeness theorem that states that a statement is true if and only if it is provable. So, another way to look at undecidability is this: a statement is undecidable if and only if it can be neither proved nor disproved.

[denotational]

UPDATE: since first writing this comment, I’ve checked four quasi-randomly selected books from my shelves (Leary and Kristiansen Introduction to Mathematical Logic, Hodges Model Theory, Manzano Model Theory, Avigad Mathematical Logic and Computation), and they all use valid/validity rather than true/truth to describe formulae that are true in all models, as I originally pointed out below. To be clear, I’m not at all trying to score points by appealing to the literature, but I think it’s really important to clarify that your definition isn’t standard because it will confuse people; I myself was confused by this exact point when I studied logic having previously read the “true but unprovable” description of Gödel 1.

> A statement is true by definition if and only if it is satisfied in every model.

I don’t think this is a standard definition.

Every treatment I’ve seen refers to truth with respect to a model; if no model is specified, it is assumed to be obvious from context. Outside of formal treatments (i.e. in the setting where the 99% of mathematicians who aren’t logicians do their work), the model is the standard model.

First-order formulae that are true in every model are validities.

[loicd]

> I don’t think this is a standard definition.

Well, I suppose it depends on your definition of standard. That's how I have been taught logic. I also believe it is the historical notion. Honestly, "true but unprovable" sounds like a bad way to explain undecidability to me. Would you have been confused by "neither provable nor disprovable" instead? Also, this introduces a bias: the axiom of choice is neither provable nor disprovable in ZF. Are you going to say it is "true but unprovable" or "false but unprovable"?

> Every treatment I’ve seen refers to truth with respect to a model

That's called satisfiability.

> Outside of formal treatments (i.e. in the setting where the 99% of mathematicians who aren’t logicians do their work), the model is the standard model.

I simply cannot agree to that. What exactly is supposed to be the standard model of ZFC? For most mathematicians, what is true is what has been proved.

[Y_Y]

Can you give an example of a nontrivial statement that's true in every model?

[loicd]

If you don't have any axioms, the statements that are true in every model are exactly the tautologies (by definition). Usually though, one is interested in a particular set of axioms, typically ZFC. Then "every model" implicitely means "every model of ZFC", so "true" statements are the statements that are true in every model of ZFC, or equivalently by Gödel's completeness theorem, the statements that are provable from the axioms ZFC (and only ZFC). As for examples of such statements, well, that's virtually all mathematics. (The use of exotic axioms is quite specialized within mathematics.)