ABSTRACT
As the rules o f MK were completely symmetrical w ith respect to formulas on the the left and on the right, also the role o f P - and Q -sign ed formulas in classical tableaux will be symmetrical. Com posite signed formulas are classified as
unramified ramified
Q v Aw : Q v Q w P vAw : P v P w P W w : P v P w Q W w : Q v Qw P v ^ w : Q v P w Q v->w : P v Q w Q ~>v : P v P -»v : Q v
A classical tableau again consists of a finite 2 -a ry tree T , a root piece R of T , and two functions t and e such that
t assigns signed formulas to the nodes of T ,
£ assigns nodes to those nodes e of T which sim ultaneously (a) are non maxim al in T and (b) should they belong to R are (the one) maximal (node in) R .
