Skip to main content
added 246 characters in body
Source Link

I think the main references for this are Jacobs's book Categorical Logic and Type Theory (Chapter 8), and also Crole's Categories for Types.

The rough idea is to do categorical logic over the `algebraic theory of types'. That is, you consider a category whose objects are finite products of a certain object $\mathit{Type}$, and whose morphisms $A \to \mathit{Type}$ are thought of as types with free type variables in $A$. Then, models are fibrations over such categories, of which you ask for more structure to be able to quantify over predicates. By carefully tuning what you demand, you may obtain quantification over all kinds of higher-order predicates, but there are ways of sticking to second-order logic.

Regarding your terminological question about the term `higher-order', I'd say `higher-order' refers both to higher-order functions and to quantification over higher-order predicates, as in, e.g., System $F\omega$. This is of course annoying.

I think the main references for this are Jacobs's book Categorical Logic and Type Theory (Chapter 8), and also Crole's Categories for Types.

The rough idea is to do categorical logic over the `algebraic theory of types'. That is, you consider a category whose objects are finite products of a certain object $\mathit{Type}$, and whose morphisms $A \to \mathit{Type}$ are thought of as types with free type variables in $A$. Then, models are fibrations over such categories, of which you ask for more structure to be able to quantify over predicates. By carefully tuning what you demand, you may obtain quantification over all kinds of higher-order predicates, but there are ways of sticking to second-order logic.

I think the main references for this are Jacobs's book Categorical Logic and Type Theory (Chapter 8), and also Crole's Categories for Types.

The rough idea is to do categorical logic over the `algebraic theory of types'. That is, you consider a category whose objects are finite products of a certain object $\mathit{Type}$, and whose morphisms $A \to \mathit{Type}$ are thought of as types with free type variables in $A$. Then, models are fibrations over such categories, of which you ask for more structure to be able to quantify over predicates. By carefully tuning what you demand, you may obtain quantification over all kinds of higher-order predicates, but there are ways of sticking to second-order logic.

Regarding your terminological question about the term `higher-order', I'd say `higher-order' refers both to higher-order functions and to quantification over higher-order predicates, as in, e.g., System $F\omega$. This is of course annoying.

Source Link

I think the main references for this are Jacobs's book Categorical Logic and Type Theory (Chapter 8), and also Crole's Categories for Types.

The rough idea is to do categorical logic over the `algebraic theory of types'. That is, you consider a category whose objects are finite products of a certain object $\mathit{Type}$, and whose morphisms $A \to \mathit{Type}$ are thought of as types with free type variables in $A$. Then, models are fibrations over such categories, of which you ask for more structure to be able to quantify over predicates. By carefully tuning what you demand, you may obtain quantification over all kinds of higher-order predicates, but there are ways of sticking to second-order logic.