# Notion of Truth and Axioms

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.

• 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

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.
• 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 supports Monica 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 supports Monica Aug 25 '11 at 10:46