Page 336 - Encyclopedia of Philosophy of Language

Formal Semantics
xex from the set of well-formed formulas. Roughly, characteristic function of) the set of men and the set everyvariablex,y,z,...isannotated(typed)withan ofwalkers.ThenAP•3x[MAN(x)&P(x)]isacomplex
index neN, and xnexm is acceptable only if m=n+1. Within set theory, this theory of types was superseded by Zermelo's axiomatization, where the axiom of foundation requires that each set be well-founded.
The idea of typing recurred in the context of lambda calculus, which was originally conceived by Church (1932-33) as part of a general theory about functions and logic, and intended as a foundation for math- ematics. Although the full system turned out to be inconsistent, the subsystem dealing with functions only turned out to be a successful model for com- putable functions. This system, the pure lambda calcu- lus, is a type-free theory about functions as 'rules' (prescriptions). Typed lambda calculus can be seen as a theory about functions as 'graphs' (sets of ordered pairs). In the (Church-style) typed lambda calculus under consideration here, every term has a unique type: it is an annotated version of a type-free lambda term. Within this theory, all usual logical operators (Boolean connectives and quantifiers) are definable in terms of application, abstraction, and identity.
The set of 'types' consists of primitive types and types formed out of them by means of certain oper- ations. Common primitive types in logical semantics include e (entities) and t (truth values). Only the type- forming operator that forms function types (a, b) out of types a and b will be used. A 'frame' D is a family of domains Da, one for each type a, such that D, is an arbitrary nonempty set (th e set of individuals), D,= {0,1}, the set of truth values, and D(fl;£>)=D?- the set of functions from objects in D0 to objects in Dfc. (Using 'Schonfinkel's trick' (1924), the functions of several arguments can be obtained by iteration of application.)
The formal 'language' to refer to objects in such structures consists of the following 'terms': infinitely many variables xa of each type a; some typed constants ca; and the following compound terms: if a(aj>) and ra are terms, then <r(t) is a term of type b ('application'); ifabisatermandxa isavariable,thenAx•aisaterm of type (a, b) ('abstraction'); and if aa and ra are terms, thenCT=Tis a term of type t ('identity').
A 'model' M is an ordered pair <D, I), where D is a
frame, and I is an 'interpretation function': a function
term of type ((e,f)» 0 which denotes the function from sets of individuals to truth values such that a set is assigned the value 1 iff there is a man in that set: a plausible interpretation for the noun phrase a num. Now, consider the term A.P•3x[MAN(x) A P(JC)](WALK) of type t. The value of this term is the above function applied to the set of walkers. It will be 1 iff there is a man who walks. In fact, the latter term is equivalent to 3x[MAN(x)&WALK(JC)].
There are various alternatives in setting up typed lambda calculus. For example, Montague's IL(inten- sional logic (1974)) is a version of type theory which enables one to form 'intensional' types (s,a) out of a type a. His frames include an additional nonempty set
W (of possible worlds), and the definition of domains w
is extended with the clause that D(J-a)=Da , that is, the set of functions from possible worlds to objects in Da. Together with appropriate adaptions of the for- mal language and its interpretation, this version allows a formal reconstruction of semantic notions such as properties, propositions, and individual con- cepts. Gallin (1975) has shown that IL can be embed- ded into the extensional theory outlined above if it is enriched with a basic type s, such that D,=W. The resulting system is called 'two-sorted type theory.'
Moreover, the whole format of presentation can be shifted. Thus, Orey (1959) proposed to interpret the calculus in hierarchies of'relations,' rather than func- tions. Muskens (1989) has argued that this relational interpretation is more convenient if the objective is to 'partialize' semantics, a move motivated by various linguistic considerations involving the semantics of so-called 'attitude reports' in natural language.
2. Categories
According to Ajdukiewicz (1935), natural language expressions exhibit a function/argument structure, symbolized in the category (A,B) for expressions needing an expression of category A to yield an expression of category B, plus the axioms (A, B), A=>B and A, (A, B)=>B. However, in natural languages these functors usually have a direction in which they look for their arguments. Therefore, Bar-Hillel (1953) pro- posed a 'directed' variant, the so-called 'A jdu- kiewicz/Bar-Hillel calculus' (AB),where left-looking and right-looking functors each have their own axiom: B/A,A=>BandA,A\B=>B.WhenaCutruleisadded: ifT=*AandX,A,Y=>B,thenX,T,Y=>B(whereA,B are categories, T,X, Y finite sequences of categories, and T is nonempty), ABcan be used for language recognition.
Notice that AB grammars are extremely lexicalist. They only have universal axioms, a universal cut rule, and a lexicon. There are no fragment-specific rules for combining expressions. Assume, for example, the lexical category-assignments George -* NP, saw -*•
such that I(ca)eDa for each constant ca.The 'extension' M
or 'interpretation' |<r| * of a term a in a model M undera'variableassignment'g(i.e.,afunctionsuch thatg(xa)eDaforeachvariablexa;g[d/x]istheassign-
ment g' such that g'(x)=d and g'(y) =g(y) if x ^y) is M
defined as follows: |c| *=I(c); W ^^^jc); MMM
KT)| *=|<r| *(|T| -»); |Ajc-<rr*=feD?' such that for MMM
alld:f(d) =H****;and\a=T| *=1iffM *=\r\ *. An example: let P(eJ) and xe be variables which (due to their type) range over (characteristic functions of) sets of individuals and individuals, respectively. Let
MAN(,,() and WALiq,0 be constants interpreted as (the 314