Overall I still have no understanding of theorem 5.1 though. I'm not terribly familiar with the field in general but the other proofs were still fairly straightforward, whereas this proof loses me in the first sentence, without referencing a result I can look up either inside or outside of the paper.

Were you OK with the proof of Theorem 4.1? To me, that and the proof of Theorem 5.1 are of equal difficulty. (Some of the other authors had more experience with Kripke semantics than I did, so they did most of the editing of those proofs. They work better with diagrams.)

orthonormal seems to believe that PrudentBot couldn't be implemented for the LessWrong PD competition, although he did say with algorithmic proof search, would he change his opinion using Kripke semantics?

Yes; a PD tournament among modal sentences using the code Eliezer linked would be feasible and quite interesting!