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