[thorel]

This idea of giving "meaning" to a set of axioms is precisely captured by the notion of "interpretation" in logic [1]. The rough idea is to map the symbols of the formal language to some pre-existing objects. As you say, this gives one way of formalizing truth: a sentence (string of symbols that respect the syntax of your language) is true if it holds for the objects the sentence is referring to (via a chosen interpretation). This notion of truth is sometimes referred to as semantic truth.

An alternative approach is purely syntactic and sees a logical system as collection of valid transformation rules that can be applied to the axioms. In this view, a sentence is true if it can be obtained from the axioms by applying a sequence of valid transformation rules. This purely syntactic notion of truth is known as “provability”.

Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide.

[1] https://en.wikipedia.org/wiki/Interpretation_(logic)

[Tainnor]

> Then the key question is to ask whether the two notions coincide: one way to state Godel's first incompleteness theorem is that it shows the two notions do not coincide

It's even more subtle than that. They do coincide in a sense, which is proven by Gödel's completeness theorem (well, at least in First-Order Logic). That one just says that a sentence is provable from some axioms exactly iff it's true in every interpretation that satisfy the axioms.

So one thing that Gödel's first incompleteness theorem shows it's that it's impossible to uniquely characterise even a simple structure such as the natural numbers by some "reasonable"[0] axioms - precisely because there will always be sentences that are correct in some interpretations but not in others.

Unless you use second-order logic - in which case the whole enterprise breaks down for different reasons (because completeness doesn't hold for second order logic).

[0] reasonable basically means that it must be possible to verify whether a sentence is an axiom or not, otherwise you could just say that "every true sentence is an axiom"

[thorel]

Agreed, thanks for the clarifications. Another result worth mentioning, which also shows that you cannot hope to uniquely characterize a structure by "reasonable" axioms is the Löwenheim–Skolem theorem which predates Godel's incompleteness (although the history of these results is somewhat convoluted).

There, the obstacle is in some sense of a simplest nature: if your set of axioms admits a countable model, then it admits models of all infinite cardinalities. In other words, it shows that there is something fundamentally impossible in trying to capture an infinite structure (like numbers) by finite means (e.g. recursively axiomatizable).

[ginnungagap]

> In other words, it shows that there is something fundamentally impossible in trying to capture an infinite structure (like numbers) by finite means (e.g. recursively axiomatizable).

Let me just point out for other readers that Löwenheim-Skolem applies to ANY first order theory (in a countable language, or also in an uncountable language if stated in the form that a theory with an infinite model with cardinality at least that of the language has infinite models in all cardinalities at least as big as that of the language), it doesn't care about how complex the axioms are from a computability point of view

[Tainnor]

You're correct, but I think the spirit of what GP wrote is still true.

You can't capture an infinite structure fully by "finitary" methods, either you use FOL and then you run into L-S, or you use higher-order logic (for which L-S doesn't apply) but then you don't have a complete proof system anymore.

To tie it all together, L-S and incompleteness are about different flavours of "not being able to capture something". L-S is about models of different cardinalities. These models do still all satisfy exactly the same sentences. Incompleteness is about different models actually satisfying different sentences.

[Tainnor]

Löwenheim-Skolem is such a mind-blowing result. It's a shame it's not talked about more often.