MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top


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.

share|cite|improve this question
Perhaps it makes sense to a philosopher, but for me, the question is a collection of random words. Voted to close. – Mark Sapir Aug 21 '11 at 9:45
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. – SNd Aug 25 '11 at 0:30
up vote 14 down vote accepted

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.

share|cite|improve this answer
Thanks for your answer, Carl. – user12806 Aug 21 '11 at 18:51
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). – Emil Jeřábek Aug 23 '11 at 11:49
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). ... – Emil Jeřábek Aug 25 '11 at 10:46
... 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”. – Emil Jeřábek Aug 25 '11 at 10:55
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.) – Emil Jeřábek Aug 25 '11 at 12:13

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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