2
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.