From ff5160f2478aa8f07fef5df00ee8470e2b2aaa3e Mon Sep 17 00:00:00 2001 From: Pi-Cla Date: Thu, 29 Feb 2024 13:46:16 +0000 Subject: [PATCH] Fix TRules getting swapped --- content/normal-modal-logic/tableaux/rules-for-K.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/content/normal-modal-logic/tableaux/rules-for-K.tex b/content/normal-modal-logic/tableaux/rules-for-K.tex index 69ea62cf..0d738b85 100644 --- a/content/normal-modal-logic/tableaux/rules-for-K.tex +++ b/content/normal-modal-logic/tableaux/rules-for-K.tex @@ -108,20 +108,20 @@ prefix~$\sigma$ is $\sigma.n$. However, which $n$ is allowed depends on whether the sign is~$\True$ or~$\False$. -\iftag{prvBox}{The $\TRule{\Box}{\True}$ rule extends a branch +\iftag{prvBox}{The $\TRule{\True}{\Box}$ rule extends a branch containing $\sFmla{\True}{\Box !A}[\sigma]$ by $\sFmla{\True}{!A}[\sigma.n]$.\iftag{prvDiamond}{ Similarly, - t}{}}{T}\iftag{prvDiamond}{he $\TRule{\Diamond}{\False}$ rule + t}{}}{T}\iftag{prvDiamond}{he $\TRule{\False}{\Diamond}$ rule extends a branch containing $\sFmla{\False}{\Diamond !A}[\sigma]$ by $\sFmla{\False}{!A}[\sigma.n]$.}{} \iftag{notprvBox,notprvDiamond}{It}{They} can only be applied for a prefix~$\sigma.n$ which \emph{already} occurs on the branch in which it is applied. Let's call such a prefix ``used'' (on the branch). -\iftag{prvBox}{The $\TRule{\Box}{\False}$ rule extends a branch +\iftag{prvBox}{The $\TRule{\False}{\Box}$ rule extends a branch containing $\sFmla{\False}{\Box !A}[\sigma]$ by $\sFmla{\False}{!A}[\sigma.n]$.\iftag{prvDiamond}{ Similarly, - t}{}}{T}\iftag{prvDiamond}{he $\TRule{\Diamond}{\True}$ rule extends + t}{}}{T}\iftag{prvDiamond}{he $\TRule{\True}{\Diamond}$ rule extends a branch containing $\sFmla{\True}{\Diamond !A}[\sigma]$ by $\sFmla{\True}{!A}[\sigma.n]$.}{} \iftag{notprvBox,notprvDiamond}{This rule}{These rules}, however, can