What is truth in the completeness theorem?

[Demystifier]

According the the Godel's completeness theorem, a statement in first order logic is true if and only if it can be formally proved from the first order axioms. But what does it mean that a statement is true? Obviously, it cannot be by definition that true means provable in first order logic, because then the theorem would be trivial. So how is truth in this context defined? How do we know that something is true without referring to the completeness theorem? Clearly, to know that something is true, we must prove it. But in this context we are not allowed to prove it with first order logic, so what kind of logic is used to prove the truth? Is it some informal logic that cannot be formalized? Does this logic have a name?

 

[andrewkirk]

But what does it mean that a statement is true?

In the wiki version it says 'logically valid' rather than 'true'. But whatever it's called, it means that every structure or model that is a semantic interpretation of the theory satisfies the statement.

Consider the field axioms. These are satisfied by any field. Different structures/models that satisfy them are the reals, the rationals, the complex numbers, the integers modulo p for any prime p, and a myriad of other fields based on surds that we encounter in Galois theory. Those models differ in more ways than just the labels. There are some things that are true for only some of those models. For instance the reals and rationals are totally ordered, but the complex numbers and integers modulo p are not. The truth of those things are proved not by the field axioms but by the axioms of the relevant model (eg we can construct a stand-alone axiomatisation of the complex numbers), which will entail the field axioms but will generate more true statements than the field axioms alone can generate.

What the Godel completeness theorem tells us is that, out of all that additional structure, if there is any statement that is true for ALL fields, then it must be provable by the field axioms alone - even if all the proofs we know use specific properties of the field in question (one proof for the reals, a completely different, non-analogous proof for integers modulo p, etc). Godel tells us there must be a proof that does not rely on use model-specific axioms.

Conversely, if there is no proof of statement S in theory T then there must be at least one model M that satisfies theory T, in which S is not true.

I hope that makes sense. It's a bit meta.

 

[Demystifier]

if there is any statement that is true for ALL fields, then it must be provable by the field axioms alone

OK, but my question is this. How can we know that a statement is true for all fields, if not by proving it from axioms? We can check case by case that the statement is true in this model and that model, but we cannot check all models (since there is an infinite number of them). Do we prove the truth by some informal meta logic that cannot be formalized?

Or is the definition of truth nonconstructive, i.e. the definition does not allow us to explicitly determine that something is true (except by the use of the completeness theorem)?

 

[Demystifier]

Related to this, what kind of logic is used to prove the completeness theorem? Since it is a theorem about first order logic, the proof itself cannot be a proof within first order logic, am I right? So is it some informal meta logic that cannot be formalized?

 

[andrewkirk]

How can we know that a statement is true for all fields

I suspect the only way we can know is if we can prove it in the theory T. But it is conceivable that there could be case-specific proofs for all possible structures, even though we could never find them all. What Godel tells us is that that can't be the case unless there is also a non-case-specific proof.

Since it is a theorem about first order logic, the proof itself cannot be a proof within first order logic, am I right?

It can be in first-order logic. All that's needed is that the language M in which Godel's proof is done is richer than the language L that it's talking about, meaning that M can refer to everything that L can refer to, and can also refer to all the symbols of L as constants of M. This needs to be meta-ised one step further since L is general not specific, but than can be done with set theory, which can be axiomatised in first-order logic.

 

[rubi]

Provability is a purely syntactic concept, while truth is concerned with models of theories within set theory (usually ZFC + possibly some large cardinal axioms). A sentence $\phi$ about a model $\mathcal M$ of a theory $\Gamma$ is said to be true, iff the sentence $\mathcal M \models \phi$ is provable within set theory. It's called Tarski truth semantics. If for all models $\mathcal M$, we have $\mathcal M\models\phi$, then we say that $\phi$ is valid ($\Gamma\models\phi$). This is also a sentence that can be formalized within set theory and can thus be proved within set theory. Now Gödels completeness theorem says that $\Gamma\models\phi$ implies $\Gamma\vdash\phi$, i.e. $\phi$ is provable from $\Gamma$.

 

[Demystifier]

Now Gödels completeness theorem says that $\Gamma\models\phi$ implies $\Gamma\vdash\phi$, i.e. $\phi$ is provable from $\Gamma$.

A related question is this. What is the difference between "implies" (symbol $\rightarrow$) and "is provable" (symbol $\vdash$)? In general, what is the difference between $A\rightarrow B$ and $A\vdash B$ ? More specifically, could we write the statement above as
$$(\Gamma\models\phi)\vdash(\Gamma\vdash\phi)?$$
If not, why not?

 

[rubi]

$\rightarrow$ is a logical connective in propositional logic, just like $\land$ or $\lor$. $\vdash$ is a symbol in the metalanguage. However, there is a connection between them given by the deduction theorem. It says that $\{A\}\vdash B$ implies $\vdash A\rightarrow B$, i.e. if $B$ can be proved from $A$, then the sentence $A\rightarrow B$ can be proved without using any axioms.

The sentence $(\Gamma\models\phi)\vdash(\Gamma\vdash\phi)$ is a bit odd, because $\vdash$ shouldn't appear as part of a sentence ($\Gamma\vdash\phi$ in this case), since it is not supposed to be a symbol in the object language. One could however formalize the sentence $\Gamma\vdash\phi$ in set theory, but then $\vdash$ would take two different meanings, depending on where it is used. The sentence would then read $(\Gamma\models\phi)\vdash(\Gamma\vdash_\text{formalized}\phi)$, but of course we could omit the "formalized" index, since we can tell the difference from the context.

Edit: The strictly formal statement of Gödel's completeness theorem would be:
$$ZFC\vdash (\Gamma\models\phi)\rightarrow(\Gamma\vdash_\text{formalized}\phi)$$