I'm reading through Ebbinghaus' Mathematical Logic and more specifically chapter 4 where a sequent calculus is constructed. Below is the rule I need clarification on because, according to my definitely-wrong understanding, it leads to a contradiction.
Here, $\Gamma$ is just a sequent of formulas. At first, this rule was intuitive to me until I encountered in a justification in the next section where $\Gamma'$ was $\Gamma$ with $\neg \phi$. According to this rule, that is valid. In fact, the book has a definition on the notion of correctness:
A sequent $\Gamma \phi$ is correct if $\Gamma \models \phi$, or $\{\psi \mid \psi \text{ is a member of } \Gamma\} \models \phi$.
Rule 2.1 is supposed to yield a correct formula, but $\Gamma' \phi$ is not correct because there exists no interpretation $\mathfrak J$ such that $\mathfrak J \models \phi$ and $\mathfrak J \models \neg\phi$. How can this be? What am I missing here?
"Consistent" and "Correct" are not synonyms.
A correct sequent may have inconsistent premises.
$\phi,\lnot\phi\vdash\phi$ is correct, by definition, because $\phi\models\phi$ and $\phi$ is a member of $\{\phi,\lnot\phi\}$.
$\phi,\lnot\phi\vdash\lnot\phi$ is also correct, because $\lnot\phi\models\lnot\phi$ and $\lnot\phi$ is a member of $\{\phi,\lnot\phi\}$.
The fact that no interpretation will satisfy $\{\phi,\lnot\phi\}$ has no standing.