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

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. — fdrake

Yes, the incompleteness theorem, when about PA in particular, is a meta-theorem about PA.

If PA is consistent, then:

PA |/- G

PA |/- ~G

PA |/- Con(PA)

But, if I'm not mistaken, there are certain statements that PA can prove about itself.

@Tarskian claims ('Inc' here for 'is incomplete'):

PA |- ~Con(PA) v Inc(PA)

equivalently:

PA |- Con(PA) -> Inc(PA)

equivalently:

PA + Con(PA) |- Inc(PA)

I tend to think that that is correct, though I'm not sure.

If at some point I have time enough, I'd like to refresh my knowledge to organize notes on what are some things PA does prove about itself.

It’s easy to dismiss the implications of formal systems by saying they don’t apply to language because it’s informal. Following that logic, one could argue that mathematics never perfectly applies to the real world, and therefore its implications shouldn’t be considered relevant to it.

What would be more interesting is to understand why such implications arise within a formal system in the first place. Once we understand that, we can assess whether it’s reasonable to assume those implications might also hold for language or nature.

Did Wittgenstein even attempt to figure out why?

What would be more interesting is to understand why such implications arise within a formal system in the first place. Once we understand that, we can assess whether it’s reasonable to assume those implications might also hold for language or nature.

Did Wittgenstein even attempt to figure out why — Skalidris

Yes he did. He would never argue that the implications of mathematics are “irrelevant to the real world”. Rather, the implications of formal systems can only be made sense of if we recognize that they are only intelligible within the language game , or ‘form of life’, that they belong to, and that they are of no help in explaining the transition between language games.

PA |- ~Con(PA) v Inc(PA)

equivalently:

PA |- Con(PA) -> Inc(PA)

equivalently:

PA + Con(PA) |- Inc(PA) — TonesInDeepFreeze

Followup to myself:

Yes, each of the above is correct.