fixed other typos (I hope there is no more now)

livrelogique · Mar 6, 2024 · c50cb44 · c50cb44
1 parent 4f1851e
commit c50cb44
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/dist/sequentcalculus.html b/dist/sequentcalculus.html
@@ -122,7 +122,7 @@ <h3>Examples of proofs</h3>
       //|- p or not p
     </textarea>
 
-    Try to prove the following De Morgan law in sequent calculus: <code>not (p or q) -> (not p) and (not q)</code>
+    Try to prove the following De Morgan's law in sequent calculus: <code>not (p or q) -> (not p) and (not q)</code>
     <textarea proofSystem="SequentCalculus">
       //p |- p, q
       //|- p, q, not p
@@ -334,8 +334,8 @@ <h3>First-order proofs using contraction rules</h3>
 
     Try to prove the drinking person's paradox: in a bar, there is always a person such that if this person drinks, everyone drinks.
     <textarea proofSystem="SequentCalculus">
-      //P(x), P(y) |- P(y), forall y P(y)
-      //P(x) |- P(y), (P(y) -> forall y P(y))
+      //P(x), P(y) |- P(y), forall z P(z)
+      //P(x) |- P(y), (P(y) -> forall z P(z))
       //P(x) |- P(y), exists x (P(x) -> forall y P(y))
       //P(x) |- forall y P(y), exists x (P(x) -> forall y P(y))
       //|- P(x) -> forall y P(y), exists x (P(x) -> forall y P(y))