|
108 | 108 | prefix~$\sigma$ is $\sigma.n$. However, which $n$ is allowed depends
|
109 | 109 | on whether the sign is~$\True$ or~$\False$.
|
110 | 110 |
|
111 |
| -\iftag{prvBox}{The $\TRule{\Box}{\True}$ rule extends a branch |
| 111 | +\iftag{prvBox}{The $\TRule{\True}{\Box}$ rule extends a branch |
112 | 112 | containing $\sFmla{\True}{\Box !A}[\sigma]$ by
|
113 | 113 | $\sFmla{\True}{!A}[\sigma.n]$.\iftag{prvDiamond}{ Similarly,
|
114 |
| - t}{}}{T}\iftag{prvDiamond}{he $\TRule{\Diamond}{\False}$ rule |
| 114 | + t}{}}{T}\iftag{prvDiamond}{he $\TRule{\False}{\Diamond}$ rule |
115 | 115 | extends a branch containing $\sFmla{\False}{\Diamond !A}[\sigma]$ by
|
116 | 116 | $\sFmla{\False}{!A}[\sigma.n]$.}{}
|
117 | 117 | \iftag{notprvBox,notprvDiamond}{It}{They} can only be applied for a
|
118 | 118 | prefix~$\sigma.n$ which \emph{already} occurs on the branch in which
|
119 | 119 | it is applied. Let's call such a prefix ``used'' (on the branch).
|
120 | 120 |
|
121 |
| -\iftag{prvBox}{The $\TRule{\Box}{\False}$ rule extends a branch |
| 121 | +\iftag{prvBox}{The $\TRule{\False}{\Box}$ rule extends a branch |
122 | 122 | containing $\sFmla{\False}{\Box !A}[\sigma]$ by
|
123 | 123 | $\sFmla{\False}{!A}[\sigma.n]$.\iftag{prvDiamond}{ Similarly,
|
124 |
| - t}{}}{T}\iftag{prvDiamond}{he $\TRule{\Diamond}{\True}$ rule extends |
| 124 | + t}{}}{T}\iftag{prvDiamond}{he $\TRule{\True}{\Diamond}$ rule extends |
125 | 125 | a branch containing $\sFmla{\True}{\Diamond !A}[\sigma]$ by
|
126 | 126 | $\sFmla{\True}{!A}[\sigma.n]$.}{}
|
127 | 127 | \iftag{notprvBox,notprvDiamond}{This rule}{These rules}, however, can
|
|
0 commit comments