Tutorial Contents Tutorial Three: Propositional Calculus: Tableaux - The Sentence Tableaux Rules - Testing Arguments for Validity - Sequents - Syntactic Sequents - Semantic Sequents - Soundness and Completeness - Correctness of Sequents and Validity of Arguments More Tutorials One Two Four Five Six Seven

### Syntactic sequents

A syntactic sequent takes one of the following forms:

##### (i) j1, j2, … |- y  (where j1, j2, …, and y are formulae)

e.g. [P«[QÙR]], [P®[¬QÚS]] |- [[QÙR]®S]

(One can read this as saying that  the set {[P«[QÙR]], [P®[¬QÚS]]} syntactically entails  [[QÙR]®S].)

##### (ii) |- y

e.g. |- [PÚ¬P]

(One can read this as saying that [PÚ¬P] is a syntactic theorem.)

##### (iii) j1, j2, … |-

e.g. ¬[P®Q] |-

(one can read this as saying that ¬[P®Q] is syntactically inconsistent.)

##### The "|-" is the syntactic turnstile.

The counterexample set of a syntactic sequent is the set consisting of all the formulae before the turnstile (if any) together with the negation of the formula after the turnstile (if there is one).

What a sequent says is that its counterexample set generates a tableau which closes.

So,  "[P«[QÙR]], [P®[¬QÚS]] |- [[QÙR]®S]" says that the set {[P«[QÙR]], [P®[¬QÚS]], ¬[[QÙR]®S]} generates a tableau which closes. It does, as we discovered earlier. So the sequent is correct.

"|-[PÚ¬P]" says that {¬[PÚ¬P]} generates a closed tableau. It does.

ü¬[PÚ¬P]

¬P

¬¬P

"¬[P®Q] |-" says that {¬[P®Q] } generates a closed tableau. It doesn't; so the sequent is incorrect.

ü¬[P®Q]

P

¬Q

This tableau is now finished, and has not closed.