You misunderstand soundness and completeness of logic. You think that it says:
A statement is true if, and only if, it is provable.
But it really says:
A statement is true in every model if, and only if, it is provable.
It can happen that there is a model in which a statement is true but not provable. What if you live in such a model? Then it could happen that in the model in which you live there is a total function $f$, but there is no proof that $f$ is total.
Here is a precise mathematical reason why your thinking does not work. I am going to show that, whatever formal system you are using (so long as it is a reasonable one), there is a total function which your formal system does not prove to be total.
You do proofs in some formal system $T$ (for instance, $T$ could be first-order logic and Zermelo-Fraenkel set theory) whose axioms are computably enumerable (or else you're a mystic guru). Let us also assume that $T$ contains arithmetic, and that $T$ is consistent (or else you're mad).
Define the following function
if n encodes a proof of 0 = 1 in formal system T:
while True: pass
f is total if, and only if, $T$ is consistent:
- if $T$ is consistent then it does not prove $0 = 1$, hence
f never enters the infinite
f is total, then it never enters the infinite
while loop, therefore no $n$ encodes a proof of $0 = 1$ in $T$, therefore there is no proof of $0 = 1$ in $T$, which means that $T$ is consistent.
Because $T$ is consistent,
f is total.
But $T$ does not prove that
f is total: if it did, then it would prove that, for every $n$, $n$ does not encode a proof of $0 = 1$, but this would imply that $T$ proves its own consistency, which it cannot by Gödel's incompleteness theorem.