Page 357 - Encyclopedia of Philosophy of Language

an object of type a and t(x,p) a function from objects of type a to objects of type /?. Note that clause (v) is rather similar to clause (iii), and clause (iv) to (vi).
A
type (s, ((e, t), t)), i.e., properties of sets of individuals, and objects of type e individuals.
Unlike predicate logic and extensional type theory, intensional type theory does not satisfy a so-called replacement theorem:
The reason is that the cap-operator'
like the lambda-abstractor T; it abstracts, so to speak, only over objects of type s. Since s is not really a type in this system so that variables of that type are disallowed, one has to introduce a separate operator to be able to denote the intension of an expression into the formal language. Similarly, the cup-operator is a form of function application; it yields the value of an intension at the present world. According to clause (vii), finally, the necessity operator captures universal necessity.
Table 2 gives the intension of the expressions in Table 1 in terms of types:
Table 2.
Expression
proper names, definite descriptions
sentences common nouns,
intransitive verbs transitive verbs determiners conjunctions
Type
e
(M ) (',(M »
(5,((j,((*,0,0),(«,0)) (j,((j,(*,r)),(j,((*,0,/)))) (j,((j,fl,(j,fl,fl))
This principle still does hold, though, if the type of t"is extensional; that is to say: intensional type theory generalizes extensional type theory.
A counterexample to the replacement theorem is
v
the context C\(xe = (the tallest man)). Here, 'the tall-
est man' is interpreted as an object of type (s,e); namely, the function that assigns to each possible world the tallest man in that world. Then, even if:
v
ljohn]a_w =l (the tallest man)]^
it may still be so that:
v
l[john/x]O(xe = (the tallest manj)]aiW
vv
9*[[ (the tallest man)/x]Q(x,= (the tallest
man))]fliB,
John may be the tallest man in world w, but of course it is not necessary that he is the tallest man in any
In the case of proper names, definite descriptions, and sentences, it is plain that the types of objects are identical to the objects given in Table 1. But this also holds good for the other kinds of expression. For instance, objects of type (s, (e, /)) are functions from possible worlds to sets of individuals. Similarly, objects of type (s, (((s, (e, /)), t), (e, /))), the transitive verbs, are functions from possible worlds to objects of type (((s, (e, /)), t), (e, /)). The latter objects, in turn, are best seen as two-place relations among objects of
be false. On the other hand, in each world the tallest
v
man is necessarily the tallest man: l[ (the tallest
man)/x]{3(xe="(the tallest mari))\atW is always true. In short, one has a counterexample to the invalid reasoning:
John is the tallest man.
Necessarily, the tallest man is the tallest man. .'. Necessarily, John is the tallest man.
See also: De Dicto/De Re; Intension; Modal Logic.
Bibliography
Gamut L T F 1991 Logic Language and Meaning. Vol. 2: Intensional Logic and Logical Grammar. University of Chicago Press, Chicago, IL
Mathematical logic studies formal languages. The language which is the object of logical study is called the 'object language,' the vehicle of thought in study- ing it is the 'metalanguage.' Generally, the syntax of the object language is rigorously defined, that of the metalanguage is not. The object language might be the first-order language of arithmetic, with a fixed
logical and nonlogical vocabulary and unambiguous formation rules. The metalanguage is the informal language of mathematics with some additional formal elements such as elements of set theoretic notation and abbreviations like iff (for: 'if and only if) and => (for: 'only if). Because the object language was devised to formalize mathematical reasoning, the logi-
' functions much
Metalanguage versus Object Language J. van Eijck
Metalanguage versus Object Language
Replacement theorem
If [/ = t']a,w = 1, then l[t/x]t' = (t'/x]t"l,w
= 1.
world. So l[john/x][3(xe=
v
(the tallest mari))\a<w may
335