reorganization of the rules in natural deduction

livrelogique · Oct 25, 2023 · cdc2f16 · cdc2f16
1 parent e6a0c43
commit cdc2f16
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/dist/naturaldeduction.html b/dist/naturaldeduction.html
@@ -207,7 +207,7 @@ <h2>First-order logic</h2>
 
 <h3>Examples of direct applications of rules</h3>
 
-
+<h4>Existential quantifier</h4>
 
   <textarea proofSystem="NaturalDeduction">
   Q(x) |- P(a)  *
@@ -231,6 +231,7 @@ <h3>Examples of direct applications of rules</h3>
   Q(x) |- p
 </textarea>
 
+<h4>Universal quantifier</h4>
 
 If you proved <code>P(x)</code> and the hypothesis do not depend on <code>x</code>, then you deduce <code>forall x P(x)</code>. That rule is called the introduction of <code>forall</code>.
   <textarea proofSystem="NaturalDeduction">