# Clarification for a rule in this sequent calculus

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?

• It is simply the Weakenin rule: we can always add unnecessary premises. Commented Feb 19 at 6:46
• Re your puzzling: assume that $\Gamma \varphi$ is correct. This means that, in every interpretation where... $\varphi$ must be true. But this means also that there is no int where all of $\Gamma$ and $\lnot \varphi$ is true. Thus, if we add the "contradictory" premise $\lnot \varphi$ to the original set $\Gamma$ of premises, what we get is an inconsistent set of premises, i.e. a set $\Gamma'$ that is never true. Thus, the new sequent $\Gamma' \varphi$ still holds. Commented Feb 19 at 7:32
• Commented Feb 19 at 7:33

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