Seem I can't use latex commands on here. Latex works on math.stackexchange, maybe it would be a good idea here as well if linguistics.stackexchange is intended to be a place for questions about formal semantics.
I am basing my question on chapters 'Montague Grammar' and 'Intensional Type Theory' of Gamut 1991.
Basically, I wonder about the interpretation of (higher order) variables in intensional type theory, and the effect on meaning postulates in MG.
Gamut presents 'Meaning Postulate 2', essentially saying that a relation between individuals and second-order properties representing an extensional transitive verb must be equivalent to a relation between individuals, as follows:
Exist S, For all x, For all X, Box, Delta(x, X) <--> Caret_Down X(Caret_Up lambda-y Caret_down S(x, y))
Here, S is a variable of type
<s, <e, <e, t>>> (two-place FO relation), X is a variable of type
<s, <<s, <e, t>>, t>> (SO property), and Delta is a constant symbol representing any extensional TV.
Here's the alternative version I have in mind:
Exist S, For all x, For all X, Box Delta(x, Caret_up X) <--> X(Caret_Up lambda-y Caret_down S(x, y))
S and Delta as above, but variable X is now of type
<<s, <e, t>>, t>, i.e. a set of first-order properties, instead of a second-order property.
I hope despite the lack of typesetting the difference became clear:
The original MP2 (in the GAMUT version) demands the existence of a relation S s.t. for all individuals x and for all second-order properties X, if Delta holds between x and the SO property X, then the extension of the SO property X behaves in a certain way.
Version 2 instead requires the existence of a relation S s.t. for all individuals x and for all sets of first-order properties X, if Delta holds between x and the intension of X, then the set of FO properties X behaves in a certain way.
Even shorter, and a bit imprecise: (v1) quantifies over the intension of terms, (v2) over the extension of terms.
By our definition of the semantics of ITT we can show the equivalence of interpretation of "Intension of alpha", "I(alpha)" (where I is the interpretation function of constants) and "Caret_Up(alpha)", so leaving quantification aside, (v1) and (v2) could be taken to be equivalent.
However, by our interpretation of quantifiers, "For all X" will range over (semantic) objects, not syntactic objects (i.e. not term symbols, but sets and functions over our domain), so I am not sure if I am right to think the two are equivalent, i.e. whether models of (v1) and (v2) are equivalent w.r.t. any expression of L_ITT.