Incompleteness is not a theorem of PA, unless PA is inconsistent. — TonesInDeepFreeze

Gödel's incompleteness theorem proves that PA is inconsistent or incomplete. That is a perfectly legitimate theorem in PA. It does not prove that PA is incomplete. That is a theorem in PA + Cons(PA).

The use of logical entailment predates model theory by decades — Tarskian

By millennia. But those concepts are not formal.

T ⊨S as a synonym for "S is true in T". — Tarskian

You are so confused.

T |= S stands for "T entails S" not "S is true in T".

We know that 'true' and 'provable' are different notions.

A sentence is provable or not in a theory.

A sentence is true or not in a model.

A sentence is neither true nor false in a theory

A sentence is neither provable nor unprovable in a model.

The concept of 'provable' pertains to theories.

The concept of 'true' pertains to models.

The linkage is the soundness and completeness theorems:

soundness: If a sentence S is provable from a set of sentences G, then S is entailed by G.
That is, if G |- S then G |= S

completeness: If a sentence S is entailed by set of sentences G, then S is provable from G.
That is, if G |= S then G |- S

I think some people do say "S is true in T", but when we unpack it, it is a loose way of saying, "If all the sentences in T are true, then S is true." But what does 'true' mean? In mathematical logic, a sentence is true or not per a model. So "S is true in T" is a loose way of saying "Every model in which the sentences in T are all true is a model in which S is true", which is just to say T |= S, with the completeness theorem T |- S, which is just to say that S is in T (with the definition of 'theory' as a set of sentences closed under provability).

Here are usages:

G is a set of sentences (which could be a theory or not), M is a model, S is a sentence:

G |- S ... G proves S

G |= S ... G entails S ... in mathematical logic, that is: Every model of G is a model of S

|=_M S ... S is true in M

M |= S ... (not "M entails S" as it would appear, which would make no sense, since a model doesn't entail, but rather |=_M S)

I did not say that your remark would be wrong — Tarskian

Here's what you wrote:

it is not possible to preclude the second disjunct. — Tarskian

the Gödelian statements that cannot be expressed by language. There are uncountably many of those. — Tarskian

In a given countable language, there are only countably many sentences.

But there are uncountably many languages and systems, so it's trivial that there are uncountably many true but unprovable sentences.

But there are uncountably many languages and systems, so it's trivial that there are uncountably many true and provable sentences across the class of all languages.

Gödel's incompleteness theorem proves that PA is inconsistent or incomplete. — Tarskian

Of course, that is just sentential logic from:

If PA is consistent then PA is incomplete.

That is a perfectly legitimate theorem in PA. — Tarskian

I'm not sure about that; I'd have to think about it.

It does not prove that PA is incomplete. — Tarskian

Correct.

That is a theorem in PA + Cons(PA). — Tarskian

If Con(PA) then PA is incomplete. That is: If PA is consistent then PA is incomplete.

hat is a perfectly legitimate theorem in PA. — Tarskian

I'm not sure about that; I'd have to think about it. — TonesInDeepFreeze

I don't think it's a theorem in PA, it's a theorem about PA. PA + some additional axiom could make cons(PA) a theorem, but that wouldn't be a theorem in raw PA.

I don't think it's a theorem in PA, it's a theorem about PA. — fdrake

It is an existence theorem about a sentence that is supposed to exist in PA.

The canonical witness is definitely a sentence in the language of PA:

G ⇔ ¬ Bew(⌜G⌝)

meaning:

"This is not provable."

Of course, the fact that this sentence exists in the language of PA says something about PA