The question “What is the relation between lambda calculus and logical form?" is comparable to the question “What is the relation any formal system of representation and the logical form of natural languages?”
The answer then is trivially, that the relation is representational, or, one of translation. Lambda calculus can represent many things, only one of which is the LF of L.
Conventions
Let’s denote some natural language as L; its logical form as LF; and F as a formal system with alphabet A and a set of formation rules R, which can generate the expressions of LF.
Lambda Calculus
In what sense, and when, can lambda calculus be considered a better representational system for the LF of L, than say,
- predicate logic
- predicate logic enriched with events
- predicate logic enriched with tense, modality, and possible worlds
Each of such formal logics have different expressive capabilities. They may vary in their suitability for denoting the semantics of natural languages because they acknowledge different logical entities, like events or time intervals, so they introduce new variables to be quantified over.
Different logics acknowledge different logical entities
Logics are ontologies, systems expressing what exists.
The most austere and restrictive ones acknowledge only elements and sets.
But Russell, Church, Reichembach and others, enriched it with higher types.
Davidson added events.
Others acknowledged times, time intervals, modalities, propositions, possible worlds, and more. Montague semantics has all of it.
You can take 'lambda calculus' as a limit of expressivity for a formal language - it can acknowledge and interoperate with an infinite number of types of entities.
That means that lambda calculus is a syntactic system for expressing various systems of logic, so it is up to the person at hand to decide what underlying system of logic they will be using it with.
Lambda calculus is actually a meta-syntax for any type of logic
The enormous advantage of lambda calculus over elementary logics as a metalanguage for LF comes from that, assuming the analyst accepts a very rich ontology such as Frege's, where entities are either functions or objects of any type one chooses to include, it is possible to consider any non-atomic expression e of any L as the product of two factors, a function F and its argument a, and say that F(a) = e.
Since any function can be turned into an argument of a higher-order function - this is called type-shifting, type-raising, and is essentially function composition, the analyst can - recursively - re-analyze functions as arguments, and viceversa, at will, depending on the type of the domains of the functions they may be interested in, in order to exhaustively analyze e into just two factors: a function F, and its argument a.
In other words, it provides a very general, open level of abstraction and flexibility which can accommodate any type of logic, because it’s a way of allowing any system of logic to be expressed as elements and composition of functions on them, regardless of what the particular functions are (ie modal, temporal, epistemic, etc.)
By non-atomic expression, I literally mean any expression - i.e., not just sentences, words, or intermediate phrases, of any level of internal complexity - NPs, VPS, APs, AdvPs, PPs, QPs… - but also strings - continuous or not - of linguistic material that, under other analytical approaches (e.g., phrase structure grammar, with its constituency tests), would not be acknowledged as relevant syntactic constituents, and therefore would not be eligible to undergo operations - (either in syntax or at LF).
Lambda calculus is built on abstract mathematics
Actually, since lambda calculus is based on functional analysis, and the latter is so powerful a tool, it can in principle be applied even to sub-morphemic units.
In other words, 'features' (= [attribute:value] pairs) or even feature-values can also be analysed as 'arguments' (or functions!) if necessary, although, in practice, most syntactic-semantic theories treat minimal 'signs' as unanalysable atoms and seldom or never perform sub-atomic analysis (the event structure of verbs, mainly, excluded).
That makes lambda calculus an extremely powerful and flexible metalanguage for the representation of the 'factors' that compositionally contribute meaning to NL expressions of any level of complexity. You can take the sense of a DP expression like 'the definition of syntactic categories in English' and analyze it into a function 'the definition of syntactic categories in __' and an argument 'English', just as easily as you can take the function to be 'the' and the argument the rest of that DP (the NP), or the function to be 'the definition of syntactic __ in English' and the argument to be 'categories', etc. In principle, given an LF object O you can 'abstract' ANY component C of O and analyse the remainder as a function F( ) = O.
One of the consequences that have attracted more attention is that if lambda calculus is available to compute LF, grammars can be monostratal, i.e., it is possible to compute 'meaning' directly from 'surface syntax'. Thus, constructions that in early PSG or 'Chomskian generative grammar' are supposed to involve 'displacement' (e.g., WH-Movement, Topicalisation, Subject Raising, Extraposition, Right Node Raising, etc.) can be computed as if everything was 'in situ' provided certain kinds of PSG (GPSG, HPSG, etc.) or Categorial Grammar work in tandem with Lambda Calculus to generate syntactic structures and calculate compositional LFs, respectively. Also, since in lambda calculus virtually anything can be treated as a syntactic/semantic 'factor' ('constituent'), coordinative or elliptical constructions (e.g., Gapping, Sluicing, Right Node Raising) that under standard PSG approaches create constituency paradoxes, no longer do in Categorial Grammar cum Lambda Calculus. Mark Steedman's Surface Structure and Interpretation(MIT 1996) or The Syntactic Process (MIT 2000) are authoritative and readable classical statements in this respect. At a more elementary level (and under a Chomskian view of syntax), I. Heim & A. Kratzer's Semantics in Generative Grammar (Blackwell, 1998) is also worth reading.
Of course, all that immense analytical and computational power has its negative side, too: grammars must not only be simple and elegant, but also, and above all, empirically adequate, which means able to generate enough without overgenerating, and, as you can imagine, unrestricted categorial grammar cum lambda calculus overgenerates massively, it acknowledges wildly extravagant LF/semantic entities ('objects' and 'functions') which must ultimately correlate with just as extravagant extralinguistic 'entities', and, needless to say, raises formidable linguistic-theoretic, metaphysical and philosophical issues.
