Mathematical Foundation of Computer Science

DHARM

132 MATHEMATICAL FOUNDATION OF COMPUTER SCIENCE

These possibilities are shown below in Fig. 5.29.

Or,

α

θ θ

β

α 1

α (^2) T β 1 β 2
T 1 1
XX
Fig. 5.29
Thus if v(α) = true;
then (v(α 1 ) = true ) ∧ ( v(α 2 ) = true );
else if v(β) = true;
then ( v(ß 1 ) = true ) ∨ ( v(β 2 ) = true );
Hence, T 1 is true.
That concludes the result.
Theorem 5.2. If formula at the root of the tableaux is true then tableaux is true.
Proof. The statement pronounced by the theorem is an implicative type.
i.e., if ( ...............) then ( ...............);
that is, if ( formula at the root of the tableaux is true) then (tableaux is true) under ‘v’;
The statement is equivalently to its symbolic view,
if (P) then (Q); where antecedent part is P and consequent is Q
⇒ P → Q
⇔ ~ Q → ~ P (using transportation rule)
⇒ if (~Q) then ( ~ P);
⇒ if ( tableaux is not true) then (formula at root is not true) under ‘v’;
Since, a tableaux is not true, only when there is no true path in the tableaux; It follows
that tableaux is closed.
We already know that a formula which is false under all possible interpretations is
called as ‘contradiction’. Therefore we say that,
if ( X is a ‘contradiction’) then (~ X will be tautology);
⇔ if ( X is a tautology) then ( ~ X is a contradiction);
So, if tableaux is closed then formula at the root is a contradiction.
Example 5.26. Show

1. A → B


2. A /∴ B
   Sol. From the given argument we can determine the formula say X,
   where, X : ((A → B) ∧ A) → B)
   Put negation of X so we have, ~ (((A → B) ∧ A) → B)