There is a nice book by Melvin Fitting: Types, Tableaus, and Gödel’s God, Kluwer 2002. It introduces some fairly standard typed higher order logic and then form

There is a nice book by Melvin Fitting: Types, Tableaus, and Gödel’s God, Kluwer 2002. It introduces some fairly standard typed higher order logic and then formalizes Gödel's proof in it. Although I personally like it a bit less than Mendelsohn and Fitting's book on first order modal logic, it's a good read (if you like logic and have had some basic course in logic sometime).