1
$\begingroup$

Hello,

The proofs in logic often use the notion of truth.

Can we ignore the notion of truth, if we add axioms to the Peano's axioms ?

Is it possible to prove Gödel's first incompleteness theorem without the notion of truth ?

The proof of the Gödel's first incompleteness theorem, that I know is: Gödel numbers by $n$ the statements $E_n(i)$ with one argument $i$. "$E_i(i)$ is not provable" is a statement $A(i)$. There is an $n$ such that $A$ is $E_n$. The proof of the theorem says: if $A(n)$ is not $\mathit{true}$, $E_n(n)$ is provable. So $A(n)$ is provable, and $A(n)$ is $\mathit{true}$, contradiction. So $A(n)$ is $\mathit{true}$, and not provable.

If $n$ is the Gödel's number of a statement $Q_n$ (without argument), and if $P(n)$ is the statement saying that $Q_n$ is provable in the formal system of Peano's axioms, we add, for every $n$, the axiom: "$P(n) \implies Q_n$".

So the step "$A(n)$ is provable, implies $A(n)$" in the previous proof, is an axiom.

So we don't use the notion of truth. Do you have references about this subject ?

Thanks in advance.

Improve this question
$\endgroup$
2
  • 3
    $\begingroup$ Perhaps it makes sense to a philosopher, but for me, the question is a collection of random words. Voted to close. $\endgroup$
    – user6976
    Commented Aug 21, 2011 at 9:45
  • 1
    $\begingroup$ The question is quite reasonable but it should be made CW because the existence of purely syntactic proof of first incompleteness theorem is very well known. $\endgroup$
    – SNd
    Commented Aug 25, 2011 at 0:30

1 Answer 1

Reset to default
14
$\begingroup$

The proof of the incompleteness theorem can already be done syntactically, ignoring truth, if we remove the conclusion that the Gödel sentence is true and leave only that it is neither provable nor disprovable. In particular, the "usual" proof of the incompleteness theorem is syntactic once we move to Rosser's version. For Gödel's version, there is an extra hypothesis of $\omega$-consistency, which is directly about truth in the metatheory: $\omega$-consistency corresponds to the reflection scheme $\operatorname{Pvbl}_T((\exists x)\psi) \to (\exists x)\psi$ where $\psi$ is quantifier-free. The explicit use of this assumption was elided in the question, but it become more obvious if we write the formalized provability predicate $\operatorname{Pvbl}_T$ instead of "is provable".

If we start asking what axioms are used in the metatheory, we need to move to a formal metatheory. One good reference for this and everything in the question is Smorynski's article in the Handbook of Mathematical Logic. He covers in detail the question of what metatheory is sufficient. The short version is that for an effectively axiomatized theory $T$ that meets the hypotheses of the incompleteness theorems (with Rosser's trick), PRA will prove $\operatorname{Con}(T) \to \operatorname{Con}(T + \lnot \operatorname{Con}(T))$. There is no notion of "truth" in the language of PRA to begin with, and this proof is just syntactic.

In general, axiom schemes in the metatheory containing sentences of the form $\operatorname{Pvbl}_T(\phi) \to \phi$ are called "reflection" schemes in the context of arithmetic. They have been studied in detail, and Smorynski spends several pages on them in his article. Another reference, which I have been meaning to read but haven't had the chance yet, is Axiomatic Theories of Truth by Halbach. I think Halbach's book should be very related to the topics in this question.

Improve this answer
$\endgroup$
5
  • $\begingroup$ PRA is an overkill. A weak fragment of bounded arithmetic (such as PV or $S^1_2$) is enough, provided $T$ is presented with a polynomial-time set of axioms (which is not a significant restriction, by Craig’s trick). $\endgroup$
    – Emil Jeřábek
    Commented Aug 23, 2011 at 11:49
  • $\begingroup$ Thanks, Emil. What are bounded arithmetic and PV ? $\endgroup$
    – user12806
    Commented Aug 24, 2011 at 17:50
  • 1
    $\begingroup$ Bounded arithmetic is a generic name for fragments of arithmetic that only have induction for (a subset of) bounded formulas (i.e., only with quantifiers $\exists x\le t\,\phi(x)$, $\forall x\le t\,\phi(x)$) in the original arithmetical language or its slight extensions (meaning basically that there should not be any function in the language with exponential growth). The prototypical example is $I\Delta_0$, though it turns out more useful to study theories in an expanded language that allows to prove all polynomial-time computable functions total (Buss’s theories). ... $\endgroup$
    – Emil Jeřábek
    Commented Aug 25, 2011 at 10:46
  • 1
    $\begingroup$ ... PV (originally introduced by Cook as an equational theory) has a language containing function symbols for all polynomial-time functions, and it is axiomatized by basic defining equations for these functions plus induction for open formulas in its language. You can find more on bounded arithmetic in Chapter V of Hájek & Pudlák “Metamathematics of first-order arithmetic”, Buss’s PhD thesis (available on his home page), Krajíček’s “Bounded arithmetic, propositional logic, and complexity theory”, or Cook & Nguyen “Logical foundations of complexity theory”. $\endgroup$
    – Emil Jeřábek
    Commented Aug 25, 2011 at 10:55
  • 1
    $\begingroup$ Maybe I should also mention that bounded arithmetic is interpretable (on a cut) in Robinson’s Q, so it has as low a proof theoretic strength as it can get. (This is in fact the main reason why Gödel’s second incompleteness theorem applies already to Q and its extensions.) $\endgroup$
    – Emil Jeřábek
    Commented Aug 25, 2011 at 12:13

Not the answer you're looking for? Browse other questions tagged or ask your own question.