Propositional modal logic is a standard tool, but first-order modal logic is not. There are problems with constant domains versus varying domains. There are problems with rigidity versus non-rigidity. It is all much more complicated than it needs to be.
In the first part of my talk I will discuss why constant/varying domains is a non-issue. I will also show where the problems with non-rigidity arise. And I will present a semantics and a tableau proof theory that deals with all this, and more, simply and naturally.
In the second part of my talk I will discuss, in a more condensed form, how these ideas carry over to a straightforward higher-order modal logic, with a semantics based on a blend of Kripke and Henkin models. Again, tableau rules are available. I will illustrate their use by applying them to part of the Gödel ontological argument.