Yes it will? This works for any first-order theory with a recursive set of axioms. You are simply searching for proofs of implications from the axioms and using the halting oracle to tell if the search terminates or not. By the compactness theorem this is guaranteed to work.
Of course you have to input the axioms, how would a theorem prover work otherwise?
> By the compactness theorem this is guaranteed to work.
I think you mean completeness, but essentially yes.
In this case I meant compactness - if a statement follows from your (possibly infinite set of) axioms then it follows from a finite subset of them. But you can skin the cat in many ways, yeah (proof theory vs model theory way of looking at it I guess).