-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathintensional.tex
6179 lines (5113 loc) · 271 KB
/
intensional.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\chapter{Modality and intensionality without possible worlds}
\label{ch:intensional}
\setcounter{equation}{0}
\section{Possible worlds, modality and intensionality}
\label{sec:possworlds}
\cite{Montague1973} uses possible worlds to analyze both modality
(represented in his fragment by the adverbs \textit{possibly} and
\textit{necessarily}) and a variety of intensional constructions in
addition to the temperature and price examples discussed in
Chapter~\ref{ch:commonnouns}: intensional transitive verbs such as
\textit{seek}, intensional adverbs such as \textit{voluntarily}, verbs
of propositional attitudes such as \textit{believe} and
\textit{assert} and verbs taking infinitival complements such as
\textit{try (to)} and \textit{wish (to)}.
A short introduction to the
use of possible worlds in modal logic and philosophical conceptions of
possible worlds is given by \cite{Menzel2015}. As he points out at
the beginning of this article possible worlds are considered to be
totalities (or at least a limit) which include the situations which we
are aware of around us.
The notion of possible world is intuitively appealing. We talk of
living in the best (or worst) of all possible worlds. But equally we
talk of the best (or worst) possibility. When we talk in such
terms we normally have a small finite number of possibilities in mind
which we are contrasting. This has led some authors to use the term
``possible world'' to refer not to a total universe but to a small set
of facts that might obtain in some version of the world. This appears
to be standard usage in probability theory \citep[e.g.][]{Halpern2003}. It is
important not to confuse this notion with the notion of possible world
as a totality which is used in semantics, inherited from modal logic.
This point is made by \cite{CooperDobnikLappinLarsson2014a} and \cite{Lappin2015}.
Problems have been raised for the notion possible world. These have to
do with how you individuate and count them and how many possible
worlds there must be. \cite{Rescher1999} takes up these problems from
a philosophical perspective. He argues that it is impossible to
individuate possible worlds and therefore impossible to count them.
\cite{Lappin2015} takes up the representation problem for possible
worlds. If you cannot represent possible worlds then you cannot
individuate them.
The central problem for possible worlds as they are talked about in
the semantics literature seems to be that the intuitive way to
distinguish one possible world from another is to find a proposition
that is true in the first world but false in the second. This would
be fine except that we now have the corresponding problem for
propositions. Unfortunately the intuitive way of distinguishing
between one proposition and another (if you are a possible worlds
theorist) is to find a possible world in which the first proposition
is true and the other is false. This, of course, is circular and will
not give us an individuation of either possible worlds or
propositions. The standard version of possible worlds semantics as
proposed by Montague does not, of course, fall into this obvious trap.
Worlds are not represented in terms of sets of propositions which are
true in them. Rather we just define an interpretation to include
a set of possible worlds and leave aside the question of how they
have been individuated. In a sense it is fine from a technical
point of view to have an arbitrary set whose membership we cannot
represent as a central component of our semantic theory. But it
leaves us with the suspicion that we are left with an abstract theory
which we do not really know how to connect to any empirical
observations of the world. If you take a mathematical view of the
semantic enterprise as Montague did, this may be acceptable. But if
you are interested in semantics as an aspect of human cognitive
ability it can appear problematic. Traditional possible world
semantics is a theory based on an assumed set of possible worlds. But
it is not a theory of the possible worlds as such, beyond the claim
that there is a set of them.
Despite this, there is an intuition about the set of possible worlds
which possible world theorists hold onto: that they represent all the
logical possibilities. This, at least, gives us a way of considering
the required cardinality of the set of possible worlds. The issue of
the cardinality of the set of possible worlds and its relationship to
a psychological theory of language is something that is already taken
up by \cite{Partee1977}. Here she refers to Lewis's
(\citeyear{Lewis1973}) argument that there must be at least $\beth_2$
(the cardinality of the power set of the power set of natural numbers)
possible worlds. The argument\footnote{which I first heard from
Barbara Partee but for which I cannot find a published reference} goes like this: suppose we have a
family that goes on for ever. That is, there would be $\aleph_0$
members of the family. Now consider that in a logically possible
world (though possibly not in biologically possible worlds) any subset
of these family members might have blue eyes (none of them, all of
them and all the possibilities in between). This gives us a set of
possible worlds whose cardinality is the same as the power set of the
natural numbers $2^{\aleph_0}$ or $\beth_1$, that is, the cardinality of the set of real numbers.
Now consider the logical possibility that each of those possible
worlds is biologically plausible. Again, logically speaking, any subset
of those worlds could be biologically plausible. This will yield a set of possible worlds
of cardinality $2^{2^{\aleph_0}}$ or $\beth_2$. In principle one
could create sets of possible worlds of any of the infinitely many
infinite cardinalities although as Lewis claims $\beth_2$ is probably
sufficient for normal purposes.
Another argument for the uncountability of the set of possible worlds
comes from usual assumptions about space and time. We normally assume
that the set of moments of time has the same cardinality as the
set of points on the real line, that is, that time is continuous.
Similarly we also assume that space is continuous. Now
for any possible world where an object is at a certain location at a
certain time there is another logically possible world where that
object is located at a different location or occupies its location in
the first world at a different time. For each such world
there are uncountably many different logically possible worlds in
which the object is located elsewhere.
How do we manage to reason about such large numbers of possibilities?
The answer we want to propose here is that we reason in terms of
types. A single type has a set of witnesses and there are no
constraints on the cardinality of the set of witnesses. Types which
have infinitely many witnesses are not more complex than types which
have a small finite number of witnesses. Reasoning with a type
involves manipulating the structural object which is the type itself
not the set of its witnesses. Thus, for example, reasoning with a
record type may be more complex than reasoning with a basic type that
has no components. But still a record type is always a finite
structure and so we are not entering into the complexity of
manipulating uncountable sets, even though the record type may be
thought of as a ``representation'' for its set of witnesses which may
indeed be an uncountable set. Here our approach connects
with proof theoretic approaches. In proof theory we manipulate
expressions in a language which may represent sets of objects. Our
types are not expressions in a language but they are objects in our
type theoretic universe which could be thought of as ``representing''
the set of their witnesses. This approach also makes it possible to have a
learning theory where agents can be acquainted with a type without
being acquainted with the complete set of its witnesses. Knowing a
type whose witnesses are dogs does not mean that you are acquainted
with the set of all dogs, but rather that you know a dog when you see
one, that is, you have a reliable dog \textit{classifier}. (See
\citealp{Larsson2013} for a discussion of the relationship between types
and classifiers.) An important aspect of human cognitive processing is
that it involves reasoning with the types themselves, treating them as
first class citizens which can be arguments to predicates. This is
what gives rise to modality and intensionality. Possibly this higher
level reasoning is unique, or, at least, most fully developed, in
humans.
We think of types like record types as being types of
situations. If we want to keep to the idea of possible worlds as
total universes it is straightforward to convert a type of situations, $T$,
to a type of worlds, $T^W$, as long as we have a way of defining
worlds as maximal situations. We could say that a world, $w$, is of
type $T^W$ just in case some part, $s$ of $w$ is of type $T$.
Actually, we do not need to do this because of the way we have set up
subtyping. If $T$ is a record type and $s:T$, then if $s<s'$, that is
$s$ is a proper part of $s'$ in the sense defined in
Chapter~\ref{ch:commonnouns}, then $s':T$. If we had a way of
defining maximal situations, that is, situations $s$ such that there
is no $s'$ such that $s<s'$, we could take these to be our worlds.
The problem is, though that it
is not clear that it is desirable, or even possible, to characterize a
notion of maximal situation in this sense. Certainly, there is no
notion of maximal record so our choice of modelling situations as
records suggests that there is no notion of maximal situation. Our axioms say that given any record it is
always possible to add a new field to it.\footnote{This fact is
parallel to Proposition 2 in \cite{Barwise1989}, Ch. 8:
\textit{Every situation, $s$, is a proper part of some other
situation, $s'$}.}
\section{Modal type systems}%\todo{Moved from Ch. 1. Needs integrating}
\label{sec:percint-modal}
Let us develop further the story about Kim's walk in the park from
Chapter~\ref{ch:infex}. Kim continues her walk still thinking about
the boy and the dog whom she had seen playing the game of fetch. She
thinks, ``Was
the boy standing too close to the pond? Suppose he had fallen in. If
he had been my son, I wouldn't have let him play just there.'' An
important aspect of human cognition is that we are not only able to
observe things as they are but also to conceive of alternatives which
go beyond the completion of observed events in the way discussed in
Chapter~\ref{ch:infex},
Section~\ref{sec:ev-strings}. We can not only observe objects and
perceive them to be of certain types we can also consider
possibilities in which they belong to different types and perhaps do
not belong to the type we have observed. We have managed to unhook
type judgements from direct perception. While the seeds of this
ability can be seen in the kind of event perception and prediction
discussed in Chapter~\ref{ch:infex} in that it gives us a way to consider types which have
not yet been realized, it is at least one step further in cognitive
evolution to be able to consider alternative type assignments which do
not correspond to completions of events already perceived.
% While perception and typing are at the core of cognitive processing an
% important feature of cognitive systems is the ability to consider
% alternative typings which have not be observed.
% While we perceive $a$ to
% be of type $T_1$ it is perhaps nevertheless conceivable that $a$ could
% have been of type $T_2$.
This leads us to construct \textit{modal type
systems} with alternative assignments of objects to
types.\footnote{The term \textit{modal} is taken from modal logic. See
\cite{HughesCresswel1968} for a classic introduction. A modern
introduction is to be found in \cite{BlackburnRijkeVenema2001}.}
Figure~\ref{fig:modal} provides an example of a modal system of basic
types with two
possibilities, one where the extensions of types $T_1$ and $T_2$
overlap and another possibility where they do not.
\begin{figure}[h]
%\includegraphics[width=\textwidth]{modal}
\begin{adjustbox}{max width=\textwidth}
\begin{tikzpicture}[
type/.style={circle, inner sep=0pt, minimum size=6pt, ball color=BTypeCol},
firsttype/.style={circle, inner sep=0pt, minimum size=6pt, ball color=FirstTypeCol},
secondtype/.style={circle, inner sep=0pt, minimum size=6pt, ball color=SecondTypeCol},
objects/.style={circle, inner sep=0pt, minimum size=6pt, ball color=ObjectCol},
modalobjects/.style={circle, inner sep=0pt, minimum size=6pt, ball color=ModalCol}
]
% basic types:
\begin{scope}[
% every node/.append style={yslant=0,xslant=1.75},
yslant=0,xslant=1.75
]
\filldraw [fill=BTypeCol, draw=BorderCol, thick, fill opacity=0.5] (0,0) rectangle (8,2);
\foreach \x/\y in {0.5/1.3, 1.4/1.6, 1.8/1.3, 1.9/0.5, 3.3/1.8, 2.6/1.5, 4.4/0.9, 4.7/1, 5.5/0.3, 5.6/1.1, 5.5/1.7, 6.4/1.2, 6.7/1.6} {
\node [type] at (\x,\y) {};
}
\node [coordinate] (btypeleft) at (0,1) {};
\node [coordinate] (btyperight) at (8,1) {};
\node [type, label=above:$T_1$] (t1) at (1.3,0.6) {};
\node [type, label=above:$T_2$] (t2) at (4.5,0.5) {};
\end{scope}
% objects:
\begin{scope}[
% every node/.append style={yslant=0,xslant=1.75},
%yslant=0,xslant=1.75,
yshift=-100
]
\filldraw [fill=ObjectCol, opacity=0.4, draw=BorderCol, ultra thick] (5,0) ellipse (6 and 1);
\foreach \a/\b in {5.5/0.7, 6.4/0.2, 6.7/0.6, 7/0, 7.5/0.35, 8/-0.3, 8.1/0.2, 8.7/0, 9/0.2, 10/0.1} {
\node [objects] at (\a,\b) {};
}
% for T1 from BType:
\node [modalobjects, label=above:$a$] (o1) at (0.3,-0.1) {};
\node [objects] (o2) at (1,0.35) {};
\node [objects] (o3) at (1.6,-0.2) {};
\node [ellipse, fit=(o1) (o2) (o3), yscale=0.7, draw=BTypeCol, thick, fill=BTypeCol, fill opacity=0.3] (fitA) {};
\draw [BTypeCol, thick] (t1) -- (fitA.east);
\draw [BTypeCol, thick] (t1) -- (fitA.west);
% for T2 from BType:
\node [objects] (o4) at (2.6,-0.5) {};
\node [objects] (o5) at (3.1,-0.5) {};
\node [objects] (o6) at (3.3,-0.1) {};
\node [ellipse, fit=(o3) (o4) (o5) (o6), yscale=0.7, draw=BTypeCol, thick, fill=BTypeCol, fill opacity=0.2] (fitB) {};
\draw [BTypeCol, thick] (t2) -- (fitB.east);
\draw [BTypeCol, thick] (t2) -- (fitB.west);
% % for T2 from Type1:
\node [objects] (o7) at (4,0.4) {};
\node [objects] (o8) at (4.4,0) {};
\node [objects] (o9) at (4.7,0.1) {};
% \node [ellipse, fit=(o3) (o4) (o5) (o6) (o7) (o8) (o9), yscale=0.6, xscale=0.9, draw=FirstTypeCol, thick, fill=FirstTypeCol, fill opacity=0.2] (fitC) {};
% % for T2 from Type2:
\node [objects] (o10) at (5.5,-0.3) {};
\node [objects] (o11) at (5.6,-0.1) {};
% \node [ellipse, fit=(o3) (o4) (o5) (o6) (o7) (o8) (o9) (o10) (o11), yscale=0.7, xscale=0.8, draw=SecondTypeCol, thick, fill=SecondTypeCol, fill opacity=0.2] (fitD) {};
\end{scope}
% modal types:
\begin{scope}[
% every node/.append style={yslant=0,xslant=1.75},
%yslant=0,xslant=1.75,
yshift=-35,
xshift=220
]
\filldraw [fill=ObjectCol, opacity=0.4, draw=BorderCol, ultra thick] (3.5,0) ellipse (4 and 0.75);
\foreach \a/\b in {0.3/-0.1, 1.5/-0.3, 3.9/0.2, 7/0} {
\node [objects] at (\a,\b) {};
}
\node [modalobjects, label=above:$a$] at (0.7,0) {};
\node [objects] (i1) at (5.7,-0.2) {};
\node [objects] (i2) at (6.1,0.3) {};
\node [objects] (i3) at (5,0) {};
\node [ellipse, fit=(i1) (i2) (i3), yscale=0.7, draw=BTypeCol,
thick, fill=BTypeCol, fill opacity=0.2] (fitAA) {};
\draw [BTypeCol, thick] (t2) -- (fitAA.north);
\draw [BTypeCol, thick] (t2) -- (fitAA.south west);
\node [objects] (i4) at (1.6,0.1) {};
\node [objects] (i5) at (2,0.2) {};
\node [modalobjects, label=above:$b$] (i6) at (2.5,-0.3) {};
\node [objects] (i7) at (2.7,0.35) {};
\node [ellipse, fit=(i4) (i5) (i6) (i7), yscale=0.7, xscale=1.1,
draw=BTypeCol, thick, fill=BTypeCol, fill opacity=0.2] (fitBB) {};
\draw [BTypeCol, thick] (t1) -- (fitBB.north);
\draw [BTypeCol, thick] (t1) -- (fitBB.south west);
\end{scope}
% % Type1:
% \begin{scope}[
% % every node/.append style={yslant=0,xslant=1.75},
% yslant=0,xslant=1.75,
% xshift=-100,
% yshift=80
% ]
% \filldraw [fill=FirstTypeCol, draw=BorderCol, thick, fill opacity=0.3] (0,0) rectangle (8,2);
% \node [coordinate] (firsttypeleft) at (0,1) {};
% \node [coordinate] (firsttyperight) at (8,1) {};
% \foreach \x/\y in {0.45/1.4, 1.4/1.6, 1.9/0.5, 3.3/1.8, 2.6/1.5, 4.7/1, 5.5/0.3, 5.6/1.1, 6.7/1.6} {
% \node [firsttype] at (\x,\y) {};
% }
% \node [firsttype, label=above:$T_1$] (ft1) at (1.8,1.1) {};
% \node [firsttype, label=above:$T_2$] (ft2) at (5.8,0.7) {};
% \node [firsttype, label=above:$T_3$] (ft3) at (6.4,1.2) {};
% \node [firsttype, label=above:{\textbf{Type$^1$}}] (ft) at (4,0.4) {};
% \draw [FirstTypeCol, thick] (ft) -- (btypeleft);
% \draw [FirstTypeCol, thick] (ft) -- (btyperight);
% \draw [FirstTypeCol, thick] (ft2) -- (fitC.east);
% \draw [FirstTypeCol, thick] (ft2) -- (fitC.west);
% \end{scope}
% % Type2:
% \begin{scope}[
% % every node/.append style={yslant=0,xslant=1.75},
% yslant=0,xslant=1.75,
% xshift=-200,
% yshift=160
% ]
% \filldraw [fill=SecondTypeCol, draw=BorderCol, thick, fill opacity=0.1] (0,0) rectangle (8,2);
% \foreach \x/\y in {1.4/1.6, 1.9/0.5, 3.2/1.5, 4.7/1, 5.4/1.2, 5.8/0.3, 6/0.3, 6.2/1.6} {
% \node [secondtype] at (\x,\y) {};
% }
% \node [secondtype, label=above:$T_1$] (st1) at (1.2,1) {};
% \node [secondtype, label=above:$T_2$] (st2) at (4.8,0.7) {};
% \node [secondtype, label=above:$T_3$] (st3) at (2.6,1.3) {};
% \node [secondtype, label=above:{\textbf{Type$^2$}}] (st) at (3.4,0.5) {};
% \draw [SecondTypeCol, thick] (st) -- (firsttypeleft);
% \draw [SecondTypeCol, thick] (st) -- (firsttyperight);
% \draw [SecondTypeCol, thick] (st2) -- (fitD.east);
% \draw [SecondTypeCol, thick] (st2) -- (fitD.west);
% \end{scope}
\end{tikzpicture}
\end{adjustbox}
\caption{Modal system of basic types}
\label{fig:modal}
\end{figure}
The object $a$ is
of type $T_1$ in the first possibility but not in the second
possibility. There is an object, $b$, of type $T_1$ in the second
possibility. $b$ does not exist at all in the first possibility.
In the
figure we just show two possibilities but our general definition in
Appendix~\ref{app:modal}, introduced in Chapter~\ref{ch:percint}, p.~\pageref{ex:modalsys-complex},
allows for there to be any number of possibilities, including
infinitely many.
% \begin{shaded}
% We start by characterizing a modal system of basic types in \nexteg{},
% repeated in Appendix~\ref{sec:basic}.
% \begin{ex}
% A \textit{modal system of basic types} is a family of
% pairs:
% \begin{display}
% \textbf{TYPE$_{\mathit{MB}}$} = $\langle${\bf Type},
% $A\rangle_{A\in\mathcal{A}}$
% \end{display}
% where:
% \begin{enumerate}
% \item $\mathcal{A}$ is a set of functions with domain \textbf{Type}
% \item for each $A\in\mathcal{A}$, $\langle${\bf Type}, $A\rangle$ is a
% system of basic types
% \end{enumerate}
% \label{ex:def-modal-basic-types}
% \end{ex}
% \end{shaded}
Given this apparatus we define four simple modal notions:
\begin{description}
\item[(necessary) equivalence] Two types are (necessarily) equivalent
just in case the extension of one type is identical with that of
the other type in all the possibilities. While the different
possibilities may provide different extensions for the types, it
will always be the case that in any given possibility the two types
will have the same extension.
\item[subtype] One type is a subtype of another just in case whatever
possibility you look at it is always the case that the extension of
the first type is a subset of the extension of the second. We can
also say that the first type ``entails'' the second, that is, any
object which is of the first type will also be of the second type,
no matter which possibility you are considering.
\item[necessity] The notion of necessity we characterize for a type
could be glossed as ``necessarily realized'' or ``necessarily
instantiated''. A type will be necessary just in case there is
something of the type in all the possibilities.
\item[possibility] This notion corresponds to ``possibly realized'' or
``possibly instantiated''. A type will be possible just in case
there is some possibility according to which it has a non-null
extension.
\end{description}
\begin{shaded}
These notions are made precise for modal systems of complex types in
\nexteg{} and (\ref{ex:inclusive-modal-notions}), repeated in Appendix~\ref{app:modal}. As a preliminary we
note that if
\begin{quote}
{\bf TYPE$_{\mathit{MC}}$} = $\langle${\bf Type}$_M$, {\bf BType},
$\langle$\textbf{PType}$_M$, {\bf Pred}, \textbf{ArgIndices}, {\it
Arity\/}$\rangle, M\rangle_{M\in\mathcal{M}}$
\end{quote}
is a modal system of complex types based
on $\mathcal{M}$, we shall use the notation {\bf
TYPE$_{\mathit{MC}_M}$} (where $M\in\mathcal{M}$) to refer to that
system of complex types in {\bf TYPE$_{\mathit{MC}}$} whose model is
$M$. Let \textbf{Type}$_{\mathit{MC}_{\mathit{restr}}}$ be
$\bigcap\limits_{M\in\mathcal{M}}\!\textbf{Type}_M$, the
``restrictive'' set of
types which occur in all possibilities, and \textbf{Type}$_{\mathit{MC}_{\mathit{incl}}}$ be
$\bigcup\limits_{M\in\mathcal{M}}\!\textbf{Type}_M$, the
``inclusive'' set of
types which occur in at least one possibility. Then we can define
modal notions either restrictively or inclusively (indicated by the
subscripts $r$ and $i$ respectively).
\begin{ex}
\textbf{restrictive modal notions}
\begin{subex}
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T_1$ \textit{is
(necessarily) equivalent$_r$
to} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
$T_1\approx_{\mathbf{TYPE_{\mathit{MC}}}}T_2$, iff for all
$M\in\mathcal{M}$, $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}=\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T_1$ \textit{is a subtype$_r$ of} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
$T_1\sqsubseteq_{\mathbf{TYPE_{\mathit{MC}}}}T_2$, iff for all
$M\in\mathcal{M}$, $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}\subseteq\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$
\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T$ \textit{is necessary$_r$ in} {\bf TYPE$_{\mathit{MC}}$} iff for all
$M\in\mathcal{M}$, \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$
\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{restr}}}$, $T$ \textit{is possible$_r$ in} {\bf TYPE$_{\mathit{MC}}$} iff for some
$M\in\mathcal{M}$, \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$
\end{subex}
\end{ex}
\begin{ex}
\textbf{inclusive modal notions}
\begin{subex}
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T_1$ \textit{is
(necessarily) equivalent$_i$
to} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
$T_1\approx_{\mathbf{TYPE_{\mathit{MC}}}}T_2$, iff for all
$M\in\mathcal{M}$, if $T_1$ and $T_2$ are members of
\textbf{Type}$_M$, then $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}=\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$
\item for any $T_1,T_2\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T_1$ \textit{is a subtype$_i$ of} $T_2$ \textit{in} {\bf TYPE$_{\mathit{MC}}$},
$T_1\sqsubseteq_{\mathbf{TYPE_{\mathit{MC}}}}T_2$, iff for all
$M\in\mathcal{M}$, if $T_1$ and $T_2$ are members of
\textbf{Type}$_M$, then $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_1\}\subseteq\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T_2\}$
\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T$ \textit{is necessary$_i$ in} {\bf TYPE$_{\mathit{MC}}$} iff for all
$M\in\mathcal{M}$, if $T\in$\textbf{Type}$_M$, then \\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$
\item for any $T\in\textbf{Type}_{\mathit{MC}_{\mathit{incl}}}$, $T$ \textit{is possible$_i$ in} {\bf TYPE$_{\mathit{MC}}$} iff for some
$M\in\mathcal{M}$, if $T\in$\textbf{Type}$_M$, then\\ $\{a\mid a:_{\mathbf{TYPE}_{\mathit{MC}_M}}T\}\not=\emptyset$
\end{subex}
\label{ex:inclusive-modal-notions}
\end{ex}
It is easy to see that if any of the restrictive definitions holds for
given types in a particular system then the corresponding inclusive
definition will also hold for those types in that system.
This can be recast in terms of our informal proof theoretic notation
where we use `$T\ \mathrm{true}$' to represent that $T$ has some
witness, `$T_1\sqsubseteq_rT_2$' (`$T_1\sqsubseteq_iT_2$') to
represent that $T_1$ is a restrictive (inclusive) subtype of $T_2$,
`$T_1\approx_rT_2$' (`$T_1\approx_iT_2$') to represent that $T_1$ is
restrictively (inclusively) equivalent to $T_2$, `$T\ \mathrm{nec}_r$'
(`$T\ \mathrm{nec}_i$') to represent that $T$ is restrictively
(inclusively) necessary and `$T\ \mathrm{poss}_r$' (`$T\
\mathrm{poss}_i$') to represent that $T$ is restrictively
(inclusively) possible. We give the restrictive notions in \nexteg{}.
\begin{ex}
\textbf{restrictive modal notions}
For $\mathcal{G}$ a modal system of complex types
\begin{subex}
\item
\begin{prooftree}
\hypo{[\Gamma\in\mathcal{G}]}
\ellipsis{}{\Gamma\vdash T_1\in\textbf{Type}}
\hypo{[\Gamma\in\mathcal{G}]}
\ellipsis{}{\Gamma\vdash T_2\in\textbf{Type}}
\hypo{[\Gamma\in\mathcal{G},\Gamma\vdash a:T_1]}
\ellipsis{}{\Gamma\vdash a:T_2}
\infer3{\mathcal{G}\vdash T_1\sqsubseteq_r T_2}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\mathcal{G}\vdash T_1\sqsubseteq_r T_2}
\hypo{\mathcal{G}\vdash T_2\sqsubseteq_r T_1}
\infer2{\mathcal{G}\vdash T_1\approx_r T_2}
\end{prooftree}
\item
\begin{prooftree}
\hypo{[\Gamma\in\mathcal{G}]}
\ellipsis{}{\Gamma\vdash T\in\textbf{Type}}
\hypo{[\Gamma\in\mathcal{G}]}
\ellipsis{}{\Gamma\vdash T\ \mathrm{true}}
\infer2{\mathcal{G}\vdash T\ \mathrm{nec}_r}
\end{prooftree}
\item
\begin{prooftree}
\hypo{[\Gamma\in\mathcal{G}]}
\ellipsis{}{\Gamma\vdash T\in\textbf{Type}}
\hypo{\Gamma'\in\mathcal{G}}
\hypo{\Gamma'\vdash a:T}
\infer3{\mathcal{G}\vdash T\ \mathrm{poss}_r}
\end{prooftree}
\end{subex}
\end{ex}
The inclusive notions are given in \nexteg{}.
\begin{ex}
\textbf{inclusive modal notions}
For $\mathcal{G}$ a modal system of complex types
\begin{subex}
\item
\begin{prooftree}
\hypo{[\Gamma\in\mathcal{G},\Gamma\vdash
T_1\in\textbf{Type},\Gamma\vdash
T_2\in\textbf{Type},\Gamma\vdash a:T_1]}
\ellipsis{}{\Gamma\vdash a:T_2}
\infer1{\mathcal{G}\vdash T_1\sqsubseteq_i T_2}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\mathcal{G}\vdash T_1\sqsubseteq_i T_2}
\hypo{\mathcal{G}\vdash T_2\sqsubseteq_i T_2}
\infer2{\mathcal{G}\vdash T_1\approx_i T_2}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\Gamma'\in\mathcal{G}}
\hypo{\Gamma'\vdash T\in\textbf{Type}}
\hypo{[\Gamma\in\mathcal{G},\Gamma\vdash T\in\textbf{Type}]}
\ellipsis{}{\Gamma\vdash T\ \mathrm{true}}
\infer3{\mathcal{G}\vdash T\ \mathrm{nec}_i}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\Gamma\in\mathcal{G}}
\hypo{\Gamma\vdash T\in\textbf{Type}}
\hypo{\Gamma\vdash a:T}
\infer3{\mathcal{G}\vdash T\ \mathrm{poss}_i}
\end{prooftree}
\end{subex}
\end{ex}
\end{shaded}
Note that
all of these notions are relativized to the modal system you are
considering and the possibilities it offers. We may think of the
family of assignments $\mathcal{A}$ as providing a modal base in the
sense of \cite{Kratzer2012}.
We may wish to consider very small families of
assignments corresponding to the knowledge we have. Alternatively, we
may want to consider strong logical variants of these modal notions
where we consider all the logical possibilities, for example, all
possible assignments of extensions to types.
% So far we have talked about modal systems of basic types. Modal
% systems of complex types, where we introduce ptypes, create a
% minor complication. What ptypes that are present in a system depends
% on what objects there are of the types that are used in the arities of
% the predicates. Thus if we have some predicate $r$ with arity
% $\langle\textit{Ind},\textit{Ind}\rangle$ and a possibility where the
% set assigned to \textit{Ind} is $\{a,b\}$ then according to that
% possibility the ptypes formed with $r$ will be $r(a,a)$, $r(a,b)$,
% $r(b,a)$ and $r(b,b)$. In a possibility where \textit{Ind} is
% assigned a different set the set of available ptypes will be
% different. It is an important feature of type theories with types
% constructed from predicates that the collection of such types depends
% on what objects are available as arguments to the predicates. This
% makes type theory very different from a logical language such as
% predicate calculus where the notion of well-formedness of syntactic
% expressions containing predicates is defined independently of what is
% provided by the model as denotations of arguments to the predicate.
% This leads us (in Appendix~\ref{app:modal}) to define two variants of
% each of our modal notions: \textit{restrictive} variants which are only defined
% for types which exist in all possibilities and \textit{inclusive}
% variants which require that the modal definition holds for all the
% possibilities in which the types exist and disregards those in which
% the types do not exist. For example, a type is \textit{necessary}$_r$
% (that is, ``restrictively necessary'') just in case the type is
% available in all possibilities and has a non-empty set of witnesses in
% all possibilities. It is \textit{necessary}$_i$ (``inclusively
% necessary'') just in case in all the possibilities in which the type
% is provided it has a non-empty set of witnesses. It is clear that if
% a type is necessary$_r$ it will also be necessary$_i$ but there may be
% types which are necessary$_i$ but not necessary$_r$ (if the type is
% not provided in all possibilities). A similar relationship between
% the restrictive and inclusive notions holds for all the modal notions
% we have discussed.
% There may be significant classes of modal type systems in which the
% types available in the different possibilities do not vary. This
% could be achieved by requiring that the types used in the arities of
% predicates always have the same witnesses in all the possibilities.
% This seems feasible if we restrict the types used in predicate arities
% to basic ontological categories such as individual or time point. It
% seems reasonable to consider modal systems in which an individual in
% one possibility will be an individual in any other possibility, for
% example. It seems reasonable to say that we wish to consider
% possibilities where, for example, Kim is a man rather than a woman,
% but not possibilities where Kim is a point in time rather than an
% individual. However, the notion ``basic ontological category'' is a
% slippery one and we do not want to be forced to make commitments about that.
% In the definition of a system of complex types in
% section~\ref{app:comptypes} we call the pair of an assignment to
% basic types and assignment to ptypes, $\langle A,F\rangle$, a \textit{model} because of its
% similarity to first order models.\footnote{For a more detailed
% discussion of the relationship between this and first order models
% as used in the interpretation of first order logic see
% \cite{Cooperforthcoming}.} The model provides an interface
% between
% the type theoretical system and a domain external to the type theory.
% The natural domain to relate to the type theory is that of individuals
% and situations, that is the kind of things we can perceive or at least
% consider as possibilities. However, we may want to use models which
% relate to our perceptual apparatus, as in \cite{Larsson2011}, rather
% than directly to the world. This can also be the key for relating the
% type theory to a dynamically changing world where the models
% representing our perceived possibilities are not fixed. % We will
% return to this in Chapter~\ref{ch:coord}.
\section{Modality without possible worlds}
\cite{Montague1973} introduces \textit{necessarily} and
\textit{possibly} as sentence adverbs, that is, they combine with a
sentence to produce another sentence. If $\alpha$ is a sentence, then
\textit{necessarily} $\alpha$ is true in a possible world, $w$, just in case $\alpha$ is true in
every possible world and \textit{possibly} $\alpha$ is true in a
possible world, $w$, just in case there is some possible world in
which $\alpha$ is true.\footnote{This simple treatment of modality
corresponds to the modal logic system S5 where there is no
restriction on accessibility between possible worlds
\citep{HughesCresswel1968,HughesCresswell1996}.}
In Chapter~\ref{ch:percint}, p.~\pageref{pg:modal-systems} and
Appendix~\ref{app:modal} we introduce modal type systems which are
families of type systems, which we call \textit{possibilities}, differing in their assignments of
witnesses to basic types and ptypes. The important difference between
possible worlds and possibilities is that for possibilities the
parameters along which they can vary are fixed by the available types
introduced in the type system, a well-defined notion, and one which
varies depending on the particular type system. Thus we have a way of
characterizing the dimensions along which the possibilities associated
with a given type system vary and thus we have a way of representing the
possibilities, whereas we do not have such a way of characterizing
possible worlds. Building on the modal notions that we introduced in
Section~\ref{sec:percint-modal} we can introduce type constructors `$\Box$' and `$\Diamond$' corresponding to the operators in modal
logic as
in \nexteg{}.
\begin{ex}
If $T$ is a type, then $\Box_r T$, $\Box_i T$, $\Diamond_r T$ and $\Diamond_i T$ are types
\end{ex}
These types obey the constraints in \nexteg{} which correspond to the
truth conditions for the corresponding operators in modal logic (S5).
\begin{ex}
\begin{subex}
\item $\Box_{r/i} T$ is non-empty iff $T$ is restrictively/inclusively
necessary (approximately, non-empty in all possibilities)
\item $\Diamond_{r/i} T$ is non-empty iff $T$ is
restrictively/inclusively possible (approximately, non-empty in some possibility)
\end{subex}
\label{ex:modalconds}
\end{ex}
\begin{shaded}
Making the witness conditions for these types meet the constraints in
\preveg{} is a little tricky. We do not have biconditionals, but two
conditionals which correspond to introduction and elimination rules in
proof theory. Suppose that $\mathbb{T}$ is a modal type system and
that $p\in\mathbb{T}$ is a possibility in $\mathbb{T}$. Then for
`$\Box_{r\i} T$ we have \nexteg{}.
\begin{ex}
\begin{subex}
\item If $a:_p\Box_{r/i}T$ then $T$ is necessary$_{r/i}$ in $\mathbb{T}$
\item If $T$ is necessary$_{r/i}$ in $\mathbb{T}$ then for any
$p'\in\mathbb{T}$ there is some $a'$ such that $a':_{p'}\Box_{r/i}T$
\end{subex}
\label{ex:witconds-Box}
\end{ex}
Note that the two clauses in \preveg{} jointly entail \nexteg{}.
\begin{ex}
For any $p'\in\mathbb{T}$ there is some $a'$ such that
$a':_{p'}\Box_{r/i}T$ (``$\Box_{r/i}T$ is true in $p'$'') iff $T$ is
necessary$_{r/i}$ in $\mathbb{T}$
\end{ex}
For `$\Diamond_{r/i}T$' we have \nexteg{}.
\begin{ex}
\begin{subex}
\item If $a:_p\Diamond_{r/i}T$ then $T$ is possible$_{r/i}$ in $\mathbb{T}$
\item If $T$ is possible$_{r/i}$ in $\mathbb{T}$ then for any $p'\in\mathbb{T}$ there is some $a'$ such that $a':_{p'}\Diamond_{r/i}T$
\end{subex}
\label{ex:witconds-Diamond}
\end{ex}
The two clauses in \preveg{} jointly entail \nexteg{}.
\begin{ex}
For any $p'\in\mathbb{T}$ there is some $a'$ such that
$a':_{p'}\Diamond_{r/i}T$ (``$\Diamond_{r/i}T$ is true in $p'$'') iff $T$ is
possible$_{r/i}$ in $\mathbb{T}$
\end{ex}
We can recreate the witness conditions in (\ref{ex:witconds-Box}) and
(\ref{ex:witconds-Diamond}) in our informal proof theoretic
representation as in \nexteg{} where we use $\mathcal{G}\vdash T\text{
nec/poss}_{r/i}$ to represent $T$ is necessary/possible$_{r/i}$ in $\mathcal{G}$.
\begin{ex}
For $\mathcal{G}$ a modal system of complex types:
\begin{subex}
\item
\begin{prooftree}
\hypo{\Gamma\in\mathcal{G}}
\hypo{\Gamma\vdash a:\Box_{r/i} T}
\infer2{\mathcal{G}\vdash T\text{ nec}_{r/i}}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\mathcal{G}\vdash T\text{ nec}_{r/i}}
\hypo{\Gamma\in\mathcal{G}}
\infer2{\Gamma\vdash\Box_{r/i}T\text{ true}}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\Gamma\in\mathcal{G}}
\hypo{\Gamma\vdash a:\Diamond_{r/i} T}
\infer2{\mathcal{G}\vdash T\text{ poss}_{r/i}}
\end{prooftree}
\item
\begin{prooftree}
\hypo{\mathcal{G}\vdash T\text{ poss}_{r/i}}
\hypo{\Gamma\in\mathcal{G}}
\infer2{\Gamma\vdash\Diamond_{r/i}T\text{ true}}
\end{prooftree}
\end{subex}
\end{ex}
\end{shaded}
This shows how we can, if we want to, recreate in TTR the simple S5 modal
system (that is, where all possibilities are accessible to each other)
that \cite{Montague1973} uses.
% In order to see how we can meet these constraints we have to first
% note that in a modal type system we cannot talk of an object $a$ being
% of a type $T$ \textit{tout court} as we have done so far. $a$ may be
% of type $T$ in some possibilities but not others. This means that we
% have to relativize being of a type to possibilities,
% $p$ which are members of a modal type system, $\mathcal{P}$. Instead of writing $a:T$, we will write $a:_{p,\mathcal{P}} T$ (``$a$ is of
% type $T$ in possibility $p$ within modal type system $\mathcal{P}$'').\footnote{Note that in Appendix~\ref{app:ttr} we have throughout
% the formal development of TTR always relativized the of-type
% relation to the type system being considered, and in the case of
% modal type systems in addition to the possibility (identified by the
% model associated with the possibility).} We also correspondingly
% relativize our notation for the set of witnesses of a type as in
% \nexteg{}.
% \begin{ex}
% $\down{T}_{p,\mathcal{P}} = \{a\mid a:_{p,\mathcal{P}}T\}$
% \end{ex}
% We introduce two basic types of types, \textit{Nec} and \textit{Poss},
% the types of necessary and possible propositions respectively. The
% witness conditions for these types are given in
% \nexteg{}.\footnote{Note that it is important for these types that we
% have introduced stratified types (Appendix~\ref{app:int}) since
% \textit{Nec} and \textit{Poss} can themselves be necessary and
% possible types. For example, instead of \textit{Nec}
% :$_{p,\mathcal{P}}$ \textit{Nec} we have \mbox{\textit{Nec}$^n$
% :$_{p,\mathcal{P}}$ \textit{Nec}$^{n+1}$} to avoid the danger of
% running into a version of Russell's paradox. As usual we will
% suppress discussion of stratification in the text in order to
% simplify the presentation.}
% \begin{ex}
% \begin{subex}
% \item $T:_{p,\mathcal{P}}$ \textit{Nec} iff for all
% $p'\in\mathcal{P}$, $\down{T}_{p',\mathcal{P}}\not=\emptyset$
% \item $T:_{p,\mathcal{P}}$ \textit{Poss} iff for some
% $p'\in\mathcal{P}$, $\down{T}_{p',\mathcal{P}}\not=\emptyset$
% \end{subex}
% \end{ex}
% Now consider that the inclusion of singleton types in our system
% (Appendix~\ref{app:singletontypes}) allows for the types
% \textit{Nec}$_T$ and \textit{Poss}$_T$ for any type, $T$. These types
% have a single witness, $T$, if $T$ is necessary or possible
% respectively and otherwise have no witnesses. These types thus meet
% the constraints on $\Box T$ and $\Diamond T$ given in
% (\ref{ex:modalconds}). We propose therefore to make the
% identifications given in \nexteg{}.
% \begin{ex}
% \begin{subex}
% \item $\Box T = \textit{Nec}_T$
% \item $\Diamond T = \textit{Poss}_T$
% \end{subex}
% \end{ex}
We have used the symbols `$\Box$' and `$\Diamond$' above to suggest
the relationship between our proposal in terms of types and the
traditional formulas of modal logic. We could, however, have achieved
the same effect as above by introducing predicates `nec$_{r/i}$' and `poss$_{r/i}$'
with arity
$\langle$\textit{Type}$\rangle$ and giving ptypes of the form
`nec$_{r/i}(T)$' and `poss$_{r/i}(T)$' the same witness conditions as
above. % which obey the constraints in
% \nexteg{}.
% \begin{ex}
% \begin{subex}
%
% \item $\down{\text{nec}(T)} \not=\emptyset$ iff $T$ : \textit{Nec}
%
% \item $\down{\text{poss}(T)} \not=\emptyset$ iff $T$ : \textit{Poss}
%
% \end{subex}
%
% \end{ex}
We will pursue this option below where we will add additional arguments to the predicate.
How many possibilities are there in a modal type system? The answer
to this question is that there can be as many as you choose for the
given type system, ranging from a small finite number of possibilities
to a higher order infinity. The definition of a modal type system
given in Appendix~\ref{app:modal} only requires that there be a family
of possibilities. Thus this definition includes the kind of
restricted sets of ``possible worlds'' differing along a small finite
set of parameters which probability theorists talk of and indeed also
linguistic semanticists talk of informally when they are in pedagogical
explanatory mode (see, for example, \citealp{DowtyWallPeters1981} and
a lot of recent literature on inquisitive semantics such as
\citealp{GroenendijkRoelofsen2012}).
It is important in a modal type system that the identity criteria for
the possibilities are determined by the types provided by the system.
Two possibilities are distinct only if they differ in the witnesses
associated with some basic type or ptype. It is not possible to make
distinctions for which you do not have appropriate types available.
Thus the range of possibilities is limited by the types which are
available to classify objects.
This is not to say that we have eliminated all potential decidability
problems from modal type systems. Of course, if the types that we use
to construct the system are not decidable it may not be possible to
decide on identity for possibilities. Even if all the types are
guaranteed to be decidable, given an inifinite
set of possibilities there cannot be any general guarantee that we can
decide whether an arbitrary type is necessary or possible or not since
we cannot visit every possibility in a finite amount of time. We can
only be sure if we have some general argument about the
possibilities which does not involve inspecting each possibility
individually. But having a way of distinguishing between
possibilities which may in the limit be undecidable is better than not
having a way of distinguishing between possibilities, other than that
they are distinct members of a set.
The work on modality in natural language which has followed after
Montague's original work all points to a more restricted kind of
modality which involves arguing from some basic assumptions to a
conclusion rather than considering all logical possibilities. This
view of modality in natural language has been put forward by Kratzer
in a body of work beginning with \cite{Kratzer1977}. This and other
papers by Kratzer on modality are collected in revised and commented
form in \cite{Kratzer2012} and there is much other literature which
builds on Kratzer's ideas. An excellent introduction to Kratzer's
work is given in Chapter~3 of \cite{Portner2009}. The essential idea is that modals like
\textit{must} (corresponding to necessity) and \textit{can}
(corresponding to possibility) must be interpreted relative to a
``conversational background'' which in \cite{Kratzer1981} (Chapter~2
of \citealp{Kratzer2012}) is split into two components, a \textit{modal base} and an
\textit{ordering source}. The modal base is a set of
propositions\footnote{Actually, a function which determines a set of
propositions for each possible world.} which characterize the
assumptions from which we are arguing. The ordering source is a set of
propositions\footnote{Again relativized to possible worlds.} which determine an ideal which we are trying to get as
close to as possible. It is called an ordering source because
Kratzer, following \cite{Lewis1981}, thinks of it as inducing a
partial ordering on possible worlds, in terms of their closeness to
the ideal. Kratzer's insight is that necessity and possibility in
natural language should be defined relative to a modal base and an
ordering source. In simple terms, a proposition, $p$, is necessary with
respect to a modal base, $b$, and an ordering source (ideal), $i$,
just in case $p$
follows from the conjunction of $b$ and $i$. A proposition, $p$, is