Sequents

As 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.