ABSTRACT
The method of tableaux, developed for propositional logic in Chapters 1.5 , 4.6 and 5.6 , extends to quantifier logic in a straightforward manner. W or king again w ith signed formulas, the table of components becomes:
unramified ramified
Q vAw Q v Q w P vAw P v P w P vVw P v P w Q W w Q v Q w P v-Hv Q v P w Q v-nv P v Q w Q w P V P “ >V Q v P a Q V x V Q s u b ( x , t | v ) P V x V : P s u b ( x , y P 3 x v P s u b ( x , t |v ) Q 3 x v : Q s u b ( x , y
such that quantified formulas now are assigned arbitrarily many components, namely one for every term t or for every variable y resp ective ly ; in the case of classical logic the component P a is again om itted.
