Let $T$ be a theory over $S$, prove that $T \vdash \{\phi \rightarrow \psi \} \iff (T \cup \phi) \vdash \psi$

Question

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!

Answer 1

$(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.

Answer 2

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.