theorem, which has a surprisingly tedious proof, says that the function does
what it is intended to do.
Theorem. For all conditions γ and boxes Φ:
=AX λiφt = λi∃j(Φ(i)(j))
=AX λiγt = γ
References
[1] Andrews, P.B.: 1986, An Introduction to Mathematical Logic and Type
Theory: to Truth through Proof, Academic Press, Orlando, Florida.
[2] Barwise, J.: 1987, Noun Phrases, Generalized Quantifiers and
Anaphora, in P. Grdenfors (ed.), Generalized Quantifiers, Reidel, Dor-
drecht, 1-29.
[3] Van Benthem, J.F.A.K.: 1986, Essays in Logical Semantics, Reidel,
Dordrecht.
[4] Van Benthem, J.F.A.K.: 1988, The Lambek Calculus, in: R.E. Oehrle,
E. Bach and D. Wheeler (eds.), 1988, Categorial Grammars and Natural
Language Structures, Reidel, Dordrecht.
[5] Van Benthem, J.F.A.K.: 1991, Language in Action, North-Holland, Am-
sterdam.
[6] Church, A.: 1940, A Formulation of the Simple Theory of Types, The
Journal of Symbolic Logic 5, 56-68.
[7] Gallin, D.: 1975, Intensional and Higher-Order Modal Logic, North-
Holland, Amsterdam.
[8] Groenendijk, J. and Stokhof, M.: 1990, Dynamic Montague Grammar,
in L. Klmn and L. Plos (eds.), Papers from the Second Symposium on
Logic and Language, Akadmiai Kiad, Budapest, 3-48.
[9] Groenendijk, J. and Stokhof, M.: 1991, Dynamic Predicate Logic, Lin-
guistics and Philosophy 14, 39-100.
13