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