temporal logic Kt4



Hello to all.

I need help in creating a good proof of completeness for Kt4 temporal
logic. I am not a mathematician, just untergraduate philosophy student.
I had one seminar devoted to temporal logic, with professional
logician, who required us for pass exam doing a such proof.

If anyone could just show me a general outlines - my professor rejected
prof shown in our textbook by Swirydowicz - Modal Logic - as invalid. I
could not hope to do better than Ph.D in mathematics.

His proof looks as shown:

If |- Kt4 (fi), then (fi) is realised in all transitive and
antireflexive models.
Now assume (fi) is not a statement. By one of the Lindenbaum extension
theorems exists such extension u, that (fi) does not belong to u. From
last lemat comes (TL, (u,n)) |/= (fi) for some pair (u, n), so there is
a transitive and antireflexive model, which falsifies formula (fi).

Sorry for my english, I am not very fluent in it.

.