Let $T$ be a theory over $S$, prove that $T \vdash \{\phi \rightarrow \psi \} \iff (T \cup \phi) \vdash \psi$ Let $T$ be a theory over $S$, prove that $T \vdash \{\phi \rightarrow \psi \} \iff (T \cup \phi) \vdash \psi$.
So this seems very obvious intuitively. I'm just not sure what is the 'technique' to rigorously prove such propositions. Any assistance (hints) will be very appreciated!   
 A: Model Theory proof: 
$\Rightarrow$: Let's assume $T \cup \{\phi \} \not\vdash \psi$. So that means that if there is a structure $M$ so that $M \vDash  T \cup \{\phi \}$ then $M \not \vDash \psi \rightarrow M \vDash \lnot \psi$. 
But we know that $M \vDash T$, so we get that $M \vDash \{ \phi \rightarrow \psi \} \iff M \vDash \{ \lnot \phi \lor \psi \} \iff M \vDash \lnot \phi \lor M \vDash \psi$. But we got earlier that $M \vDash \lnot \psi$, and assume that $M \vDash \phi$. Contradiction.
Try to solve the other direction.   
A: $(T \cup \phi) \vdash \phi \to \psi$ by the monotonicity rule and obviously $(T \cup \phi) \vdash \phi$.  So by modus ponens, $(T \cup \phi) \vdash \psi$.  But if you are not allowed to use the modus ponens, only some kind of calculus, here is the proof with Gentzen-type calculus :
\begin{gather*}
(T \cup \phi \cup \neg\psi) \vdash \phi \wedge \neg\psi \text{ (obvious)}\\
T \vdash \phi \to \psi  = \neg(\phi \wedge \neg \psi)\text{ (by hypthesis)} \\
(T \cup \phi \cup \neg\psi) \vdash \neg(\phi \wedge \neg \psi)\text{ (monotonicity)}\\
(T \cup \phi \cup \neg\psi) \vdash \psi\text{ (an inconsistent theory entails anything)}\\
(T \cup \phi \cup \psi) \vdash \psi \text{ (obvious)} \\
(T \cup \phi) \vdash \psi\text{ (elimination of the term that doesn't affect the result)}
\end{gather*}
The strategy the other way round is similar, but longer.
