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