While syntax dictates the structural well-formedness of linguistic expressions, semantics determines their meaning. Founded by logician Richard Montague in the late 1960s, formal semantics demonstrates that natural languages can be characterized with the same mathematical rigor, model theory, and typed lambda calculus historically reserved for formal symbolic logic.
1. The Principle of Semantic Compositionality
Formulated implicitly by Gottlob Frege, the Principle of Compositionality states that the semantic interpretation of a complex linguistic expression is a strict mathematical function of the semantic values of its immediate syntactic constituents and the syntactic rule used to combine them:
[
llbracket [A B]
rbracket = mathcal{F}left( llbracket A
rbracket, llbracket B
rbracket
ight)
]
Richard Montague famously codified this in his foundational 1970 paper “Universal Grammar”: “There is in my opinion no important theoretical difference between natural languages and the artificial languages of logicians.”
2. Model-Theoretic Semantics: Entities, Worlds, and Truth Values
In formal semantics, linguistic meaning is not an internal mental image, but a relationship between symbols and an abstract mathematical model of the world. A model (mathcal{M}) is defined as an ordered pair:
[
mathcal{M} = langle mathcal{D}, mathcal{I}
angle
]
where:
- (mathcal{D}) is a non-empty domain of individual entities ((mathcal{D} = { a, b, c, dots })).
- (mathcal{I}) is an interpretation function mapping constant symbols to entities ((mathcal{I}( ext{“John”}) = j in mathcal{D})), properties to sets of entities ((mathcal{I}( ext{“runs”}) subseteq mathcal{D})), and (n)-place relations to sets of (n)-tuples ((mathcal{I}( ext{“loves”}) subseteq mathcal{D} imes mathcal{D})).
The semantic value (denotation) of a declarative sentence (S) is its truth value: (llbracket S
rbracket^mathcal{M} in { 0, 1 }).
3. Alonzo Church’s Typed Lambda Calculus
To compute the semantic values of arbitrarily complex phrases compositionally, Montague semantics employs Alonzo Church’s simply typed lambda calculus. The ontological universe is constructed from two primitive semantic types:
- (e): The type of individual entities ((mathcal{D}_e)).
- (t): The type of Boolean truth values ((mathcal{D}_t = { 0, 1 })).
From these primitives, functional types (langle sigma, au
angle) are constructed recursively, representing mathematical functions whose domain is of type (sigma) and range is of type ( au):
- Intransitive Verbs & Common Nouns (Type (langle e, t
angle)): Functions from entities to truth values (characteristic functions of sets). For example:
[
llbracket ext{“sleeps”}
rbracket = lambda x_e . , ext{Sleep}(x)
] - Transitive Verbs (Type (langle e, langle e, t
angle
angle)): Functions taking an object entity argument and returning a predicate:
[
llbracket ext{“loves”}
rbracket = lambda y_e . , lambda x_e . , ext{Love}(x, y)
] - Quantified Noun Phrases (Type (langle langle e, t
angle, t
angle)): Generalized quantifiers acting as higher-order functions over predicates:
[
llbracket ext{“every linguist”}
rbracket = lambda P_{langle e, t
angle} . , orall x_e , [ ext{Linguist}(x) o P(x)]
]
4. Functional Application and Beta-Reduction
The universal compositional rule governing semantic computation at syntactic tree branching nodes is Functional Application:
Functional Application: If a node (alpha) has daughters (beta) and (gamma), where (llbracket beta
rbracket) is of type (langle sigma, au
angle) and (llbracket gamma
rbracket) is of type (sigma), then (llbracket alpha
rbracket = llbracket beta
rbracket(llbracket gamma
rbracket)).
Evaluating an expression proceeds via (beta)-reduction (substituting argument terms for lambda-bound variables). Consider the derivation for the sentence “John loves Mary”:
[
begin{aligned}
llbracket ext{VP}
rbracket &= llbracket ext{“loves”}
rbracket(llbracket ext{“Mary”}
rbracket)
&= (lambda y . lambda x . ext{Love}(x, y))(m) xrightarrow{beta} lambda x . ext{Love}(x, m)
llbracket ext{S}
rbracket &= llbracket ext{VP}
rbracket(llbracket ext{“John”}
rbracket)
&= (lambda x . ext{Love}(x, m))(j) xrightarrow{beta} ext{Love}(j, m)
nd{aligned}
]
The output is a formal first-order proposition that evaluates deterministically to (1) (True) or (0) (False) relative to the state of affairs in model (mathcal{M}), establishing the rigorous mathematical bridge between syntactic syntax and philosophical semantics.
