Intensional and Higher-Order Modal Logic: With Applications to Montague Semantics

Montague's intensional logic IL has variables and constants of every type, application, abstraction and identity, and two operators on indices: ^A, the intension of A, a function from indices, and ˇA, the value at the current index of an intension. A term has a value at an index under an assignment, a constant denoting at each index what its meaning gives it there. Gallin translates IL into the two-sorted type theory Ty₂, where indices are the values of variables of type $s$: a constant becomes a constant of type $⟨s,α⟩$ applied to a distinguished index variable, ^A the abstraction of the translate of A over that variable, and ˇA the application of the translate of A to it. The translation preserves the semantics: the value of a term at an index is the value of its translate with the index variable sent to that index, so a formula is valid in IL exactly when its translate is valid in Ty₂.

Implementation notes

The types of IL are the composition engine's types, the intension type $⟨s,α⟩$ being Ty.intens α, and the terms of Ty₂ are the engine's terms under its total interpretation, with application the mode of functional application and identity a constant interpreted as equality. Variables are typed by a typing of their indices, as the engine's are. The index variable is the variable 0 of the translate, and the variables of the term being translated are shifted up by one, so the translation is defined on every term and captures no variable.

References

• Gallin 1975, Intensional and Higher-Order Modal Logic: With Applications to Montague Semantics