Comment by rssoconnor | Hacker News Reader

Comment by rssoconnor | Hacker News Reader

Parent Full thread

There are true (in the sense of Tarski's definition of truth) but unprovable (Π₁) sentences in any consistent (sufficiently powerful) system. Which of these true sentences are unprovable varies from system to system.

Π₁-sentences (see arithmetical hierarchy) are closed formulas of the form, ∀x:ℕ. P(x), where P is some decidable predicate. i.e. all quantifiers in P are bounded. Thus for any given fixed value for x, say n, P(n) can be expanded out into conjunctions and disjunctions of atomic equalities and inequalities between closed arithmetic formula and those (in)equalities can in turn be decided (in principle) by calculation. Notice that 'x' is a formal variable in the language of first order logic, while we are using 'n' as a meta-variable denoting a term representing a numeral, e.g. 42.

Σ₁-sentences are closed formulas of the form, ∃x:ℕ. P(x), where P is again a decidable predicate.

Some basic first order logic yields that the negation of a Σ₁-sentence is logically equivalent to a Π₁-sentences and similarly the negation of a Π₁-sentence is logically equivalent to a Σ₁-sentence.

Important Fact: All true Σ₁-sentences are provable (in any sufficiently powerful system). Why? Suppose ∃x. P(x) is true. Then, there is some numeral 'n' where P(n) is true. Since P(n) is decidable we can prove P(n) when P(n) is true. And, by the rule of existential introduction, ∃x.P(x) is provable from P(n).

Now, let us consider some consistent system T (which is "sufficiently powerful"). For example, we can take T to be ZFC if you think ZFC is consistent. We can construct a Goedel-Rosser sentence for T, let's call this sentence G. G is a Π₁-sentence by construction, so we can put G in the form of ∀x:ℕ. P(x) for some decidable predicate P.

Now either G is true, (i.e. ∀x:ℕ. P(x) is true) or ¬G is true, (i.e. ∃x:ℕ. ¬P(x) is true). Suppose ¬G is true. Since ¬G is (equivalent to) a Σ₁-sentence then T proves ¬G. But by the Goedel-Rosser incompleteness theorem, this would imply that T is inconsistent, contradicting our assumption.

Thus it must be the case that G is true. However G is unprovable in T because, again by the Goedel-Rosser incompleteness theorem, if G were provable in T, then T would be inconsistent, contradicting our assumption.

Thus G is an example of a true sentence that isn't provable in T.

So, what do you think about my answer to the same parent? In particular, how is your answer compatible with the fact that ZFC is complete, because it is a first-order theory?

For sake of argument we will be presuming below that ZFC is consistent.

While it is true that ZFC is model-complete in your sense (which holds for all first-order theories as you note), ZFC has many non-standard models that come with with non-standard sets of natural numbers within them. There are Σ₁-sentences that are false in models with standard sets of natural numbers but are true in models with non-standard sets of numbers.

Tarski's definition of truth, which I'm using for the definition of (in)completeness in my comment, excludes non-standard models because it requires, for example, for a Σ₁-sentence ∃x. P(x) to be considered true, that there actually exist a numeral (e.g. a closed term such as 42), 'n' where P(n) is true (recalling P is a decidable predicate the truth or falsity of P(n) can be determined (in principle) by calculation). When a Σ₁-sentence is only true in models with non-standard natural numbers, such numerals that witness P do not exist.

Some people argue that non-standard natural numbers are just as good as standard natural numbers, and you can try that argument I suppose. However, if I'm hiring someone do formal analysis of some algorithm and they "prove" that it is terminating by showing it terminates in some non-standard number of iterations, then I'm just going to fire them because such a result isn't helpful for reasoning about programs.

There is a material difference between standard and non-standard natural numbers. The standard natural numbers are formed in a natural way from the terms that make up the formal language of the first-order logic under consideration (i.e. the terms that are numerals), but the non-standard natural numbers cannot since they include "numbers" that have no associated numeral. Also note this way of characterizing the standard natural numbers won't work for characterizing "standard sets", because we do not expect all sets to come with canonical concrete terms denoting them, like we do expect for natural numbers.

Very helpful answer, thank you! I suspected that it has something to do with "Tarski's definition of truth", but there seem to be different ideas around about what this means. While Wikipedia agrees with yours, I can point to at least one popular book ("An Introduction to Mathematical Logic" by Richard E. Hodel) that equates Tarski truth just with model theoretic truth.

I wouldn't fire the analyst in your example, by the way, because the fault would be mine: I should have just specified what complexity bound would be acceptable in a termination proof of the algorithm for it to be practical for my purposes.

I guess Tarski's definition of truth is relative to some interpretation, but the usual unqualified version of his definition is implicitly relative to the standard model of natural numbers. (Edit: or maybe it is me who is using the notion of Tarski's definition of truth incorrectly.)

> I wouldn't fire the analyst in your example, by the way, because the fault would be mine: I should have just specified what complexity bound would be acceptable in a termination proof of the algorithm for it to be practical for my purposes.

I thought someone might say something like this. My counter is that if the analyst just used a normal proof system (i.e. one that doesn't assume false (in the standard model) axioms) then we could use Goedel's Dialectica [1] to mine the proof for some (probably crappy) complexity bound. That said, this is getting close to the edge of my knowledge on this subject.

[1] http://math.stanford.edu/~feferman/papers/dialectica.pdf

The halting problem provides examples of true but unprovable

propositions because there are some expressions that do not

halt but it is unprovable that they do not halt.

Reply on news.ycombinator.com