From e6a0c431f325091c5dbf8fec0105c53bfc7cfe0f Mon Sep 17 00:00:00 2001
From: Francois Schwarzentruber <fschwarz@schumann.irisa.fr>
Date: Wed, 25 Oct 2023 10:32:10 +0200
Subject: [PATCH] #1 solved: reorganization of the rules in natural deduction

---
 dist/naturaldeduction.html | 57 +++++++++++++++++++++++++++++---------
 1 file changed, 44 insertions(+), 13 deletions(-)

diff --git a/dist/naturaldeduction.html b/dist/naturaldeduction.html
index a5c6d7a..21be6d1 100644
--- a/dist/naturaldeduction.html
+++ b/dist/naturaldeduction.html
@@ -27,7 +27,12 @@ <h2>In propositional logic</h2>
 
   <h3>Examples of direct applications of rules</h3>
 
-First, let us explore the rules in propositional logic. First, you can simply conclude an hypothesis:
+First, let us explore the rules in propositional logic. 
+
+<h4>Dealing with hypotheses</h4>
+
+
+First, you can simply conclude an hypothesis:
   <textarea proofSystem="NaturalDeduction">
     q |- q
   </textarea>
@@ -37,6 +42,16 @@ <h3>Examples of direct applications of rules</h3>
   </textarea>
 
 
+
+Of course, you can add hypothesis without destroying what you already proved:
+
+  <textarea proofSystem="NaturalDeduction">
+p |- q  *
+p, r |- q
+</textarea>
+
+<h4>Absurd</h4>
+
 If an hypothesis of the form <code>not phi</code> leads to a contradiction, you can derive <code>phi</code> and remove that hypothesis.
   <textarea proofSystem="NaturalDeduction">
   not p |- bottom  *
@@ -49,14 +64,8 @@ <h3>Examples of direct applications of rules</h3>
     </textarea>
 
 
-Of course, you can add hypothesis without destroying what you already proved:
-
-  <textarea proofSystem="NaturalDeduction">
-p |- q  *
-p, r |- q
-</textarea>
-
 
+<h4>Implication</h4>
 
 Now, if you suppose <code>p</code> and derive <code>q</code>, you can irrevocably prove <code>p -> q</code>.
 
@@ -72,6 +81,24 @@ <h3>Examples of direct applications of rules</h3>
     </textarea>
 
 
+    If you have already proven <code>p</code> and you have <code>p -> q</code>, you have a proof for <code>q</code>:
+
+    <textarea proofSystem="NaturalDeduction">
+      |-  p             *
+      |-  p -> q        *
+      |- q
+      </textarea>
+  
+  <textarea proofSystem="NaturalDeduction">
+    r |-  p             *
+    r |-  p -> q        *
+    r |- q
+    </textarea>
+
+
+<h4>Or</h4>
+
+
   <textarea proofSystem="NaturalDeduction">
   p |- q  *
   p |- q or r
@@ -89,6 +116,11 @@ <h3>Examples of direct applications of rules</h3>
   p |- s
 </textarea>
 
+
+
+
+<h4>And</h4>
+
   <textarea proofSystem="NaturalDeduction">
 p |- q *
 p |- r *
@@ -106,6 +138,10 @@ <h3>Examples of direct applications of rules</h3>
   p |- r
 </textarea>
 
+
+<h4>Not</h4>
+
+
   <textarea proofSystem="NaturalDeduction">
   p, q |- bottom *
   q |- not p
@@ -122,11 +158,6 @@ <h3>Examples of direct applications of rules</h3>
 
 
 
-
-
-
-
-
 <h3>Examples of proofs</h3>
 
 Show that we can deduce <code>p -> r</code> from <code>(p or q) -> r</code>.