Svejdar proof method for GL logic
[](p => -[]p).-[]F =>-[]p
Proof 1 : []F, []p, [](p => -[]p), p |-- p, F initial sequent 2 : []F, []p, [](p => -[]p), p |-- []p, F initial sequent 3 : -[]p, []F, []p, [](p => -[]p), p |-- F by notR applied to 2 4 : (p => -[]p), []F, []p, [](p => -[]p), p |-- F by implyL applied to 1, 3 5 : []p, [](p => -[]p) |-- []F by necR applied to 4 6 : [](p => -[]p) |-- -[]p, []F by notL applied to 5 7 : -[]F, [](p => -[]p) |-- -[]p by notR applied to 6 8 : ([](p => -[]p) . -[]F) |-- -[]p by andL applied to 7 9 : |-- (([](p => -[]p) . -[]F) => -[]p) by implyR applied to 8
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021