The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 22 Jun 2021, Pierre-Marie Pédrot wrote:

> I personally really hate the phrasing of Gödel's incompleteness theorem
> as "there are unprovable true statements" because it's implicitly
> referring to the meta and confusing the reader about some grand and
> transcendental notion of "truth" when this does not exist. Except maybe
> when you're a Girard fan and / or some neo-Popperian believer, in which
> case you may claim that Π01 formulae are falsifiable in the only
> standard model we have, a.k.a. our local universe, and thus there is
> some well-behaved notion of truth for these (but not above).

I don't know if this is a Girardian argument, but the case for these 
Goedel sentences being true seems pretty solid to me and follows directly 
from the fact that any system with "sufficent arithmetic" (e.g Robinson 
Arithmetic or Hodel's NN, etc) is Sigma_1-complete.

Why are they Sigma_1-complete?  Because if some Sigma_1 formula, ∃x:N. 
P(x) is "true" then (at least according to Tarski's definition of truth) 
there is some natural number n such that P(n) is true.  If there really is 
such a natural number n, then there is some literal term (what I'd call a 
numeral), that denotes this number n, that can be written as 
1+1+1+1+...+1+0, or (...(b0*(1+1) + b1)*(1+1) + ...) + bn for some list of 
binary digits 0 or 1, or however else you want to write terms that denote 
natural numbers.  If we let t be any one of these terms that denotes n 
then P(t) is a "true" Delta_0 statement, and "true" Delta_0 statements are 
also all provable.  Since all the quantifers are bounded, then they can 
all be logically eliminated by expanding them out as conjunctions or 
disjunctions until you get an logically equivalent expresison P'(t) that 
is quantifier free.  All the atomic formulas within this quantifer free 
expression are equalities or inequalites between closed terms that denote 
natural numbers, and it is just a matter of computation to compare each of 
pair of terms to determine whether each one is equivalent to T (true) or F 
(false), in which case P'(t) is logically equivalent to some P'', which is 
proposition in terms of pure boolean logic.  Again it is a simple Boolean 
computation to simplifiy this expression to another logically equivalent 
proposition P''' which is either T or F.  And since our starting 
hypothesis was that P(t) was "true" and we have shown that it is logically 
equivalent to P''', then it must be the case that P''' is T and not F.

All of the above deductions can be formally carried out in any of these 
logics with "sufficent arithemetic" to deduce that P(t) <-> T, and hence 
deduce P(t) in such a system.  Then existential introduction lets us prove 
in such a system the statement ∃x:N. P(x).

The contrapositive version of Sigma_1-completness is that if your proof 
system does not prove some Sigma_1 statement S, then S cannot be "true". 
One might even go as far as saying that such a statement S is "false", 
because if it isn't "true", then what else could it be?

In the case of a Goedel sentence G, it is a Pi_1 sentence, and hence it's 
negation ¬G is Sigma_1.  If ¬G cannot be deduced in such a proof system, 
then it must be the case that ¬G is "false" and hence ¬¬G is "true". Even 
a constructivist would concede that ¬¬G implies G for a Pi_1 statement G.
Thus the Goedel sentence G is true when ¬G is not provable.

Of course, this conclusion only applies under the condition that ¬G is not 
provable.  You may very well be working in a system where ¬G is provable, 
and above reasoning doesn't apply.  We cannot even conclude that ¬G is 
true because that assumes your system is Sigma_1-sound, but we've only 
shown Sigma_1-completeness.  In fact, if ¬G is provable then the system in 
question definitely is not Sigma_1-sound because, as a consequnce of the 
construction of ¬G, the sytem is inconsistent and proves everything 
(requires Rosser's consturction of G IIRC).

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''