Gödel's first incompleteness theorem from halting problem using soundness. Is it possible to use semantic consistency?

Question

Here is my proof of a variation of Gödel's first incompleteness theorem (Theorem 1). It uses soundness as one of the hypothesis. I would like to know if it would be possible to prove Theorem 2.

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.

Here is how I would prove it. Consider the following program, godel.py:

import is_theorem_in_S
import halt_to_S

def godel(input):
    godel_program = read('godel.py')
    halts_in_S = halt_to_S(godel_program)
    not_halts_in_S = 'NOT ' + halts_in_S

    if is_proof_in_S(not_halts_in_S) == 'yes':
        return 'halts'
    else:
        # loop
        while True:
            pass

We import two functions:

• is_theorem_in_S checks if the given formula is a theorem in $S$ (that is, if it is provable). This function will stop if the formula is provable, and loop if it is not. This is due to the fact that $S$ is recursively axiomatizable, a).
• halt_to_S turns, or a given input program $P$, the statement "$P$ halts with empty input" into a formula in $S$. This is possible because of c).

halts_in_S stores the formula equivalent to "godel.py halts on empty input", and:

not_halts_in_S stores the formula equivalent to "godel.py does NOT halt on empty input" (1)

If not_halts_in_S is a theorem, the function is_proof_in_S(not_halts_in_S) will return 'yes' and the problem will halt. If not, the program will enter an infinite loop.

The question is, what happens to godel.py when input is empty ('')?

If we assume godel.py stops on empty input, the only way to do so is because it returned 'halts', and this can only happen if is_proof_in_S(not_halts_in_S) == 'yes', hence it can only happen if not_halts_in_S is a theorem. Because of the soundness of $S$ (b), not_halts_in_S would be true.

But if not_halts_in_S is true, then, using (1), that would mean godel.py does not stop on empty input, which gives a contradiction.

We now know that:

godel.py does not halt on empty input (2)

Let's check that not_halts_in_S is true but is not a theorem. It is true because of (2). However, not_halts_in_S is not a theorem. For that, we use (2) again. The fact that godel.py does not halt means that it is not possible that is_proof_in_S(not_halts_in_S) == 'yes', in other words, not_halts_in_S is not a theorem.

We have found a statement in $S$ that is true but is not a theorem. This means that $S$ is semantically incomplete.

---

Would it be possible to tweak this proof so that we can prove Theorem 2?

Theorem 2 (First Incompleteness Theorem, semantic consistency version). Let $S$ be a formal system such that:

a) $S$ is recursively axiomatizable (that is, its axioms are recursively enumerable).

b) $S$ is semantically consistent (that is, it is not possible that, given a formula $\phi$, both $\phi$ and $\neg\phi$ are 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.