Classifying topos for higher order logic

138 Views Asked by At

Chapter X of Mac Lane and Moerdijk's Sheaves in Geometry and Logic focuses on Classifying topoi. The basic concept in the early pages is the one of geometric formula, which is by definition a first-order formula.

Now, it is possible that it comes clear later in the book, but just for curiosity: is there a version of "Classifying topos" in higher order logic? I.e., can one introduce similar notions when the language is not first-order, and so "classify" kinds of objects which are intrinsically higher-order?

Sorry if the question is vague (hope it has at least sense), but before going through I would just like to satisfy this curiosity.

Thank you in advance.

1

There are 1 best solutions below

0
On BEST ANSWER

The answer is yes, you will have to move from geometric to logical morphisms. Look at the Ph.D thesis of Awodey.

PS. That chapter is amazing.