Using an inference in an inference The problem
If $\Sigma$ is a set of premises, the Suppes system of inference has the following property (aka deduction theorem) for all propositional formulae $\alpha$ and $\beta$:
$$\tag{1}\label{eq:prop}
\Sigma\cup\{\alpha\} \vdash_S \beta
\quad\Leftrightarrow\quad
\Sigma\vdash_S\alpha\to\beta
$$
What inference rules are relevant to determining the correctness of property \eqref{eq:prop}?
Inferences within inferences?
The Suppes system consists of the usual Modus Ponens, elimination and introduction rules, and conditional and indirect proofs, and I know how to write proofs using Fitch notation. Or I would if it wasn't for that pesky $\vdash_S$, that occurs twice in the claim.
In order to determine what inference rules rules might be required to prove \eqref{eq:prop}, I would need to write up a proof of it, but how do I incorporate the symbol $\vdash_S$ into a Fitch table? I believe another way of writing the left and right sides of the equivalence in \eqref{eq:prop} are
$$\tag{2}\label{eq:infers}
  \frac{ \Sigma\lor\alpha }{ \beta }
  \quad\text{and}\quad
    \frac{ \Sigma }{ \alpha\to\beta }\,.
$$
My question then is, what exactly are my premises in proving ''$\Rightarrow$'' and ''$\Leftarrow$'' in \eqref{eq:prop}? The entire inferences in \eqref{eq:infers}? The one on the right looks like a conditional proof
$$\tag{CP}\label{eq:CP}
\frac{\substack{[\alpha]\\\vdots\\\beta}}{\alpha\to\beta},
$$
but what is the one one the left? Disjunctive elimination
$$\tag{DE}\label{eq:DE}
\frac{ \alpha\lor\alpha }{ \alpha }\,?
$$
Edit
I have been given a hint that the relevant inference rules are in the set
$$\tag{IP}\label{eq:IP}
\frac{ \lnot\beta\to\lnot\alpha\land\alpha }{ \beta }\,,
$$
\eqref{eq:CP} above, Modus Ponens
$$\tag{MP}\label{eq:MP}
\frac{\alpha\to\beta\qquad\alpha}{\beta}
$$
and Disjunctive Syllogism
$$\tag{DS}\label{eq:DS}
\frac{ \alpha\lor\beta\qquad\alpha\to\phi\qquad\beta\to\varphi }{ \phi\lor\varphi }\,.
$$
 A: Given a set of formulas $\Sigma$ and a formula $\beta$, the notation $\Sigma \vdash_S \beta$ (which is not a formula) means that there is a derivation in the Suppes system whose assumptions are in $\Sigma$ and whose conclusion is $\beta$.
The symbol $\vdash_S$ is not part of the object language (it is not a connective) and hence it should not be incorporated in a Fitch table. It is a meta-symbol to express the concept of derivability.
Let us see how to prove the equivalence $(1)$ in your post.
($\Rightarrow$) In the left-to-right proof of the equivalence $(1)$, your hypothesis is that there is a derivation $\pi$ in the Suppes system whose assumptions are in $\Sigma \cup \{\alpha\}$ and whose conclusion is $\beta$; using that hypothesis, you have to show that there exists a derivation $\pi'$ in the Suppes system whose assumptions are in $\Sigma$ and whose conclusion  is $\alpha \to \beta$.
Concretely, take $\pi$ (it exists by hypothesis) and apply the rule for conditional proof (CP) to it, which discharges the assumption $\alpha$. Thus, you get a derivation $\pi'$ whose assumption are in $\Sigma$ and whose conclusion is $\alpha \to \beta$, as required.
($\Leftarrow$) Conversely, in the right-to-left proof of the equivalence $(1)$, your hypothesis is that there is a derivation $\pi'$ in the Suppes system whose assumptions are in $\Sigma$ and whose conclusion  is $\alpha \to \beta$; using that hypothesis, you have to show that there exists a derivation $\pi$ in the Suppes system whose assumptions are in $\Sigma \cup \{\alpha\}$ and whose conclusion is $\beta$.
Concretely, take $\pi'$ (it exists by hypothesis) and observe that $\pi'$ is a derivation whose assumptions are in $\Sigma \cup \{\alpha\}$ and whose conclusion is $\alpha \to \beta$ (indeed, you can freely add assumptions that you do not use in your derivation). 
Since $\alpha$ is an assumption, you can apply modus ponens (MP) to $\alpha$ and $\alpha \to \beta$ to get $\beta$. Therefore, the derivation $\pi$ obtained from $\pi'$ by adding at the end (MP) applied to $\alpha$ and $\alpha \to \beta$ has the assumptions in $\Sigma \cup \{\alpha\}$ and the conclusion $\beta$, as required. 
Therefore, the inference rules that are relevant to prove the equivalence $(1)$ are (CP) for the direction $\Rightarrow$, and (MP) for the direction $\Leftarrow$.

Note that your notations on $(2)$ are essentially meaningless for two reasons:


*

*$\Sigma$ can be a set of infinite formulas, and usually in logic inference rules deal with a finite number of premises.

*$\Sigma \cup \{\alpha\}$ in a premise intuitively means that your assumptions are in $\Sigma \cup \{\alpha\}$, so your premises are all the formulas in $\Sigma$ and (not or) $\alpha$.
