From 0965d96f46de75e162f211bae3d1af0faec08a95 Mon Sep 17 00:00:00 2001 From: Yiannis Hadjicharalambous Date: Mon, 18 Aug 2025 18:44:54 +0200 Subject: [PATCH 1/5] Update systems-distinct.tex --- content/normal-modal-logic/axioms-systems/systems-distinct.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/normal-modal-logic/axioms-systems/systems-distinct.tex b/content/normal-modal-logic/axioms-systems/systems-distinct.tex index b22d424a..a5362cba 100644 --- a/content/normal-modal-logic/axioms-systems/systems-distinct.tex +++ b/content/normal-modal-logic/axioms-systems/systems-distinct.tex @@ -92,7 +92,7 @@ $\mSat/{{}}{\Box\Diamond\lnot p}$}, right=of w1] {$w_2$} ; \draw[reflexive above] (w2) to (w2); \node[world] (w3) [label={right:\mFalse{p}},right=of w2] {$w_3$}; - \draw[reflexive above] (w2) to (w2); + \draw[reflexive above] (w3) to (w3); \draw[->, bend left] (w1) to (w2); \draw[->, bend left] (w2) to (w3); \draw[->, bend left] (w3) to (w2); From 05cc241eda3c4ade60c0e7da7687bd470c5054f5 Mon Sep 17 00:00:00 2001 From: Yiannis Hadjicharalambous Date: Thu, 21 Aug 2025 00:42:10 +0200 Subject: [PATCH 2/5] i think this should be checked too since it's been applied (step 8 & 9) --- content/normal-modal-logic/tableaux/countermodels.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/normal-modal-logic/tableaux/countermodels.tex b/content/normal-modal-logic/tableaux/countermodels.tex index 19d23d38..cd9e721c 100644 --- a/content/normal-modal-logic/tableaux/countermodels.tex +++ b/content/normal-modal-logic/tableaux/countermodels.tex @@ -111,7 +111,7 @@ [\pFmla{\False}{\Box(p \lor q) \lif (\Box p \lor \Box q)}{1}, just = \TAss, checked [\pFmla{\True}{\Box(p \lor q)}{1}, - just = {\TRule{\False}{\lif}[1]}, + just = {\TRule{\False}{\lif}[1]}, checked [\pFmla{\False}{\Box p \lor \Box q}{1}, just = {\TRule{\False}{\lif}[1]}, checked [\pFmla{\False}{\Box p}{1}, From c3be4fe51c57c6d936c28fdb956fd1d686d1fa88 Mon Sep 17 00:00:00 2001 From: Yiannis Hadjicharalambous Date: Thu, 21 Aug 2025 16:33:10 +0200 Subject: [PATCH 3/5] correction on which proof line used --- .../normal-modal-logic/axioms-systems/proofs-modal-systems.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex b/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex index 63359fa7..e469030b 100644 --- a/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex +++ b/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex @@ -51,7 +51,7 @@ with $\Box!A$ for $p$\\ 3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL 1, 2\\ 4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\ - 5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 1, 4. \\ + 5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 4, 3. \\ \end{derivation} \item $\Log{KB4} \Proves \Ax{5}$: \begin{derivation} From 8360b1c04d2922d5085a2c49b2137149055271a4 Mon Sep 17 00:00:00 2001 From: Yiannis Hadjicharalambous Date: Mon, 25 Aug 2025 14:53:53 +0200 Subject: [PATCH 4/5] minor typo corrections again --- .../axioms-systems/proofs-modal-systems.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex b/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex index e469030b..fc4a5d2e 100644 --- a/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex +++ b/content/normal-modal-logic/axioms-systems/proofs-modal-systems.tex @@ -31,7 +31,7 @@ \begin{derivation} 1. & $\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$ & \Ax{5}\\ 2. & $\Log{KT5} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$\\ - 3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL. + 3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL, 2, 1. \end{derivation} \item $\Log{KT5} \Proves \Ax{4}$: \begin{derivation} @@ -39,7 +39,7 @@ with $\Box!A$ for $p$\\ 2. & $\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$ & $\Ax{T_\Diamond}$ with $\Box!A$ for $p$\\ - 3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 1, 2\\ + 3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 2, 1\\ 4. & $\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$ & $\Ax{5_\Diamond}$\\ 5. & $\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$ & \RK{}, 4 \\ 6. & $\Log{KT5} \Proves \Box!A \lif \Box\Box!A$ & \PL, 3, 5. \\ @@ -49,8 +49,8 @@ 1. & $\Log{KDB4} \Proves \Diamond\Box!A \lif !A $ & $\Ax{B_\Diamond}$ \\ 2. & $\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$ & $\Ax{D}$ with $\Box!A$ for $p$\\ - 3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL 1, 2\\ - 4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\ + 3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL, 1, 2\\ + 4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\ 5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 4, 3. \\ \end{derivation} \item $\Log{KB4} \Proves \Ax{5}$: From 6f21ba2f35bc601df3037a96c366716cae649c91 Mon Sep 17 00:00:00 2001 From: Yiannis Hadjicharalambous Date: Wed, 27 Aug 2025 11:44:23 +0200 Subject: [PATCH 5/5] Fix parentheses issues in more-proofs-in-K.tex --- .../normal-modal-logic/axioms-systems/more-proofs-in-K.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex b/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex index 1205f13c..80e1854d 100644 --- a/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex +++ b/content/normal-modal-logic/axioms-systems/more-proofs-in-K.tex @@ -71,11 +71,11 @@ \begin{proof} \begin{derivation} - 1. & $\Log{K} \Proves \lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B)$ & \Taut \\ + 1. & $\Log{K} \Proves \lnot !A \lif (\lnot !B \lif \lnot (!A \lor !B))$ & \Taut \\ 2. & $\Log{K} \Proves \Box\lnot !A \lif - (\Box\lnot!B \lif \Box \lnot (!A \lor !B)$ & \RK\\ + (\Box\lnot!B \lif \Box \lnot (!A \lor !B))$ & \RK\\ 3. & $\Log{K} \Proves \Box\lnot !A \lif (\lnot \Box \lnot (!A \lor!B) - \lif \lnot\Box\lnot !B))$ & \PL, 2\\ + \lif \lnot\Box\lnot !B)$ & \PL, 2\\ 4. & $\Log{K} \Proves \lnot \Box \lnot(!A \lor !B) \lif (\Box \lnot !A \lif \lnot\Box\lnot !B)$ & \PL, 3\\ 5. & $\Log{K} \Proves \lnot \Box \lnot(!A\lor!B) \lif (\lnot