Can someone give me a natural deduction proof for this argument?

I am defending the usefulness of modern logic to a class and I came across this modalized version of a Thomistic argument (https://www.bu.edu/wcp/Papers/Reli/ReliMayd.htm). However, although I have studied both predicate and modal logic before, some of this gentleman's notations confuse me immensely. Namely, I have never seen (3[]t) for example, or a modal quantifier within the exact same parentheses as an existential quantifier.

P.S. with respect to natural deduction proofs, I am looking for something like this:

1. [](P -> Q)
2. <>(P)
3. W1: P .... 2, Possible Instantiation.
4. W1: P -> Q ..... 3, Necessary Instantiation
5. W1: Q ..... 3,4 Modus Ponens
6. <>Q ..... 5, Possible Generalization.
• They might be typos. Also premises 3 and 4 begin with a negation that doesn't seem to match the corresponding expression in natural language and the formula in the first and last parts of the text appear to be different. – Quentin Ruyant Dec 8 '15 at 10:20
• Also it seems to me that there are gaps in the reasoning. For example Aquinas says that it is absurd to think that nothing exists, and this is an important part of the argument, but I can't find any premise in the reconstruction that says that at least one thing exists. – Quentin Ruyant Dec 8 '15 at 10:34