|
31 | 31 | \begin{derivation} |
32 | 32 | 1. & $\Log{KT5} \Proves \Diamond!A \lif \Box\Diamond!A$ & \Ax{5}\\ |
33 | 33 | 2. & $\Log{KT5} \Proves !A \lif \Diamond!A$ & $\Ax{T_\Diamond}$\\ |
34 | | - 3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL. |
| 34 | + 3. & $\Log{KT5} \Proves !A \lif \Box\Diamond!A$ & \PL, 2, 1. |
35 | 35 | \end{derivation} |
36 | 36 | \item $\Log{KT5} \Proves \Ax{4}$: |
37 | 37 | \begin{derivation} |
38 | 38 | 1. &$\Log{KT5} \Proves \Diamond\Box!A \lif \Box\Diamond\Box!A$ & \Ax{5} |
39 | 39 | with $\Box!A$ for $p$\\ |
40 | 40 | 2. & $\Log{KT5} \Proves \Box!A \lif \Diamond\Box!A$ & $\Ax{T_\Diamond}$ |
41 | 41 | with $\Box!A$ for $p$\\ |
42 | | - 3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 1, 2\\ |
| 42 | + 3. & $\Log{KT5} \Proves \Box!A \lif \Box\Diamond\Box!A$ & \PL, 2, 1\\ |
43 | 43 | 4. & $\Log{KT5} \Proves \Diamond\Box!A \lif \Box!A$ & $\Ax{5_\Diamond}$\\ |
44 | 44 | 5. & $\Log{KT5} \Proves \Box\Diamond\Box!A \lif \Box\Box!A$ & \RK{}, 4 \\ |
45 | 45 | 6. & $\Log{KT5} \Proves \Box!A \lif \Box\Box!A$ & \PL, 3, 5. \\ |
|
49 | 49 | 1. & $\Log{KDB4} \Proves \Diamond\Box!A \lif !A $ & $\Ax{B_\Diamond}$ \\ |
50 | 50 | 2. & $\Log{KDB4} \Proves \Box\Box!A \lif \Diamond\Box!A$ & $\Ax{D}$ |
51 | 51 | with $\Box!A$ for $p$\\ |
52 | | - 3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL 1, 2\\ |
53 | | - 4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\ |
| 52 | + 3. & $\Log{KDB4} \Proves \Box\Box!A \lif !A$ & \PL, 1, 2\\ |
| 53 | + 4. & $\Log{KDB4} \Proves \Box!A \lif \Box\Box!A$ & \Ax{4} \\ |
54 | 54 | 5. & $\Log{KDB4} \Proves \Box!A \lif !A$ & \PL, 4, 3. \\ |
55 | 55 | \end{derivation} |
56 | 56 | \item $\Log{KB4} \Proves \Ax{5}$: |
|
0 commit comments