I am learning about Gödel's incompleteness theorems, and I want to prove them using the undecidability of the halting problem. So far, here is the result I have been able to prove:
Theorem 1 (First Incompleteness Theorem, soundness version). Let $S$ be a formal system such that:
a) $S$ is recursively axiomatizable (that is, its axioms are recursively enumerable).
b) $S$ is sound (that is, every theorem --or provable formula-- is true).
c) $S$ can express certain statements about Turing machines, specifically, it can encode, given a Turing machine $M$, that "$M$ halts on empty input".
Then, $S$ is semantically incomplete, that is, there are true formulas in $S$ that are not provable.
Note: I give a proof of this theorem here.
This version is different than Gödel's:
Theorem 2 (Gödel's First Incompleteness Theorem). Let $S$ be a formal system such that:
a) $S$ is recursively axiomatizable (in the same sense as theorem 1).
b) $S$ is syntactically consistent (it is not possible that both $\phi$ and $\neg\phi$ are provable).
c) $S$ contains a certain amount of elementary arithmetic.
Then, $S$ is syntactically incomplete, that is, there are formulas $\phi$ in $S$ such that $\phi$ nor $\neg\phi$ are provable.
For one, Gödel's version is entirely syntactical, while the one from the halting problem is semantic. My question is, is there any semantic result like the following?
Theorem 3 (Second Incompleteness Theorem, soundness version). Let $S$ be a formal system such that:
a) $S$ is recursively axiomatizable.
b) $S$ can express certain statements about Turing machines, specifically, it can encode, given a Turing machine $M$, that "$M$ halts on empty input".
Then, $S$ cannot prove its own soundness (that is, every provable formula is true).
It would be like a dual version of Theorem 1, in the sense that Theorem 4 is a dual version of Theorem 2.
Theorem 4 (Gödel's Second Incompleteness Theorem). Let $S$ be a formal system such that:
a) $S$ is recursively axiomatizable.
b) $S$ contains a certain amount of elementary arithmetic.
Then, $S$ cannot prove its own syntactic consistency (it is not possible that both $\phi$ and $\neg\phi$ are provable).
Edit: I asked this question about soundness, but given that soundness implies consistency (in a way that I do not know), I would also like to ask if it is possible to prove that:
Theorem 5 (Second Incompleteness Theorem, semantic consistency version). Let $S$ be a formal system such that:
a) $S$ is recursively axiomatizable.
b) $S$ can express certain statements about Turing machines, specifically, it can encode, given a Turing machine $M$, that "$M$ halts on empty input".
Then, $S$ cannot prove its own semantic consistency (that is, given a formula $\phi$, it is not possible that both $\phi$ and $\neg\phi$ are true).