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 6 (8) 2: (p . q) from 7 (9) 2: p from 8 (10) 2: q from 8 case 1 (11) 2: []-[]p from 5 (12) 2: -[]p from 11 (13) 2: <>-p from 12 (14) 2 -> 3 from 13 (15) 3: -p from 13 (16) 3: [](p . q) from 14 and 7 (17) 3: []-[]p from 14 and 11 (18) 3: -[]p from 17 (19) 3: <>-p from 18 (20) 3: (p . q) from 16 (21) 3: p from 20 (22) 3: q from 20 (23) 3: F from 15 and 21 end case 1 case 2 (11) 2: []-[]q from 5 (12) 2: -[]q from 11 (13) 2: <>-q from 12 (14) 2 -> 3 from 13 (15) 3: -q from 13 (16) 3: [](p . q) from 14 and 7 (17) 3: []-[]q from 14 and 11 (18) 3: -[]q from 17 (19) 3: <>-q from 18 (20) 3: (p . q) from 16 (21) 3: p from 20 (22) 3: q from 20 (23) 3: F from 15 and 22 end case 2
examples
|
rules
|
syntax
|
info
|
home
|
download
|
basis of the method (in french)
Last Modified : 17-Dec-2021