   Go backward to B.5.1 Propositional ConsequencesGo up to B.5 Deriving New KnowledgeGo forward to B.5.3 Substitutions ### B.5.2 Quantifier Consequences

There are various patterns of conclusions that occur in proofs so frequently that they are considered as "basic knowledge".

Proposition 155 (Quantifier Consequences) For every formula A and B, the following conclusions hold:
Universal Quantification and Conjunction
 (forall x: A /\  B) (forall x: A) /\  (forall x: B)
 (forall x: A) /\  (forall x: B) (forall x: A /\  B)
Existential Quantification and Disjunction
 (exists x: A \/ B) (exists x: A) \/ (exists x: B)
 (exists x: A) \/ (exists x: B) (exists x: A \/ B)
Universal and Disjunction, Existential and Conjunction
 (forall x: A) \/ (forall x: B) (forall x: A \/ B)
 (exists x: A) /\  (exists x: B) (exists x: A /\  B)
Universal and Existential Quantification
 exists x: forall y: A forall y: exists x: A
De Morgan Laws
 ~forall x: A exists x: ~A
 exists x: ~A ~forall x: A
 ~exists x: A forall x: ~A
 forall x: ~A ~exists x: A
Such Quantifier
 exists x: A A[x <- such x: A]
 (forall y_0, y_1: (A[x <- y_0] /\  A[x <- y_1]) => y_0 = y_1) (forall x: A => x = such x: A)

The last two facts about the such quantifier tell us that

1. there must exist some x such that A holds before we are allowed to conclude that (such x: A) satisfies A;
2. to prove that some y with A[x <- y] equals (such x: A), we also have to show that only one such y exists.

These conclusions can be proved by the proving techniques explained before; an example is given below.

Proof  We show for arbitrary formula A
(~forall x: A) => (exists x: ~A)
by showing (contraposition)
(~exists x: ~A) => (~~forall x: A)
i.e. (propositional consequence and substitution, see next subsection)
(~exists x: ~A) => (forall x: A).
We assume
(*) ~exists x: ~A
and show forall x: A. Take arbitrary and assume ~A. Then we have (exists x: ~A) which contradicts (*).

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   