### B.5.1 Propositional Consequences

The conclusion

~~**forall** `x`: **exists** `y`: `p`(`x`,
`y`) |

**forall** `x`: **exists** `y`: `p`(`x`,
`y`) |

holds independently of the interpretation of `p` and
consequently independently of the truth value of
(**forall** `x`: **exists** `y`: `p`(`x`, `y`)).
This is because this conclusion is an instance of the pattern

which is true independently of the truth value of `G`. We call such a
conclusion a *propositional consequence (aussagenlogische Folge)*.

**Proposition 153 (Propositional Consequences)**
The following conclusions are propositional consequences for every formula
`A` and `B`:
**Negation**-
**And Introduction and Or Elimination**-
**De Morgan**

**Modus Ponens**

**Contraposition**

There are (infinitely) many other propositional consequences.
A general strategy to show that

is a propositional consequence is to show that
`A` => `B`
is a propositional tautology.

**Proposition 154 (Tautology)**
A propositional formula with variables is a *propositional
tautology (aussagenlogische Tautologie)* if it is true for every assignment of
truth values to the variables.

We can show that a propositional formula with variables is a tautology by
constructing a truth table or by applying the *indirect method*.

**Example**
We show that
((`A` \/ `B`) /\ (`A` => `C`) /\ (`B` => `C`)) => `C`.

is a tautology by assuming that its truth value is false and then
deriving a contradiction:
((`A` \/ `B`) /\ (`A` => `C`) /\ (`B` => `C`)) => `C`

Because the implication is false, `C` is false and the
conjuncts are true. Thus
`A` and `B` must be false (since `C` is false, the
implications cannot be true otherwise). Therefore `A` \/ `B` is false, which contradicts above derivation.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999