ch5_everydays_logic/index.html

<html>
<title> Everyday logic </title>
<body bgcolor=#08FFFF>
<h1> Everyday logic </h1>

<a href="SRC/chap5.v"> Examples from the book 
<h2> Exercises </h2>


<a href="fol.html">  Exercise 5.2 page 110 </a> Some proofs in predicate calculus
<br>
<a href="on_negation.html">  Exercise 5.3 page 120 </a> On Negation
<br>
<a href="dyslexia.html">  Exercise 5.4 page 120 </a> Some bad inference rules
<br>
<a href="one_four.html">  Exercise 5.5 page 122 </a> Introducing equality and disjunction
<br>
 <a href="intuitionism.html">  Exercise 5.6 page 122  </a> Intuitionistic Propositional Logic
<br>
 <a href="class.html"> Exercise 5.7 page 123  </a> Five characterizations of classical logic 
<br>
<a href="exo_on_ex.html"> Exercise 5.9 page 124 </a> On the existential quantifier 
<br>
<a href="plus-permute2.html">  Exercise 5.10 page 127 </a> Using <tt>pattern</tt> and <tt>rewrite</tt>
<br>
<a href="eq-trans.html">   Exercise 5.11 page 129 </a> Transitivity of Leibniz equality
<br>
<a href="impred_not.html">   Exercise 5.13 page 131 </a> On Negation (impredicative definition) 
<br>
<a href="leibniz.html"> Exercise 5.14 page 132 </a> An impredicative definition of equality
<br>
<a href="impred.html">  Exercise 5.15 page 133 </a> Some other impredicative definitions
<br>
<a href="my_le.html"> Exercise 5.16 page 134 </a> An impredicative definition of <tt>&lt;=</tt>
<br>
<hr>

<h2>Errata</h2>
<ol>
<li> Page 109, second paragraph. Read "rank 4" instead of "rank 3".
<li> Page 110, script for <tt>all_imp_dist</tt>. Remove the useless
<tt>assumption</tt> at the end of the proof.
<li>
Page 110 to 113 : the old names <tt>mult_le_r</tt> and  and <tt>mult_le_l</tt>
 should 
be replaced respectively by <tt>mult_le_compat_r</tt>  and <tt>mult_le_compat_l</tt>.
<li> Page 115, Section 5.1.4, third paragraph. Read "trivial" instead of
"assumption".
</ol>
</body>
</html>