Go backward to B.5.1 Propositional ConsequencesGo up to B.5 Deriving New KnowledgeGo forward to B.5.3 Substitutions |

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

- there must exist some
`x`such that`A`holds before we are allowed to conclude that (**such**`x`:`A`) satisfies`A`; - 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.

(~by showing (contraposition)forallx:A) => (existsx: ~A)

(~i.e. (propositional consequence and substitution, see next subsection)existsx: ~A) => (~~forallx:A)

(~We assumeexistsx: ~A) => (forallx:A).

(*) ~and showexistsx: ~A

Author: Wolfgang Schreiner

Last Modification: October 4, 1999