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

  1. 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.
Going home
Pierre Castéran