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.



Notion of Truth and Axioms
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. 


