And also higher-order logics. See sections '5.9 Universes' on page 174,
and '6.3.5/6 Quantification and universes' on page 220.
Any book or paper teaching a difficult subject carries advocacy in
one way or another. If the author weren't interested in the subject,
it wouldn't have taken the task of writing the book/paper.
You mentioned "its computational aspects" in your original post.
The main principle underlying current intuitionistic logic/type theory
is that propositions behave as types in programming languages,
and proofs behave as programs (this is my oversimplified point of view,
I forgot to mention the following texts in my last message.
The first one is directly related to complexity theory, it discusses
second-order classical logic over finite structures. The second one
is more detailed, it deals with first and second-order intuitionistic
logic. You may want to compare the semantic differences between
classical SOL and System F (it's not a trivial task!).
Wolfgang Thomas, Languages, automata and logic. Technical Report 9607,
Institut f Informatik und Praktische Mathematik,
Christian-Albrechts-Universit zu Kiel, Germany, May 1996.
J.-Y. Girard (translated and with appendices by Y. Lafont & P. Taylor),
Proofs and Types, Cambridge Tracts in Theoretical Computer Science 7,
Cambridge University Press (1989)
You seem to be interested in applications of logic to artificial
intelligence. Perhaps asking this question in comp.ai or
comp.lang.functional may give more informative answers.
JosJuan Mendoza Rodruez