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