Non-formal provability

A simplified version of Goedel’s first incompleteness theorem (it’s really just a special case of Tarski’s indefinability of truth) goes like this:

• Given a sound semidecidable system of proof that is sufficiently rich for arithmetic, there is a true sentence g that is not provable.

Here:

• sound: if s is provable, s is true

• semidecidable: there is an algorithm that given any provable sentence verifies in a finite number of steps that it is provable.

The idea is that we start with a precisely defined ‘formal’ notion of proof that yields semidecidability of provably, and show that this concept of proof is incomplete—there are truths that can’t be proved.

But I am thinking there is another way of thinking about this stuff. Suppose that instead of working with a precisely defined concept of proof, we have something more like a non-formal or intuitive notion of proof, which itself is governed by some plausible axioms—if you can prove this, you can prove that, etc. That’s kind of how intuitionists think, but we don’t need to be intuitionists to find this approach attractive.

Note that I am not explicitly distinguishing axioms.

The idea is going to be this. The predicate P is not formally defined, but it still satisfies some formal constraints or axioms. These can be formulated in a formal language (Brouwer wouldn’t like this) that has a way of talking about strings of symbols and their concatenation and allows one to define a quotation function that given a string of symbols returns a string of symbols that refers to the first string.

One way to do this is to have a symbol ′α′ for any symbol α in the original language which refers to α, and a concatenation operator +, so one can then quote αβγ as ′α′ + ′β′ + ′γ′. I assume the language is rich enough to define a quotation function Q such that Q(x) is the quotation of a string x.

To formulate my axioms, I will employ some sloppy quotation mark shorthand, partly to compensate for the difficulty of dealing with corner quotes on the web. Thus, ′αβγ′ is shorthand for ′α′ + ′β′ + ′γ′, and as needed I will allow substitution inside the quotation marks. If there are nested quotation marks, the inner substitutions are resolved first.

1. For all sentences ϕ and ψ, if P(′ϕ↔︎∼ψ′) and P(′ϕ′), then P(′∼ϕ′).

2. For all sentences ϕ and ψ, if P(′ϕ↔︎∼ψ′) and P(′ψ→ϕ′), then P(′ϕ′).

3. For all sentences ϕ, we have P(′P(′ϕ′)→ϕ′).

4. If ϕ has a formal intuitionistic proof from sufficiently rich axioms of concatenation theory, then P(′ϕ′).

Here, (1) and (2) embody a little bit of facts about proof, both of which facts are intuitionistically and classically acceptable. Assumption (3) is the philosophically heaviest one, but it follows from its being axiom that if ϕ is provable, then ϕ, together with the fact that all axioms count as provable. That a formal intuitionistic proof is sufficient for provability is uncontroversial.

Using similar methods to those used to prove Goedel’s first incompleteness theorem, I think we should now be able to construct a sentence g and the prove, in a formal intuitionistic proof in a sufficiently rich concatenation theory, that:

5. g ↔︎  ∼ P(′g′).

But these facts imply a contradiction. Since 5 can be proved in our formal way, we have:

6. P(′g↔︎∼P(′g′)′). By 4.

7. P(′P(′g′)→g′). By 3.

8. P(′g′). By 6, 7 and 2.

9. P(′∼g′). By 6, 8 and 1.

Hence the system P is inconsistent in the sense that it makes both g and  ∼ g are provable.

This seems to me to be quite a paradox. I gave four very plausible assumptions about a provability property, and got the unacceptable conclusion that the provability property allows contradictions to be proved.

I expect the problem lies with 3: it lets one ‘cross levels’.

The lesson, I think, is that just as truth is itself something where we have to be very careful with the meta- and object-language distinction, the same is true of proof if we have something other than a formal notion.