Sequent


   

Let W be a set.  A sequent of W is a tuple <P,t> where P ⊆ W and t ∈ W.  The elements in P are the premises of the sequent and t is its consequent.

The sequent <P,t> is written as
 
P ⊢ t

If the set of premises is empty then the sequent is written as either...
 

⊢ t

or simply as
 

t

There is no difference, other than appearance, due to the manner in which a sequent is presented.


[ Overview | Next ]