Semantic sequents

A semantic sequent takes one of the following forms:

(One can read this as saying that the set {j₁, j₂, …} semantically entails  y.)

(One can read this as saying that y is a semantic theorem, or a tautology.)

(One can read this as saying that the set {j₁, j₂, …} is semantically inconsistent.) 

A semantic sequent says, in effect, that there is no way of making all the formulae (if any) before the turnstile true and the formula (if any) after the turnstile false simultaneously. Let us be a little more precise. A structure in the propositional calculus is an assignment of truth-values to sentence letters. What a semantic sequent says is that there is no structure (which assigns truth-values to all the sentence letters in the sequent) which makes all the formulae (if any) before the turnstile true, and the formula (if any) after it false.

An easy (if sometimes laborious) way of checking for the correctness of semantic sequents is by using truth-tables. For instance we can check the correctness of

"[P«[QÙR]], [P®[¬Q®S]] |= [[QÙR]®S]" thus:

From this one can see that there is a structure in which "[P«[QÙR]]" and  "[P®[¬Q®S]]" are both true and "[[QÙR]®S]" is false. (Look at the second row of the truth-table.) So the sequent  is incorrect.

We can, of course, speak of the counterexample set of a semantic sequent, just as we do in the case of syntactic sequents. The counterexample set consists, as you would expect, of all the formulae before the turnstile (if any) together with the negation of the formula after the turnstile (if there is one). We can also speak of a counterexample to a semantic sequent. A counterexample is a structure (which assigns truth-values to all the sentence letters in the sequent) which makes all the formulae (if any) before the turnstile true, and the formula (if any) after it false. In other words a counterexample to a sequent is a structure which makes all the formulae in the counterexample set true.