Hello,
The proofs in logic often use the notion of truth.
Is it possible to prove Gödel's first incompleteness theorem without the notion of truth and without the notion of stop for a program ?
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.