(0) T |- []C=>CTo prove T |- C, we introduce, using the diagonal lemma, a statement L for which the following holds:
(1) T |- L <=> ([]L => C)From (1) we get
(2) T |- L => ([]L => C)By (2) and (P1), we have
(3) T |- [](L => ([]L => C))so by (3) and (P3)
(4) T |- []L => []([]L => C)and by another application of (P3),
(5) T |- []L => ([][]L => []C)So, using (P2) and (5), we have
(6) T |- []L => []C(0) then implies that
(7) T |- []L => CWith (1), this implies that T |- L. So, by (2) we have
(8) T |- []L => Cand since T |- L implies T |- []L by (P1), we finally get T |- C.
A couple of comments: