Tableaux'method for intuitionistic logic through S4-translation

Tableaux'method for intuitionistic logic through S4-translation

The formula
((p => q) => (-q => -p))
is valid
Proof that the negation of its S4-translation is unsatisfiable
(1) 1: -[]([]([]p => q) => ([]-[]q => -[]p))
(2) 1: <>-([]([]p => q) => ([]-[]q => -[]p))  from 1
(3) 1 -> 2  from 2
(4) 2: -([]([]p => q) => ([]-[]q => -[]p))  from 2
(5) 2: []([]p => q)  from 4
(6) 2: -([]-[]q => -[]p)  from 4
(7) 2: ([]p => q)  from 5
(8) 2: []-[]q  from 6
(9) 2: --[]p  from 6
(10) 2: -[]q  from 8
(11) 2: <>-q  from 10
(12) 2: []p  from 9
(13) 2: p  from 12
  case 1
  (14) 2: -[]p    from 7
  (15) 2: F    from 12 and 14
  end case 1

case 2
  (14) 2: q    from 7
  (15) 2 -> 3    from 11
  (16) 3: -q    from 11
  (17) 3: []([]p => q)    from 15 and 5
  (18) 3: []-[]q    from 15 and 8
  (19) 3: []p    from 15 and 12
  (20) 3: p    from 19
  (21) 3: -[]q    from 18
  (22) 3: <>-q    from 21
  (23) 3: ([]p => q)    from 17
    case 2.1
    (24) 3: -[]p      from 23
    (25) 3: F      from 19 and 24
    end case 2.1

case 2.2
    (24) 3: q      from 23
    (25) 3: F      from 16 and 24
    end case 2.2

end case 2