Go backward to B.5.1 Propositional Consequences Go up to B.5 Deriving New Knowledge Go 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".

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.

(~forall x: A) => (exists x: ~A)

(~exists x: ~A) => (~~forall x: A)

(~exists x: ~A) => (forall x: A).

(*) ~exists x: ~A