From 47c41765b17f6f3191b64b3c0767d7fffd59bca7 Mon Sep 17 00:00:00 2001
From: MaxChang3 <36927158+maxchang3@users.noreply.github.com>
Date: Sun, 16 Aug 2026 02:23:14 +0800
Subject: [PATCH] Fix typos in soundness and completeness proofs

- In normal modal logic tableaux soundness, the countermodel must
  falsify A: use \mSat/{M}{!A}[w] instead of \mSat{M}{!A}[w].
- Same fix in intuitionistic logic tableaux soundness.
- In complete-consistent-sets, completeness gives \lnot !A \in \Gamma
  when !A \notin \Gamma.
---
 content/intuitionistic-logic/tableaux/soundness.tex             | 2 +-
 .../completeness/complete-consistent-sets.tex                   | 2 +-
 content/normal-modal-logic/tableaux/soundness.tex               | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/content/intuitionistic-logic/tableaux/soundness.tex b/content/intuitionistic-logic/tableaux/soundness.tex
index ccffaeb1..a0e26775 100644
--- a/content/intuitionistic-logic/tableaux/soundness.tex
+++ b/content/intuitionistic-logic/tableaux/soundness.tex
@@ -19,7 +19,7 @@
   has a closed !!{tableau} then $!B_1, \dots, !B_n \Entails !A$. It is
   easier to prove the contrapositive: if for some $\mModel{M}$ and
   world~$w$, $\mSat{M}{!B_i}[w]$ for all $i=1$, \dots,~$n$ but
-  $\mSat{M}{!A}[w]$, then no !!{tableau} can close. Such a
+  $\mSat/{M}{!A}[w]$, then no !!{tableau} can close. Such a
   countermodel shows that the initial assumptions of the !!{tableau}
   are satisfiable. The strategy of the proof is to show that whenever
   all the prefixed !!{formula}s on !!a{tableau} branch are
diff --git a/content/normal-modal-logic/completeness/complete-consistent-sets.tex b/content/normal-modal-logic/completeness/complete-consistent-sets.tex
index 44a4313c..3f200c4e 100644
--- a/content/normal-modal-logic/completeness/complete-consistent-sets.tex
+++ b/content/normal-modal-logic/completeness/complete-consistent-sets.tex
@@ -81,7 +81,7 @@
     case~\olref{prop:ccs-closed}.}{}
 
 \item If $\lnot!A \in \Gamma$, then by consistency $!A \notin
-    \Gamma$; and if $!A \notin \Gamma$ then $!A \in \Gamma$ since
+    \Gamma$; and if $!A \notin \Gamma$ then $\lnot !A \in \Gamma$ since
     $\Gamma$ is complete $\Sigma$-consistent.
     
   \tagitem{prvAnd}{\iftag{probAnd}{Exercise.}{Suppose $!A \land !B \in
diff --git a/content/normal-modal-logic/tableaux/soundness.tex b/content/normal-modal-logic/tableaux/soundness.tex
index 91995132..598fa28b 100644
--- a/content/normal-modal-logic/tableaux/soundness.tex
+++ b/content/normal-modal-logic/tableaux/soundness.tex
@@ -28,7 +28,7 @@
   has a closed !!{tableau} then $!B_1, \dots, !B_n \Entails !A$. It is
   easier to prove the contrapositive: if for some $\mModel{M}$ and
   world~$w$, $\mSat{M}{!B_i}[w]$ for all $i=1$, \dots,~$n$ but
-  $\mSat{M}{!A}[w]$, then no !!{tableau} can close. Such a
+  $\mSat/{M}{!A}[w]$, then no !!{tableau} can close. Such a
   countermodel shows that the initial assumptions of the !!{tableau}
   are satisfiable. The strategy of the proof is to show that whenever
   all the prefixed !!{formula}s on !!a{tableau} branch are