Mathematical Foundation of Computer Science

DHARM

PROPOSITIONAL LOGIC 131

For example, consider the formula X: (((P → Q) ∧ P) → Q)

Then tableaux of X will be,

(((P→∧→Q) P) Q) (β)

()β 1 Q ()β 2

~P

P

~Q

~ ((P→∧Q) P)

()β (^11) ~ ((P→Q) ()β 12
()α 111
()α 112
Consider the same formula with negation of it then X will be ~ (((P → Q) ∧ P) → Q). For
this formula we obtain different tableaux that is shown below.
Theorem 5.1. If T 1 is an “immediate extension” of T 2 then T 1 is true under all those interpreta-
tion for which T 2 is true.
Proof. Fig. 5.28 shows tableaux T 1 is the immediate extension of tableaux T 2. Assume that θ
and θ 1 are the paths of tableaux T 2. Also assume tableaux T 2 is true under interpretation ‘v’. It
follows that, there exist at least one true path in tableaux T 2 under ‘v’. Let this true path be θ.
Þ
q 1 q q
T 2
X X
T 1
Fig. 5.28
Now, extend the path of T 1 by assuming that it contains a β-formula or a α-formula.