Can the set of true formulas be deduced from the set of provable formulas? EDIT 01/19/2011 20:30 : judging from the two answers I got, my original question was not completely understood, so I'll try to reformulate a special case.
Imagine that you meet a supermathematician from another planet, that can do a lot of things we earthlings cannot do. In particular, he can compute effectively in his head a "completion" of ZFC, meaning a (very big) list of axioms (extending the ZFC axioms) that never contradict each other and allow one to find a yes/no answer to every question about set theory. The supermathematician is also able to find the answer in less than a second for every question.
Now you play the following game with the supermathematician. He invents some completion (call it $T$) of ZFC in his head, and your goal is to discover for yourself if the continuum hypothesis holds in $T$ or not. Of course, you may not ask him directly "Does CH hold, according to $T$?" That would be too easy. You may only ask questions of the form : "According to $T$, does ZFC prove that sentence $\phi$ ?" but you may ask as many questions
of this form as you please, and for any $\phi$ you please.
Is there a winning strategy ?
 Note that it is useless to ask, "According to $T,$ does ZFC prove CH" ? We already know that the answer is no, and this will be of no help in determining if CH holds in $T$ or not.
////////////////////////////////////////////////////////////////////
OLDER VERSION, 01/19/2011
By Goedel's incompleteness theorems, both the truth or the provability of a formula of set theory is non-computable in general. Now assume that we have a "magic machine" which can decide the provability of any sentence $\phi$ (from $ZFC$, say). So that machine tells us about the truth of the formulas of the form $ZFC \vdash \phi$. With the help of this machine,
can we determine the truth of all formulas $\phi$ ?
A more formal version of this question : assume that ZFC is consistent, and let $\Phi$ denote the set of all sentences of set theory, let ${\Phi}' \subset \Phi$ denote the set of sentences of the form $ZFC \vdash \phi$ for some sentence $\phi$. 
  Let $\cal F$ denote the set of all functions ${\Phi} \to {\lbrace {\sf true,false} \rbrace}$ corresponding to complete (=maximally consistent) extensions of $ZFC$. For $f\in {\cal F}$, denote by $r(f) : {\Phi}' \to {\lbrace {\sf true,false} \rbrace}$ the restriction of $f$ to ${\Phi}' $. So $r$ is a map  ${\cal F} \to {}^{{\Phi}'} \lbrace {\sf true,false} \rbrace$. Let us denote by ${\cal F}'$ the image of $r$. Then, the questions are :


*

*Is $r$ injective ? In other words, is there a "left inverse" $s : {\cal F}' \to {\cal F} $ such that
$s \circ r=id_{\cal F}$.

*If $s$ exists, is it "computable" ? (this is a vague question since $r$ and $s$ are defined on very large, non-computable sets. Basically it asks if the proof of existence of $s$ (if there is one) is "explicit" or not).
 A: The answer to your modified question is no, we cannot get at $T$ just by asking about what $T$ thinks ZFC proves, since perhaps $T$ includes the assertion $\neg\text{Con}(\text{ZFC})$, in which case the theory $T$ believes that ZFC proves every statement. So it will always answer yes to the queries. By the incompleteness theorem, if ZFC is consistent then it is also perfectly consistent with ZFC to hold $\neg\text{Con}(\text{ZFC})$, and thus we cannot distinguish by your method between the case where the supermathematician has a theory extending $\text{CH} +\neg\text{Con}(\text{ZFC})$ or whether his theory extends $\neg\text{CH}+\neg\text{Con}(\text{ZFC})$, since all the answers will be the same for any completions of these two theories. 
Addendum. Let me now answer without any trickery with the incompleteness theorem. The point is that set-theoretic truth is not determined by mere arithmetic truth. You've told us that our super-mathematician's theory $T$ is consistent, so it holds in some model $M$. Consider now a forcing extension of $M$ arising by the usual forcing to change the value of CH, and let $T_0$ be the new theory of the forcing extension $M[G]$. The theory $T_0$ is computable from $T$, since a statement is in $T_0$ if and only if the assertion that that statement has Boolean value $1$ for the corresponding forcing is in $T$ (this uses that the forcing is homogeneous, and so all such forcing extensions give rise to the same theory). The point now is that the theory $T$ and $T_0$ have exactly the same arithmetic truths, since arithmetic is not affected by forcing. Thus, those two theories give exactly the same answers to the questions about what ZFC proves or about what any theory of $M$ proves, since those questions are arithmetic questions (about the existence of certain finite combinatorial objects, proofs). But they differ as to CH, and so one cannot tell whether $T$ has CH or not just by asking such questions. 
Conclusion. What this argument shows is that for any theory $T$ that the supermathematician has in mind, there is another theory $T_0$ with a different answer to CH, but with all the same answers to the queries in your game. 
A: You cannot compute truth from provability with respect to a computably axiomatizable theory.
One way to see this directly is that the set of (Gödel codes of) theorems of a fixed computably-axiomatizable theory has complexity $\Sigma^0_1$ in the arithemtic hierarchy. In other words, it is computable from the halting problem, and for sufficiently strong theories, the set of codes for theorems is actually Turing equivalent as an oracle to the halting problem. 
Meanwhile, the set of true statements of arithmetic has a strictly higher complexity, exceeding $\Sigma^0_n$ for any $n$. For example, with an oracle for the theorems, we still cannot compute the truth of $\Sigma^0_3$ statements in general.
Nevertheless, it is possible to compute truth from provability with respect to some non-computable theories. For example, if we have an oracle for the collection of true statements, then we may (trivially) compute the set of true statements from it.
