

SequentsAs with the propositional calculus, so with the predicate calculus we may have both syntactic and semantic sequents.
For instance $xFx, "x[Fx®Gx]  $xFx means {$xFx, "x[Fx®Gx], ¬$xFx} generates a tableau which closes. And $xFx, "x[Fx®Gx] = $xFx means (informally) There is no interpretation which makes "$xFx" and ""x[Fx®Gx]" both true and "$xFx" false in any domain.


