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