0
$\begingroup$

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.

enter image description here

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?

$\endgroup$
3
  • $\begingroup$ It is simply the Weakenin rule: we can always add unnecessary premises. $\endgroup$ Commented Feb 19 at 6:46
  • 2
    $\begingroup$ 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. $\endgroup$ Commented Feb 19 at 7:32
  • $\begingroup$ See Weakening rule $\endgroup$ Commented Feb 19 at 7:33

1 Answer 1

2
$\begingroup$

"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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .