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




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


            {$xFx, "x[Fx®Gx], ¬$xFx} generates a tableau which closes.


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


Print this page Print this page