Everyday logic
Examples from the book
Exercises
Exercise 5.1 page 107 Polymorphic minimal propositional logic
Exercise 5.2 page 110 Some proofs in predicate calculus
Exercise 5.3 page 120 On Negation
Exercise 5.4 page 120 Some bad inference rules
Exercise 5.5 page 122 Introducing equality and disjunction
Exercise 5.6 page 122 Intuitionistic Propositional Logic
Exercise 5.7 page 123 Five characterizations of classical logic
Exercise 5.9 page 124 On the existential quantifier
Exercise 5.10 page 127 Using pattern and rewrite
Exercise 5.11 page 129 Transitivity of Leibniz equality
Exercise 5.13 page 131 On Negation (impredicative definition)
Exercise 5.14 page 132 An impredicative definition of equality
Exercise 5.15 page 133 Some impredicative definitions
Exercise 5.16 page 134 An impredicative definition of <=
Errata
 Page 109, second paragraph. Read "rank 4" instead of "rank 3".
 Page 110, script for all_imp_dist. Remove the useless
assumption at the end of the proof.

Page 110 to 113 : the old names mult_le_r and and mult_le_l
should
be replaced respectively by mult_le_compat_r and mult_le_compat_l.
 Page 115, Section 5.1.4, third paragraph. Read "trivial" instead of
"assumption".
Going home
Pierre Castéran