I'd like to ask for your help in showing me the (quite likely: several) flaws in my argument below, relating weak and strong representability in a formal system and the halting problem.
At least part of the problem is most likely that I am too informal in my definitions, leading to wrong conclusions. That said, I still can't point out exactly where my argument goes wrong. Hopefully, someone is patient enough to overlook the lack of rigor in those steps where the argument is correct in principle, and helps me understand the major mistakes of it.
(1) The halting set $HALT$, containing all pairs of numbers $(i, j)$ s.t. the Turing program (enumerated by) $i$ halts (i.e. produces an output) after finite steps on input $j$, is computably enumerable, while its complement set (of program/input pairs that do not halt) is not computably enumerable.
(2) Assuming a first-order formal system $F$ as expressive as Peano arithmetic (PA) is strong enough to reason about computable relations, we can (can we?) define a formula $H$ in $F$ that weakly represents the set $HALT$, i.e. $(i,j) \in HALT \iff \vdash H(i, j)$.
For a (sloppy) definition of $H$: $\forall x,y \: \exists z.H(x, y) \iff CompStateSequence(z, x, y)$, where $CompStateSequence(z, x, y)$ holds if $z$ encodes a finite sequence of program states for a program/input pair $(x, y)$ s.t. each state in the sequence correctly follows from the previous state according to the rules of the program, the first state is the beginning state of $(i,j)$, and and the final state is the output state of a program.
$(\rightarrow)$ If $(i,j) \in HALT$, there must be a finite sequence of computation steps computing $(i,j)$, so there must be a finite sequence of states representing a successful computation of $(i, j)$. Then we can find a proof for $H(x, y)$ in $F$, $\vdash H(i, j)$, by mechanically testing all numbers up to $z$ whether they are the desired sequence of program states.
$(\leftarrow)$ Assume $(i,j) \notin HALT$. Then there is no (finite) sequence of program states s.t. the sequence computes $(i,j)$. Assume $\vdash H(i,j)$. Then by definition of $H$, there must be a number $z$ representing a finite sequence of program states representing a computation of $(i,j)$. Contradiction, so we know $H$ (weakly) represents the set $HALT$ in $F$.
(3) Further, we can use $H$ to define (in the weaker sense of truth, not provability) set $HALT$ in $F$, i.e. $(i, j) \in HALT \iff$ $H(i, j)$ is true in the intended model of F, by a similar argument as in (2) above, with 'truth' in the place of 'provability'.
(4) (Now, for the part where I probably really just confuse myself...) Assume $(i,j) \notin HALT$. By definition of $H$ (and the argument in (3) above) we know that $H(i,j)$ is false in the intended model of $F$.
But if $H(i,j)$ is false in one model of $F$, it must be false in every model of $F$, since $(i,j)$ will not halt in any (correct) model of a theory representing Turing computability.
Then $\neg H(i,j)$ is true in every model of $F$, so $\neg H(i,j)$ is valid, so by (semantic) completeness of $F$, there is a proof of $\neg H(i,j)$ in $F$. But then $\not H$ is weakly representable as well, so together with weak representability of $H$, $HALT$ is strongly representable in $F$, which (by equivalence of strong representability and decidability) contradicts the result that the halting problem is undecidable.