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