Is it possible to construct an algorithm that can formally prove any statement in some countable first-order theory except for exactly those which aren't provable in the theory? Why or why not?
Edit: so, apparently, the answer is affirmative. Has such an algorithm already been constructed?
Edit 2: I meant countable theories.
On
Provided your language is countable, then the answer is yes, though this answer has little to do with automated theorem proving. Let $T$ be a theory in a countable language $L$. Then the set of sentences in $L$ is countable, so the set of finite sequences of sentences in $L$ is countable. Hence the set of proofs of $T$-provable sentences is countable.
So you can list the set of all proofs of $T$-provable sentences as $$\{ p_n : n < \omega \}$$ An algorithm which, given a $T$-provable sentence $\varphi$, returns a proof of $\varphi$, works as follows. Input a $T$-provable sentence $\varphi$. Set $n=0$. While $\varphi$ remains unproved, check if $p_n$ is a proof of $\varphi$; if so, then return $p_n$; else increment $n$.
But this is emphatically not what automated theorem provers do, or attempt to do.
An algorithm can enumerate all consequences of the axioms, and so eventually list all the provable statements and all the disprovable statements.
An algorithm can take any non-independent statement and (if it really is not independent) determine if the statement, or its negation, has a proof.
An algorithm cannot tell, given an arbitrary statement, whether it is provable, or disprovable, or independent.