Another example of why I don't like the word "truth" because I think it does more to muddy the situation than clarify it.
Let's drop "truth" for a sec.
Let's say I come up with a series of axioms about cows. They describe spots on cows, how many legs cows have, etc.
Now I come up with a sentence "all cows have spots." There are two ways of proving this sentence. One is a "semantic proof." That is I go and round up every cow and examine it and make sure they all have spots. Another way of proving this sentence is a "syntactic proof." I list out a series of axioms defining what cows are. Then I do a series of string manipulations on my axioms about cows according to an allowed ruleset to arrive at the statement "all cows have spots."
Semantic proofs are hard. They're annoying for finite groups of things and impossible to do for infinite groups of things. If possible we would like to use syntactic proofs. But syntactic proofs face two hurdles. The first is how to know we've applied our axioms correctly. For example, maybe one of my axiom is "all cows have 4 legs," and then I just conveniently define the symbol "4" to mean three. You can't really get around that problem. You kind of just have to tell people, don't mess around with the meaning of words.
The second hurdle though concerns our ruleset. That is string manipulations can be of an arbitrary form. How do I know, even if I've applied my axioms correctly, that my ruleset isn't crazy? Something like, anytime you see a sentence S, you're allowed to replace it with Not(S) if you want.
Godel's completeness theorem says for a lot of reasonable rulesets (including most of the ones we use for mathematics), semantic proofs and syntactic proofs coincide. You can decide to either go out and look at every cow or you can use your axioms about cows to move symbols on a sheet of paper around. As long as your axioms about cows capture enough information about whether cows have spots, with certain popular rulesets, you'll get the same result.
Put another way, as long as the result you're looking for is relevant to the axioms you've listed, either a semantic proof or a syntactic proof is valid.
Okay, but what about statements that aren't relevant to the axioms I've listed? Things like the weight of a cow? Or what about statements that are under-specified? For example if I just say as an axiom "some cows have spots," does that mean all cows have spots or that some don't?
Through the lens of Godel's completeness theorem this just means that our list of axioms is applicable to a lot more situations than we're giving it credit for. Our axioms don't talk about the weight of a cow? Well then they could be used for situations where cows are weightless or when they have weight. Our axioms don't specify whether all cows have spots? Well they can be used in situations where all cows have spots as well as situations where some cows don't have spots.
No biggie. That just means the only things relevant to our axioms are those properties in common across all the situations we could apply our axioms. And anything that can be semantically proved in all of these situations is also something that can be syntactically proved.
Okay so that concludes Godel's completeness theorem. Let's start going into his incompleteness theorems through the same lens.
Cows are really complicated things. They have tons and tons of different properties, so it's no surprise that our list of axioms will probably always under-specify them.
What if we strip things down to really really simple things. For example the natural numbers? Can we have a list of axioms that apply to the natural numbers and pin down every property about them?
The answer is no. Any list of axioms we come up with will always be "too broad." There are things other than the usual natural numbers (that's already a bit of a minefield to privilege one of them as being the "usual", but we'll ignore it for now) that I can present to you that also fulfill those axioms. In the same way that "some cows have spots" is mum on the issue of whether a certain cow doesn't have spots, and so can be used to describe either a herd of cows that all have spots or a herd of cows split half-and-half with spots and without spots, any system of logic that simultaneously fulfills both Godel's completeness theorem and incompleteness theorem means that it can be applied to more than one unique situation. Moreover those things that the system cannot syntactically prove are exactly those things that have different semantic proofs in different situations. For example, because I can't have a series of string manipulation steps that result in the sentence "all cows have spots" (Godel's incompleteness thereoms) there's gotta be some situations where all my axioms apply and all cows have spots and other situations where at least one cow doesn't have a spot (Godel's completeness theorem).
Hence through this lens Godel's incompleteness theorems aren't really about capital-T Truth so much as they are about our ability to completely specify infinite objects. If you and a friend decide to start listing out axioms to try to describe something like the natural numbers, no matter how many axioms you list out there is always something left unspecified.
"True" in this context is a technical definition, not some hand-waving thing. A sentence X being true means every model satisfies X. Provable means logical deduction within the theory proves X. So actually, Godel's theorems are exactly about truth and provability.
Yes if you appeal to model theory you're on firm ground with truth. But that's not how most informal introductions to the incompleteness theorems go (and indeed not how this article went about it).
More to the point, Godel's incompleteness theorems are theorems of proof theory, not model theory. Their proofs can be carried out with no recourse to models at all. And I think they are far less prone to being misunderstood when carried out without recourse to models and by extension without recourse to semantic truth.
You can of course choose to interpret them in model theory if you're working in a semantically complete logical system such as first-order logic with the usual semantics or second-order logic under Henkin semantics, and it is often illuminating to do so once you have those fundamentals. But I think in an informal setting those will tend only to confuse rather than clarify. And importantly the incompleteness theorems still hold in contexts where you don't really have a meaningful model theory to speak of.
Let's drop "truth" for a sec.
Let's say I come up with a series of axioms about cows. They describe spots on cows, how many legs cows have, etc.
Now I come up with a sentence "all cows have spots." There are two ways of proving this sentence. One is a "semantic proof." That is I go and round up every cow and examine it and make sure they all have spots. Another way of proving this sentence is a "syntactic proof." I list out a series of axioms defining what cows are. Then I do a series of string manipulations on my axioms about cows according to an allowed ruleset to arrive at the statement "all cows have spots."
Semantic proofs are hard. They're annoying for finite groups of things and impossible to do for infinite groups of things. If possible we would like to use syntactic proofs. But syntactic proofs face two hurdles. The first is how to know we've applied our axioms correctly. For example, maybe one of my axiom is "all cows have 4 legs," and then I just conveniently define the symbol "4" to mean three. You can't really get around that problem. You kind of just have to tell people, don't mess around with the meaning of words.
The second hurdle though concerns our ruleset. That is string manipulations can be of an arbitrary form. How do I know, even if I've applied my axioms correctly, that my ruleset isn't crazy? Something like, anytime you see a sentence S, you're allowed to replace it with Not(S) if you want.
Godel's completeness theorem says for a lot of reasonable rulesets (including most of the ones we use for mathematics), semantic proofs and syntactic proofs coincide. You can decide to either go out and look at every cow or you can use your axioms about cows to move symbols on a sheet of paper around. As long as your axioms about cows capture enough information about whether cows have spots, with certain popular rulesets, you'll get the same result.
Put another way, as long as the result you're looking for is relevant to the axioms you've listed, either a semantic proof or a syntactic proof is valid.
Okay, but what about statements that aren't relevant to the axioms I've listed? Things like the weight of a cow? Or what about statements that are under-specified? For example if I just say as an axiom "some cows have spots," does that mean all cows have spots or that some don't?
Through the lens of Godel's completeness theorem this just means that our list of axioms is applicable to a lot more situations than we're giving it credit for. Our axioms don't talk about the weight of a cow? Well then they could be used for situations where cows are weightless or when they have weight. Our axioms don't specify whether all cows have spots? Well they can be used in situations where all cows have spots as well as situations where some cows don't have spots.
No biggie. That just means the only things relevant to our axioms are those properties in common across all the situations we could apply our axioms. And anything that can be semantically proved in all of these situations is also something that can be syntactically proved.
Okay so that concludes Godel's completeness theorem. Let's start going into his incompleteness theorems through the same lens.
Cows are really complicated things. They have tons and tons of different properties, so it's no surprise that our list of axioms will probably always under-specify them.
What if we strip things down to really really simple things. For example the natural numbers? Can we have a list of axioms that apply to the natural numbers and pin down every property about them?
The answer is no. Any list of axioms we come up with will always be "too broad." There are things other than the usual natural numbers (that's already a bit of a minefield to privilege one of them as being the "usual", but we'll ignore it for now) that I can present to you that also fulfill those axioms. In the same way that "some cows have spots" is mum on the issue of whether a certain cow doesn't have spots, and so can be used to describe either a herd of cows that all have spots or a herd of cows split half-and-half with spots and without spots, any system of logic that simultaneously fulfills both Godel's completeness theorem and incompleteness theorem means that it can be applied to more than one unique situation. Moreover those things that the system cannot syntactically prove are exactly those things that have different semantic proofs in different situations. For example, because I can't have a series of string manipulation steps that result in the sentence "all cows have spots" (Godel's incompleteness thereoms) there's gotta be some situations where all my axioms apply and all cows have spots and other situations where at least one cow doesn't have a spot (Godel's completeness theorem).
Hence through this lens Godel's incompleteness theorems aren't really about capital-T Truth so much as they are about our ability to completely specify infinite objects. If you and a friend decide to start listing out axioms to try to describe something like the natural numbers, no matter how many axioms you list out there is always something left unspecified.