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 case 1 (12) 2: --[]p from 6 (13) 2: F from 8 and 12 end case 1 case 2 (12) 2: --[]q from 6 (13) 2: F from 9 and 12 end case 2
examples
|
rules
|
syntax
|
info
|
home
|
download
|
basis of the method (in french)
Last Modified : 17-Dec-2021