A non-compactness phenomenon in logics with hyperintensional predication (Q1264134)

This is a well written paper in which the authors clearly and informally explain the philosophical motivation for the type theory they use before rigorously proving their main theorem. By ``hyperintensional predication'' they mean ``a predication which can assume different truth values on terms having equal intensions but different senses''. The informal exposition clarifies their uses of `extension', `intension', and `sense' while linking them to other treatments of substitution of terms with equal extensions and intensions in expressions for propositional attitudes. They motivate using a type theory adapted from A. Bressan for a logic in a language capable of representing extensions, intensions, and senses. They prove that this logic lacks compactness.