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
 

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[QR]], [P[QS]] |- [[QR]S]

(One can read this as saying that the set {[P[QR]], [P[QS]]} syntactically entails [[QR]S].)

 

 

(ii) |- y

 

e.g. |- [PP]

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

 

 

(iii) j1, j2, |-

 

e.g. [PQ] |-

 

(one can read this as saying that [PQ] 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[QR]], [P[QS]] |- [[QR]S]" says that the set {[P[QR]], [P[QS]], [[QR]S]} generates a tableau which closes. It does, as we discovered earlier. So the sequent is correct.

 

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

 

     [PP]

     P

     P

 

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

 

     [PQ]

     P

     Q

 

This tableau is now finished, and has not closed.

 

 

Print this page Print this page
BackNext