Just a simple question about Godel incompleteness: suppose you have a certain statement $p$ that can't be proved in a formal system $S$ but it can be proved in another ("superior"?) system $S'$.In that case what is the relation between $S$ and $S'$? I mean, does $S'$ contain all the axioms and theorems of $S$ plus extra ones or not necessarily?
1
-
$\begingroup$ Not necessarily; but in some sense, it must be "stronger". See Gentzen's consistency proof. $\endgroup$ – Mauro ALLEGRANZA Feb 24 '17 at 10:50
5
$\begingroup$
$\endgroup$
Not necessarily.
For example, $\sf PA$ cannot prove $\operatorname{Con}\sf (PA)$. But Gentzen proved that $\sf PRA$ augmented by induction up to $\varepsilon_0$ can in fact prove $\operatorname{Con}(PA)$.
However, $\sf PRA$ is a weak fragment of $\sf PA$, and the induction axioms add nothing to "correct of the missing part".
Other, sillier examples, include $\sf ZFC$ which cannot prove $\operatorname{Con}\sf(ZFC)$, but $\sf PA+\operatorname{Con}(ZFC)$ clearly proves $\operatorname{Con}\sf (ZFC)$.
1
$\begingroup$
$\endgroup$
As an even sillier example, take the language of arithmetic and extend it with a new binary operator $\circledast$. Then let $S$ be the theory consisting of all PA axioms plus $0\circledast 0=0$. Apply the Gödel procedure to this and get a true sentence $G$ that $S$ does not prove.
On the other hand if we let $S'$ be the PA axioms plus $G$ itself, then that certainly does prove $G$ -- but $S'$ will not prove $0\circledast 0=0$, because we can make a model of $S'$ where $0\circledast 0=0$ is false by taking the ordinary natural numbers with the ordinary addition and multiplication, and then interpret $\circledast$ as the function that always returns $1$. (Here it is important that Gödel's construction always results in an arithmetical sentence, so we know there are no $\circledast$s in $G$).
All this is assuming the only thing you know about $S'$ is that it is something that can prove your Gödel sentence.
It seems somewhat more likely that you have read a description where $S'$ is not just any system with this property, but where you specifically construct $S'$ by taking $S$ and adding the Gödel sentence as a new axiom. In that particular case, it is of course true that $S'$ proves all of the theorems and axioms of $S$ -- simply because every $S$-proof is still a valid $S'$-proof.
