|
||||||||||||||||||||||||||||||||
Syntactic sequentsA 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
(One can read this as saying that [PÚ¬P] is a syntactic theorem.)
(iii) j1, j2, … |-
(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.
|
||||||||||||||||||||||||||||||||
|