Sequents
There are
two types of sequent: syntactic sequents and semantic sequents.
Syntactic sequents
are defined (in our case) in terms of tableaux. Semantic sequents are defined
in terms of truth. The idea behind calling sequents of the
first sort "syntactic" is that the tableau rules depend for their
application solely on the syntax of the formulae involved; they do not depend
on any meaning that the formulae may have. In particular they do not depend
on the definition of the truth-functors in terms of truth and falsity. (Though,
of course, they were actually chosen with these definitions in mind.) By
contrast the definition of semantic sequents does depend on the meaning
of the truth-functors.
|
