Tutorial Contents Tutorial Five: Predicate Calculus: Tableaux - The \$xj rule - Bad Mistakes and Technical Mistakes - Ticking - Finished Tableaux - Sequents - Soundness and Completeness - Proof of a syntactic sequent: example More Tutorials One Two Three Four Six Seven

## 1.

In the case of each of the following sequents, say whether it is correct, and, if it is incorrect, give a counterexample.
(i) ["xFxÙ"xGx] |= "x[FxÙGx]
(ii) "x[FxÙGx]  |= ["xFxÙ"xGx]
(iii) ["xFxÚ"xGx] |= "x[FxÚGx]
(iv) "x[FxÚGx] |= ["xFxÚ"xGx]
(v) [\$xFxÙ\$xGx] |= \$x[FxÙGx]
(vi) [\$xFxÚ\$xGx] |= \$x[FxÚGx]
(vii) "xFxx |= \$xFxx
(viii) "xFxa |= \$xFxa
(ix) "x[Fx®Gx] |= \$x[FxÙGx]
(x) "x[Fxa®Gxa] |= \$x[FxaÙGxa]
(xi) \$xFx, "x[Fx®Gx], "x[Fx®¬Gx] |=
(xii) \$xFx, "x\$y[FyÙRxy] |= \$y"x[FyÙRxy]
(xiii) \$xFx, "x\$y[FxÙGy] |= \$y"x[FxÙGy]
(xiv) \$xFx, ["xFx®P] |= "x[Fx®P]
(xv) \$xFx, ["xFx®P] |= \$x[Fx®P]
(xvi) [\$xFx®P] |= "x[Fx®P]
(xvii) "x[P®Fx] |= [P®"xFx]

## 2.

Show that the following sequents are incorrect by finding counterexamples.
(i) ["xFx®\$xGx] |= "x[Fx®Gx]
(ii) "x[Fx®\$yGyx] |= [\$xFx®\$x"yGxy]
(iii) "x[[Fx®Gx]Ú[¬Fx®Hx]] |= "x[GxÚHx]
(iv) "x"y\$zFxyz, \$x"yFxyx |= "x"y\$zFyzx
(v) \$x"y[FxyÙFyx], "x[Gx®"y[Fyx«Gy]] |= "xGx
(vi) \$x\$yRxy, "x"y"z[[RxyÙRyz]®Rzx], "x"y"z[[RxyÙRxz]®Ryz] |= "xRxx
(vii)

"x[Fx®"y[Gy®Rxy]], "x[HxÚ¬\$y[FyÙRxy]], "x"y[Rxy®Ryx]

|= \$x[Fx®"y[Gy®Hy]]

(viii)

"x"y[Fxy®¬"z[Gz®Hzy]], "x"y\$z[¬Hzx®Fyx]

|= "x"y[Fxy«\$z[GzÙ¬Hzy]]