CLASP
The Centre for Linguistic Theory and Studies in Probability

Propositional Attitude Operators via Homotopy Type Theory

Since it interprets propositions by sets of possible worlds, the intensional logic of Montague (1973) does not distinguish propositions which are true in the same possible worlds. Because of this, the system does not satisfactorily interpret propositional attitude verbs (believe, know, etc.), a fact which has motivated the development of ‘hyperintensional’ logics.

I will discuss a hyperintensional system which naturally incorporates the intensional logic of Montague with the usual notions of homotopy type theory (HoTT). This system is based on a fragment of Shulman (2018). From HoTT, we inherit two notions of equality, ¿ and =, which we think of as expressing intensional and extensional equalities, respectively. From Montague, we inherit a syntax for intensional operators, which for us will, however, mean operators which respect intensional but not (necessarily) extensional equality. These are used to interpret propositional attitude operators.

This approach is in the tradition of other linguistically-motivated systems with two notions of equality (Thomason 1980, Fox and Lappin 2008). Some advantages are that it allows a treatment of de re belief, and inherits a nice model theory from HoTT.