Tableaux'method for S4
[]p.[](p =>q) => []q
The formula (([]p . [](p => q)) => []q) is valid Proof that its negation is unsatisfiable (1) 1: -(([]p . [](p => q)) => []q) (2) 1: ([]p . [](p => q)) from 1 (3) 1: -[]q from 1 (4) 1: []p from 2 (5) 1: [](p => q) from 2 (6) 1: p from 4 (7) 1: (p => q) from 5 (8) 1: <>-q from 3 case 1 (9) 1: -p from 7 (10) 1: F from 6 and 9 end case 1 case 2 (9) 1: q from 7 (10) 1 -> 2 from 8 (11) 2: -q from 8 (12) 2: []p from 10 and 4 (13) 2: [](p => q) from 10 and 5 (14) 2: (p => q) from 13 (15) 2: p from 12 case 2.1 (16) 2: -p from 14 (17) 2: F from 15 and 16 end case 2.1 case 2.2 (16) 2: q from 14 (17) 2: F from 11 and 16 end case 2.2 end case 2
examples
|
rules
|
syntax
|
info
|
home
|
download
Last Modified : 17-Dec-2021