modal logic for philosophers

It names systems by listing their axioms. /MediaBox [ 0 0 432 720 ] nV;?=rX>^A&u+Hp2o)s4e@g6=0f:V'r^o:TNG"1N(C12J*gdE<0_EaT9HWAa-NYL( endobj &Un ). 9fr&5P.[pR#APsC3KC*X[%hFG6]'"\l%]0W*o#EF4[X]@(g? /URI (http://www.cambridge.org/0521682290) Let M1 be the set M, and consider the first sentence A1 . So the argument ∫(pçq) / ~∫qç~∫p has no counterexample, and so must be K-valid. 7Qf9HMeP;kIJ'^Lit9Ol`j[X$f_%u ?+W0hFgHP1?>n";,U!&c;6Y@9o(sXq`1Jj7Ql$QVL^>f5o1 endobj Many concepts in philosophy of language can be formalized in modal logic. >> *#PZE>"9f*W^`8rkjOIXIE(sH\L8LX]+j1S?h@i%?f8e_JBHMng&CVT ;#h&_#;uEF,A%07& /Annots 171 0 R /Flags 34 /Type /Font e:!hk^marn"IVEH]9Ycq=:0bBege`EJ^#&oL8M;P4[oF>_fsATKr=Cg/Dr,aFd?r3 /Rect [ 335.75236 13.1887 416.84317 26.40011 ] In order to prove ∫pç∫q, enter ~(∫pç∫q) as a new hypotheses for Indirect Proof. So the primary issue to be faced in the conversion process for systems stronger than K is to show how these additional steps in the tree can be proven. stream 4nF'"dliH0#J`JkaTBM'!`TJ6^eoEqWA.? &Un ))=T. << /Count 9 endobj >> 193 0 obj 121 0 obj ] 659 :lJp6Ju&p3j- Lemmon, E., and Scott, D. (1977) The ‘Lemmon Notes’: An Introduction to Modal Logic, Basil Blackwell, Oxford. /H /I b) Show that (∂F) follows from (), (~), and (Def∂) using diagrams. endobj /MediaBox [ 0 0 432 720 ] [[r /Type /ExtGState The basic idea is that to show that whenever an argument H / C has an S-counterexample, then it also has another S-counterexample in a model with a finite frame, that is, one where there is a finite number of possible worlds in W. When this occurs, we say that S has the finite model property. B#Xqc_o__[+*5+3&O[Js)cl"% Zu2":].7+H9(p4b5MeT[]km_YhL;uJ]KC\L%nf.q2SG*fI=HPAo_IbFoB3`D9K<66 /BG2 /Default ^O`)uBaDdlV$UlA!HSp8oB\`dj/"_*nWd+3/4%0"`Ym^TY9X%Vq+N-UP(b=,;\FW6 hbN&K2T$8G%J1Bh2b1J`%,'=DZ%nR_);JZp(_Q+C\,GXYleD$`rU'4L_)@7WmIu-% 'hJ)H#C[gaatA%5tMpb^t+:B[q3gi ,]!0eK(aE`Jku%J3Lluj5*l!+_$:^8@\h;JI7Vd7L@O4hE:CNXj0Ml1_N_2Fh#!H8 /D [ 170 0 R /Fit ] endobj U7JNV,(larQ^a83pt(lO?T! 7HtC3$i9"je@/>,:hg'p,c? << ]cmT;@E(1W!6alulZaJ+pX.2.,C8eC[s1=2&H4*((mki+]EH.iN.N]t#O\l+7Uu g'r>XE6)s9S5Gol739gYs*nDNdYfdCja:Ffo;\_mB(t0KIXKO8h:c`:D@8AlD;1"u /i0rBa8q/MYs.(U,H[[nTBks>1"@A8j*?9\adZraktXV%Fu9! Let M be any finite set, and suppose that M∪M ÷ L Ó ~t≈c for every constant c of the language. 8oOj"TeQ6o>d8])"j.];R&V:Z8Ld^Qnnr0#:a=A]!h@io$dEJ2! We are now ready 68 Modal Logic for Philosophers to give this definition for a generic intensional operator . /Annots 42 0 R Jk829kM,FnIarYLIFkKZ=^MZ,LHAMfhVe2'M5;Xm?ZrQ#GL!W!D6!mGCYJ4-G+T=k We will give the proof in one direction using diagrams and leave the other direction as an exercise. /UCR2 /Default >> For example, suppose A is proven in a subproof headed by ∫: This means that ∫A has been proven outside that subproof. e6t$s9,&fJAH3BQL]u+5VY`%8:;;!-I?7MH(YLcsrtar>;r"RO`E%!S67_k/S/,8,COme2CtWSt2HlRCP7eSG It should be obvious that once the (4)K-tree for an argument is closed, it is a straightforward matter to convert the result into a proof. In the next example, we present the corresponding proof for the tree of the argument ~pç∫~∫~~p / ~∫~∫pçp. endobj -O154H14H;$Ab4KmF$uWN/5F.8V&!86Bi2&-\KN-hD2bIHBFqq5/"J"jFiiJFXBl8P].7@^)>tD*9;P_SW2qU-FhUY1GWr7.XHUr The best way to master this material is to struggle through the exercises on your own as far as humanly possible. endobj (G2,/l<4O8Kp/k*:?MBq?XBjdEB%6] /Flags 70 So to show that such an argument must be K-valid, we assume that L, A / A has a K-counterexample, and derive a contradiction. HO:d/(ZUhAQie21VJ#)W'9YKGnhLp+f#YUu2pOOTBWgn&$i]"NhuC(GeneZAo]H/# 190 0 obj mR.dq@q2Enfs%&qPC;HXh$+G\53>DgDD3no] The completeness proof given here can be used to show that the tree method serves as a decision procedure for many of the systems discussed in Chapter 7. It follows immediately by (IP) that the argument has a proof in K. To construct *B, *w is defined for each world w on a branch as follows: Definition of *w. *w is the conjunction of all sentences appearing in w on the branch (including sentences in any continuations of w) together with ∂*v, for each world v on the branch such that there is an arrow from w to v. *B for a branch B is then defined to be *o, where o is the opening world on the branch, that is, the one at the top of the tree. To show V, ~A is a ≈-set, assume V, ~A ÷ L Ó t≈c for all c, and show that V, ~A ÷ LÓ~t≈t as follows. If At is a sentence, and x is a variable, then !xAx is a term and ¬xAx is a predicate. So aw (c) µ Dw. ÷A ------÷ ∫A ÷ ∫(AçB)ç(∫Aç∫B) (Dist) (Nec) The rule of Necessitation may appear to be incorrect. /Subtype /Link Let us use the notation ‘(M∫T)’ to record the idea that this step was applied because of the presence of the M-arrow in this tree. /Parent 166 0 R /Thumb 232 0 R So it appears we must reject (GN) since it leads us from a valid to an invalid argument. By the truth condition (ç), aw (BçC)=F and so aw (~(BçC))=T by (~). 205 0 obj /A 92 0 R 210 Modal Logic for Philosophers EXERCISE 9.11 (Difficult Project) The basic provability logic GL results from adding axiom (GL) to K. (GL) ∫(∫AçA)ç∫A A corresponding condition on frames for GL-validity is that the frame be transitive, finite and irreflexive. 1/^M>>baoSMJH0BWDd"9959dB.>)U)-[!5bi/M"ICel5$m,M:0CjE%o_s?I`k]qu3 !Q43cAm8["R%e0BGX_r$T"VG Since u is closed, it follows that au (~∫A)=T. endobj &^?A6F`m9f\95\VkhmLpL4iD+?UeJlQIj'+c^B&RqT#YgaPn92%1F96i^Gsb-1Mqj 673 Since (ƒD) constitutes a derived principle in D, converting a (D)K-tree into a proof in D is straightforward. The semantics for a logic gives a formal account of which arguments are the valid ones. << ;Nn7l$>dmZP+0<7"K#TUJS@A+Zg)VX(p#NU6/T'tHqfhu:\Gc##[scn(hu!P2 3.3. /TR2 /Default Ahr#H.9J>PIR3##BkXa^(u'7MJ0'ff#0c;H'H6#r)hTfu@s]O]cM4KTin243j/:2F /Widths [ 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 1000 However, we have just found out that the axiom corresponds to a perfectly acceptable condition on the relationship between earlier than and later than. //hrDS$FTHTUG:J/G]lsltg=Y>0H(Nd6p+##7`Q.houC83@tk$oV0'X\f&7K9TG<< 156 0 obj RZsR,"_uhCW;lE%T]NBlHW9%I/A>nmIq-qMU-R`e+S$ZW*abYWQY(tACP3d?B. /Type /Encoding Proof of (¬). GcE:h"ci0;7t8,$"+T`hjotZjb'39IN? @Zp;.ge;R#L,T)Ae_./p_pE^WTquVgo4!f<>(Z:JhO*`qa*,_456:?%2dAgT-OWEB But in K-trees, the introduction of new arrows and worlds by (∫F) guarantees that no more than one arrow points to a world. (Hint: Use the solution to Exercise 2.1a for one direction, and use 2.3b for the other.) (B) says that if A is the case, then A is necessarily possible. Each of these logics uses its own symbols for the expressions it governs. /FontDescriptor 198 0 R 8;U;C9i&Y\%)(h*p^#RsD:Xak7?tjmBa6i?#59Zk7jXTnBm84Ea%iK4Q. >> 130 0 obj 3.6. /H /I We leave the justifications for the lines of this proof as an exercise. So the only thing that remains for the proof of completeness is to show that the canonical model’s frame obeys the properties corresponding to system S. For example, when S is system M, then we must show R is reflexive. stream endobj So R2 is RoR, and R4 is RoRoRoR. 653 653 653 653 390 390 390 390 749 767 744 744 744 744 744 643 /Border [ 0 0 0 ] /FontBBox [ -170 -240 996 935 ] (NM",G These and othe… 250 250 250 250 500 556 444 556 444 333 500 556 278 250 556 278 /Title (6 x 10 Long.P65) To show this, consider the arrows from v to u and u to x. GNMCpp>\(=$so*\f$E8F+6/%eDX+otOp`WR96f(H4EH6i#GiY$T%/a/bgReX\HR&L >> endobj /FontFile3 147 0 R :"u'CJ_@BkTgD6 =ZOaBGUSAfHl^(c"dQ.c)CIZ=FJ2mAi/1j>[!hOr/!kkuR"c4! ?1_)9-9gDTiI#;Y4t^F%T3QtRqSpi!T00j*FdfAVot(M2'D>,pX(8nScn3tReQqC1 Garson, J. H>PV/-3o#&3XG\]Dt^G!`2Q\p"FB#)l-7KHmeQh;Ac)#niUOSZqL%+JqXA`TIX1qk << /FontStretch /Normal . YPM%aI^n.9*q$dD/*[E;kCrZR@K1+?q77q:B-i,AWR^4X$K@3ZCYut_DRqL!^,t<9 What has gone wrong? Th6bZZ(ha4/#9sVeYM,`6\4-e`YCh,`k(AbF'f1mg"JaI/-IVk)AV%o(.j]IVYDS! >> Explain why this method is not a general solution to converting KB-trees to proofs. We have now found a mc set v with the feature that wRv and v ¿ A, which finishes the proof of (∫¿). :7Q'640:Ll3;Q+o%ZnW\:U+IO^>CFEGQds4?qCNLg[7N64 Clearly the resulting (4)K-tree can be converted into a proof with the help of (4). endobj EV79Nk8IE:ce%:AjmMWKgXenK/OPFV /Contents 98 0 R P\F>i_OhJXo1/fP.=%t&V].cN7I+cmq_ulVKSqd`%D`W/r7V=9O1q"Zjs6Ll'Db5q "q7#4&Q! W@+WqAAF\$+H4u(,W!uJEjMG@Bf&$D!.9D:9_r3#@FXL@arRe#pJA=BRHh%*j;L`. , ∫Un )=T. . ?o"Ccdmfh5qBAF]_s4C89uA(UCt9+H&-bV[+;?Ph0! 738 It seems that for an essentialist theory, the only way out, given that John is not necessarily two-legged, is to deny (3). EXERCISE 10.3 Derive diagrams for (M), (C4), and (CD) by setting values for h, i, j, and k in the diagram for hijk-convergence, and then resolving the arrows. 8)AiIYbRr_VX! e."-#/XTsN7? >> .X&n4F_j@;+"3<7MHU6jn\o%VgE]Xt'FF/O)MOHh1_Yp)XJmI=*&4mOg/Q8d-oV]: If we try to create a 4-counterexample to this sentence by drawing the missing arrow from w to u in order to ensure that R is transitive, the tree closes. << So ∂∫AçA should be acceptable if (B) is. First, consider what (ç) tells us when aw (AçB)=F. (Y+]5Me7S;4DIOUZpbED-rJjpio78,t][7 Bibliography of Works Cited 447 Kripke, S. (1963) “Semantical Considerations in Modal Logic,” Acta Philosophica Fennica, 16, 83–94. See intensional model iteration of modal operators, 39, 49 K, 18 Kaplan, D., 428 K-counterexample, 68 K-model, 64 Kripke relation. Exercise 9.3 Suppose wRv and av (A)=T. /S /URI 99 0 obj >> 8;VGQCK(s[)TQIr1G;oj].t`T9QVV+^AoI\/-nb((N.C,'"9?6W?=JOQN..j1b_OF6r878K 667 500 1068 500 500 549 500 500 500 500 500 500 500 500 500 500 )_WZ:6*p "sk(fM*h-(&9I6-4gXu:[a.9FaG=$HeCQTCk!`&+nHBg9JT<47_Npen^]k9( endobj JV'+\$n3D%#Ft;=/mU-P%bs=s%2#upMQdXm$B@GH!r7X!8HYb$$uM/_S'8D!9J^tI 9"JnFgOoG! This means the opening segment in world v remains open, leaving the branch in world w open as well. lcc��[��\��~��E��3� BB#hK,1brB=A2`1`t1,!\sfbp(HrHEQ52'Q.LI$.fskLB:f,[W5[d*L_XbcT+BLR( To complete the proof, (Rk+1 ) must be shown from right to left given (Rk ). /Ascent 0 Fact 2. endobj In the argument we just checked, ~, ç, and ∫ were the only logical symbols. << << �,*�5#\s��]�@�p}�ۇ�uD��K�V3$��x��鼅�SP�:�M�G7��W�AɈ�"N|j{v7M�3�dg��O�w$��ާ�n��(Z{N�� ;_��=B�� << endstream /FontBBox [ -173 -217 1167 912 ] R is clearly a binary relation on W. W is nonempty by the following reasoning. But if A is verified regardless of size, then it follows that every sentence is verified, and this will prove the theorem. Filtration is a technique that allows one to reduce an S-counterexample for an argument H / C, by collapsing together into one world all those worlds that agree on the values of sentences that appear in H / C (including sentences that appear as parts of other sentences). @2Zb)lBi[gfEdWKch\Ce_/@aUq(Y%qYD?TGWB,= To guarantee uniqueness, we will need to modify the (∫F) rule as follows. For example, when Ax is ∫x>7 and t is !xNx, the principle of abstraction asserts that the de re and de dicto translations of the conclusion of the ‘planets’ argument are equivalent. geV#es8>+nkWW?V7N[Dgg._!)."PbDepkfB2-hmq+U3-C1:Z@Pkf+QC$*8F'"U*,! << endstream G(t_V-B,t2/m8&2R9IEaJ& Modal Logic for Philosophers Designed for use by philosophy students, this book provides an accessible yet technically sound treatment of modal logic and its philosophical applications. /Type /Encoding ?JI]ZjDI>751-"2=SU;`@A9t'ah94R];*'&\T@2q$3IC%eqFp$&S"'_,\s1F,6\-bO@2&J KD0?191:nCK8WpV>9A.$#Ul^0-[7#cHuGcY. /Kids [ 165 0 R 166 0 R ] endstream ? C_9_u8rF':0#aYM;hlFW\55WL.T3=+e>_#q[c.cXpH]P%Flo2SBBIF+pWbqjrVuia G]H6_5Z.gtA/H5TO2mo`:B`&$Ph_UV*>h.48ed=H6Os>-gA+_/\0*q(hb\oZ8?Bh! The book uses natural deduction systems and includes a diagram technique that extends the method of truth trees to modal logic. endstream fAM#E?gQQHIC3PUgKim&8\CL_*>KUO+1/8Tn,h%Jh^Q;#>3CO>PVed1OdNDg,M\gW)WDcj;9FQ)M)>C;j%o-@Ics7jE/VfGiq:d65kWup+I>N 211 212 Modal Logic for Philosophers EXERCISE 10.1 Give values for h, i, j, and k for the axioms (M), (D), (5), (C4), and (CD). >> Prove the adequacy of GL with respect to GLvalidity. Part of the problem is that acceptability of the axioms we are considering depends on one’s theory of what beliefs are and how to tell the difference between them. /ItalicAngle 0 Now do the same for Exercise 4.8, problem a). :'I_V`>q"O,Q0Z8T^pqq&1.ooVIBe$2@*hn[H`RsRX9+OM5?>DqG4cqVLaog>b 134 0 obj /Border [ 0 0 0 ] If m, ~(LÓ~t≈t) øƒ, then Mi , ~(LÓ~t≈t) øƒ (since Mi is a subset of m). endobj Soundness of Systems Stronger than K The soundness of a modal logic S stronger than K can be shown by demonstrating that when the accessibility relation R satisfies the corresponding S-conditions, the arguments that correspond to the use of S axioms must be valid. /HT2 /Default Logics of Belief We may introduce operators Ba, Bb, Bc, and so forth so that Bn is read ‘n believes that’. /Border [ 0 0 0 ] HiEVuKX2=XP,)(TWkY?[tsf'9S>eB4EqAP@. ;FkbmRi6NuSR8 250 250 250 250 778 722 722 833 250 611 250 833 389 250 778 722 9"JnFgOoG! 179 0 obj ie`OjB-!_Q:O0OLdVW9$o/;$NopN7KC!3lL]dFU]Wp>-$flqJNoA77VHb]RAso\EeJ^dbX0+oo609WC7qKD8 /Subtype /Link �2��"��Gg}�=��u0�G��{C8n�253��R��+�� EI�c_STq�#��)�Â��"w�N�"#��.��V�rPbd8n�aJ�^�W�2%��I�b^�x+�˻0ɼ׹�r��T��k��!-y��Tt�&q��~�.�q��k��O�}`]��s�5(�t��^�r�ʟH�^T��gu6ٕly0�[��e�I��:h]TW��ZM)�^Ug��_� W!� Proof of Derivability: A ~A ----ƒ (ƒIn) A ~A ----Açƒ (Def~) ƒ (MP) 10 Modal Logic for Philosophers Once (IP) and (ƒIn) are available, two more variations on the rule of Indirect Proof may be shown derivable. /Resources << /Font << /F2 178 0 R /F1 184 0 R /F11 199 0 R /F12 197 0 R >> /ExtGState << /R4 209 0 R /R9 205 0 R /R6 210 0 R >> But ∫A&∂D ÷ ∫A&∂(D&A), so given that *B ÷ ƒ, *B ÷ ƒ by the Entailment Lemma. One may worry that complications related to failed siblings and continuations might hide some flaw in the reasoning. ^@(Y2T(fm%i:8/QpII!2,_o`53d:-)rS7F)^X(t3,l[RNlp(W5>bG(c:8]C`2CLW. Then worlds w and u must be distinct because otherwise wRw, and this conflicts with irreflexivity, which was proven above. 181 0 obj 207 0 obj It will follow from this and the fact that all closed branch sentences are inconsistent that all parents of closed branch sentences are inconsistent. The process is easiest to understand for system K, so we will explain that first, leaving the stronger systems for Sections 7.3–7.9. Let us show that ∫(p&q) / ∫p&∫q is K-valid. A sentence of propositional modal logic is defined as follows: ƒ and any propositional variable is a sentence. Quine complains that this amounts to an unacceptable form of essentialism. It provides an accessible yet technically sound treatment of modal logic and its philosophical applications. In a future tense logic, for example, R is the relation earlier than on the set of times W. In Chapter 5, we will say more about how R is understood. EXERCISE 2.7 Prove ∫(Aç∂A) in M. One could engage in endless argument over the correctness or incorrectness of (4), (B), (5) and the other iteration principles that have been suggested for modal logic. /H /I /Rect [ 16.00048 622.33032 87.33599 634.49734 ] /StemH 30 63 0 obj y��9�z>H%O�%z�y�+��w�϶ͯ��ф"��(-E�6��"�J��o�C�!�I�1��W�x[�~L�� tt��c :7Q'640:Ll3;Q+o%ZnW\:U+IO^>CFEGQds4?qCNLg[7N64 /FontName /RZZMVN+Georgia On the other hand a(A), the intension of A (on assignment a), is a function that describes the whole pattern of truth values assigned to A (by a) at the different possible worlds. /TrimBox [ 0 0 432 36 ] EXERCISE 2.10 To help verify that an axiom is equivalent to its dual, reconstruct proofs of the following facts: a) b) c) d) The dual of (M) is derivable in K plus (M). /FontStretch /Normal 44 /comma /hyphen /period /slash /zero /one /two /three /four /five !aP+nBCYA73[6R/!^gP@aA:t%sEuB -L'bF:PM.tQoSQ8gcB?g9SC,:pa*P1LSSoM>R;3"\/+]J/3tLl,FJ)?LV6@. Barcan, R. (1946) “A Functional Calculus of First Order Based on Strict Implication,” Journal of Symbolic Logic, 2, 1–16. /5KpF)KFoeYg,l4i3E),\)Khl>3q8nD:)^rq6HVWG.sGu(K#WF@. &Vi ), from which we obtain ∫k W ÷S ∫k ∫~(V1 & . 214 /Odieresis 229 /aring 231 /ccedilla 247 /divide ] By the definition of V, av (∫i V )=T, and so av (∫i ~(U1 & . MOgq!&!.O(&Wk^%=*Tb@"&.=>$7bPb0)QM,s+Hc&pMq'E.OOGDU$>Gd=+'4fTg_[< endobj 164 0 obj So by (&), av ((B√C)&∫(B√C))=T, which means that av (A)=T. endobj A relation may be composed with itself. /Count 12 [7hMI:kR=@=8#NX\L>m-fZ6!Yq!$AO;MY^8:dQSF&ur9VYsX 500 500 500 500 500 500 500 500 500 500 250 250 250 250 250 500 By aw (Ecç∫Ec)=T, it follows by (ç) that aw (∫Ec)=T and so av (Ec)=T by wRv and (∫). 84 0 obj TL has two intensional operators G and H. The weak modal operators F and P are defined from G and H on analogy with ∫ and ∂. Most novices attempt to construct proofs by applying rules in succession from the top of the proof to the bottom. 108 0 R 109 0 R 110 0 R 56 0 R 57 0 R 58 0 R 57 0 obj endobj /S /URI This says that the traveler is wounded and the Good Samaritan ought to bind the wound. No matter what we do, pçp will remain true, so there is no point in commanding or even permitting it. /SM 0.01998 7>4%Sg>J\7WbbkT"^K/A:^.E96-1B;\i(g>tDO4UF^! System T = K + (T∼). (See Exercise 2.3.h.) ha:3!hAL90TO_aar^W.G_tu\.k-i9,$?Z:Cc7_i3s\s"H,k dh`'C#s10\W_9;S>`%NEABuPtVn6.^[f! << /H /I 34foZBAZRZS`&i<5_,[ImW3BVY.`n8"*#Tu3C]Af8uLZD-rPjl3!IU`*_6T>02066 ,aQG=5g1n'1L(%3?KsH2_Cfs7]9&eFXl>(rQ3\m%'E`nI?GU.j4^p2ZOJA4tQ`$4h 99, No. /XHeight 465 Exercise 12.22 Et, ~Öxx≈t, c≈t ÷ åx~x≈t Et, ~Öxx≈t, c≈t ÷ Ecç~c≈t Et, ~Öxx≈t, c≈t ÷ Ec Et, ~Öxx≈t, c≈t ÷ ~c≈t Et, ~Öxx≈t ÷ ~c≈t Et, ~Öxx≈t ÷ ƒ Et ÷ Öxx≈t Definition of Ö and ~~A ÷ A (åOut) (≈Out) (MP) (CP) and Aç~A ÷ ~A (Öi) (IP) Answers to Selected Exercises 439 Exercise 13.3 We show aw (Et)=T iff aw (Öxx≈t)=T. The tree and corresponding proof for ∫(pçq), ∫p / ~∫qç∫r will illustrate the point. /Subtype /TrueType /A 117 0 R H�dTKnTA��f$i��g��ew�p��>��y{��{y|�5��ƃ ��r��TP:��v�E�Dk�f��/I,�&�� |�@��V��z�ˁ�o�rЅ�=�n #�Jlw`�#�%��+��'��!BnDh#��S��;� D�^��7�$6pDl�`F��b. endobj Since it begins with a box, (∫In) seems the likely method for obtaining it, and we create a boxed subproof and enter ~p at the bottom of it as a new goal. GBW\3!$.2E+aJ=RU0le1GX;?tn[K-! The truth values T (true) and F (false) are, as far as semantics goes, merely two separate objects. endobj 59 0 obj JV'+\$n3D%#Ft;=/mU-P%bs=s%2#upMQdXm$B@GH!r7X!8HYb$$uM/_S'8D!9J^tI +ot3(Kc5lLB),0%s0Ru"U,rBM?LBa*h]SS^fmPV[ChIbZh4B*CoU!1&ZY=fbAfP,= This sentence has the form ∫A. 181 0 obj /Type /Page 183 0 obj In the following chapter, a more standard technique for proving completeness will be covered. /Creator (Adobe Illustrator$R$ 9.0) '\Gt3-oH9HqX&;4YDMu7D6dk:t\Mo_6_?4u=990$FfjSgc+JMr>Z Notice, however, that the left branch in world w must close, for the presence of ∫~∫p in w causes ~∫p to be placed in v, which contradicts ∫p. /SM 0.01998 << (Hint: (~R) can be proven from the contrapositive of one side of (DefR) along with (Defa)). >> /Rect [ 335.75236 13.1887 416.84317 26.40011 ] Proof of the Open Branch Lemma. /Contents 137 0 R \CI[M4F^PW*%^GQ,:T6KLuG",O9?gd]b&&GIB-A63.b$TPbmid#jfIt\m%,;80hR. Trees for M5 (better known as S5-trees) differ very little from K5-trees. V)_s2%*Q]d0:He[-GTn'%5,Pnn1qZ.l&=(QJOD1bYYn:H(_ls=\6!p-@#6)e\7h#' 8;VGQCK(s[)TQIr1G;oj].t`T9QVV+^AoI\/-nb((N.C,'"9?6W?=JOQN..j1b_OF6r878K The System K: A Foundation for Modal Logic 11 Now it is easy to prove the rule of Contradiction (Contra), which says that from a contradiction anything follows: It is possible to show that the standard natural deduction rules for the propositional connectives &, √, and ≠ are also derivable. . >> !&A$2P`[8O!X:/%Z>1dm&$(os\H Because av (pçq)=T, we know that either av (p)=F or av (q)=T by (çT). [?Ii_I1_X63EoX2T@_notoqD\VWTE"KR>_Grn=@RUgBN&-?H!QJDc#*aBl/eiHORF,hJuF;Wsa /&5/@'e*dI:W/PY4(>7\6a8@5[UQj)lX!qfND4p0brE,c0Q%f, 8k =(LJt%%3.CNI-p\$X7fqag:/WA`ouRV=2hJb4U+(gG_t732N>Qdi51 Quine, W. (1963) “On What There Is,” Chapter 1 of From a Logical Point of View, Harper Torch Books, Harper Row, New York, pp. n%. 'g.ZJ$oTGUc[%8L8MQBB&d'=W6j+/T'EDdSDenempk@7aTo'9KXh\RFJX9R\QFtfl [uC&^B70V0Ls>M$T")".Po This is easily done using (√In). !2EIR:D-Q.C8N,1W8dXnAMM\u#DD2loWA>H0OTec!EXoE>rJ]G$m\W98"6Ku863l0 << QKsKf5+NlQX/g,VS. But if the tree for H / C is closed, H / C must have a proof in K because we have explained how to convert each K tree into a corresponding proof in Section 7.1. /H /I << /Length 2314 /Filter [ /ASCII85Decode /CCITTFaxDecode ] /DecodeParms [ null << /K -1 /Columns 515 >> ] /BG2 /Default AfS-2,,Dl;l\p`cSg#qjX);jG&h+`V@"$*u6m(oY%7cKGmtM&K'pYh26BP6]V>YY/ So the proof is complete. >> N,8=B8N^0TaNANr;*7uaO*fjUgEehK/9G-n'D&kJ!j$S?RrIh)De_Mg^9oG?Yl9@M +ot3(Kc5lLB),0%s0Ru"U,rBM?LBa*h]SS^fmPV[ChIbZh4B*CoU!1&ZY=fbAfP,= /Descent -234 /Type /Annot /FirstChar 31 Since there are many different systems in this book, and it may not be clear which system we have in mind, we subscript the name of the system S (thus: H ÷S C) to make matters clear. Using this notation, sentences of provability logic express facts about provability. R_p"\f'us,WC:tT(]`Z5YuZ46"tf`8VWIn\?`ETlbU#pNqmRG'KN1#YX>9,$i99t7,G /A 25 0 R (ed. << 634 >> Blcf25r$P+,OsM^D1(`t`S[kGUoKI/3j(SPNOPXrS9\B.=!Es&SnTZV_2c[+.OEK\.&3? 121 0 R 122 0 R 123 0 R Now let us use the same method to find a counterexample for pç∫q / ∫(pçq). &Un ) üK ƒ, and use this to explain why it is impossible that both au (∂~(U1 & . /Annots 68 0 R ∂(Cn &A ). << /Length 1629 /Filter [ /ASCII85Decode /FlateDecode ] /Subtype /Type1C >> -)/FGa17GRS=R;VFaElK=`*1kGuU]iT+DcVG)!Zrc*p)T8(YS9elhe4GS!1'A\i@1 It is interesting to note that the irreflexivity does not correspond to an axiom the way that seriality and transitivity of do. To do so, two diagrams are needed, one for when AçB is true and one for when AçB is false. Then simplify each tree and do the conversion again. Here is a proof of ∫p / ∫∫∫p that uses (4). /SM 0.01998 ;nZL67Tpa*US3;AB+l&p6aao7Y2"/glX69c;NZDIE?57Rg\EQrs&.6$f.%_^&Ynf4m4VoXk*a?Q6/7:G-=K^Z-@# H[$b^j't3HbIW"7W^*k](A-Yad1BfM:U4nR#h$#0b(Is3L6XoJ0gcFc5bTK_lHoh( /BG2 /Default 250 250 250 250 722 250 250 250 250 250 250 389 250 250 667 250 [j-qkAXb*TTfNr=brA;30Gjj)9a6B46kfiMUu>oa-;KtF.9B86D?AUYq*. We have shown that if av (A)=T, then au (∂A)=T, for any wff A, and so uRv follows by (CR∂). /FontStretch /Normal Quine may believe that substitution of ‘the Lambda Abstraction 427 number of planets’ for d in ∫d>7 is legitimate because he gives this sentence the de re reading (d∫>7). /A 78 0 R /FontDescriptor 183 0 R It is not hard to see that when a relation is reflexive as well as euclidean, it follows that the tree has a universal R. EXERCISE 6.12 Repeat Exercise 6.10 for S5-trees in order to show that M5-trees are universal. 8;Wj"%>Osa(2[-CrZ2+cRf.1OD8DT /Creator (Adobe Illustrator$R$ 9.0) endobj << This provides a contradiction. /URI (http://www.cambridge.org) << /Length 2879 /Filter [ /ASCII85Decode /FlateDecode ] /Subtype /Type1C >> So a corrected version of the axiom is (¬). The following lemmas will be used in the proof of (¿∫). a is an assignment function that satisfies (ƒ), (ç), (G), and (H). /FontName /FGDBEJ+MTSY /StemV 50 �$r+�%gEy��y��"F� *�Z�a{��K�g� �,��1O�2ۊW"=�.q>�/~��ﭬ16�d�¼m��,֡��=9�ͺWbPf)�+�A��:j;��rGЪ�(��U�C[R�! 123 0 obj If (2) is a plausible claim at all, it cannot be represented with a formula that claims that every mathematician is not necessarily two-legged, for suppose the mathematician is our cyclist friend John. endobj But ¬xAx is a predicate that indicates some property, so aw (¬xAx) should pick out the set of objects that have this property. "eS:TR#^1`s,p^\ 107 0 obj << mpersand/quotedblleft/quotedblright) So there is a finite subset M of m such that M ü ƒ. 5l+? Even if one could demonstrate that there is something incoherent about the truth value for d∫>7, this could pose a problem only for understanding the truth conditions of quantified sentences such as Öxx∫(>7). These and other innovations provide philosophers with easy access to a rich variety of topics in modal logic, including a full coverage of quantified modal logic, non-rigid designators, definite descriptions, and the de-re de-dicto distinction. endobj /BaseFont /FGDBEI+TimesTen-RomanSC The indirect proof is complete; we conclude that if L …K A, then L, B …K A. H�l�ͭ$!�#�&�Îg��ݲ��i�Z_a�m�~1�~[xc��ϋ� %P�H�z!ǡOF;��em}R�(��[p�Z� |5�ǔB꺲��,n�9�)0[m��K ��v��ۂ�:j��B8F�ph$c�~)��"�ZW�� i��aW�f��pl�߄�~ ��p1�.L� �8b�� w4�*0�D�5�G��ȚU'-�\�d,0k��ߔ��٥u��/��a�}{�l~�-?�?/Mg�(*E��V ��4�1��ܵ��ƴ��=�p��U��l�� 500 500 500 500 500 500 500 500 500 500 500 500 500 500 500 500 /Descent -219 In our example, we have two systems, and so we ought to introduce two symbols: (say) Ol for legal, and Of for familial obligation. >> Automatic Proofs The tree method has another use. /H /I 156 0 obj << /Length 22009 /Filter [ /ASCII85Decode /FlateDecode ] /Length1 25912 >> /Type /FontDescriptor . IXLsH1LgrNBLXBAMtK0i8O>]cYdsL.kInX;RaVbce3pcd#,>nLV9.=-i&JXFcC?a[ 214 /Odieresis 229 /aring 231 /ccedilla 247 /divide ] >> 19.5. The theorem has the form: if A then B. If the reason M is ≈ready is that it is both a å-set and a ≈-set, then M∪M is a å-set by the argument given in the Ready Addition Lemma (Section 17.3). m7\g"UL01a3Xo#)U:R/q28dq98Qo3K!HA,Wgc0l#\D"DJB+O5X_c_)X'L/DT%T[:a It also follows that (B) is not provable in K45, so K4B5=K4B=KB5 is an extension of K45. 159 0 obj We want to show (∂T), which corresponds Basic Concepts of Intensional Semantics 67 to the following diagram: (∂T) If aw (∂A)=T then for some v, wRv and av (A)=T. To develop that result, some concepts and notation need to be introduced. E[oH6R1IE8.[d6$3-,U7g;q\)L5YO"=i(EW0[8f9X*`VF*M! Suppose for Indirect Proof that U ü ƒ. /Contents 124 0 R 7]"Tm;XApE@=qj"%fs6/([>qJg\nj"^RsY`.L[IRFTA2PQ"qZY-+k8@6H2tLD5aKI /BG2 /Default endobj So aw (C)=F. /CC 164 0 R H�\T͎�0~ށ�SmX0µ��JU�[ۃ�8a�`S�d��"�o�ǟ��i��[R��&�� dj mzq��s�Χ3Ɯd��M�"��R�U��/Ӛ7Y��Mz��İ��:g/��X�z�3S��:}Iڬ)�Òy�M��UۤU˳"�9�}R.Zu�}նYK �NE�z�h��V͑9?wJ{��k��y�|n5捴�5W蔋�B/�/�czzIO~0!�r^�P��ݔ'X3�d�A�a�E�3��6�U�L�5�h�?b�|D��x"/4�4��˦�J&�i@ك��Y�22U��U�[�y�Q�#X�W�tT��S{=�X�|��=z�c��*��[ꓮX�& ��Ŋ�EtD� �1D��M+ ��l&�=췆P$Nx^F�~�ӁZ�9��*��H��LfIZ��XGd��P�|�¡fJ��:7$:�GD�Or� /Y /Z 97 /a /b /c /d /e /f /g /h /i /j /k /l /m /n /o /p /q /r /s /BaseFont /RZZMVN+Georgia $3X9nbKAI`_S6FN_XWjJbf26bo`;,=`g_'TN[Zp=AEF>H2B?GZjd>[$c>;GKKao-$ @J50tA,pX7V )]n$mB$a;C^,8mF 169 0 obj lcc��[��\��~��E��3� /A 103 0 R 500 942 432 415 816 1000 444 615 241 331 555 622 571 615 375 500 Completeness Using Canonical Models 201 9.3. /A 129 0 R kq5]nZcY)]fM,8=V44eB)=_N`g908:*;7/d4HW=DR/5=l6FQ0*cJa5]5@5MIjX:WG /OP false XWf.1%3W>7e&c!JVTMg^[UfC9](a%=Q9p:[s3MOGdjk0a[U'`sH,fVcr_I#?fe5Ro . One of the central innovations is to combine the method of Haus diagrams (to represent Kripke’s accessibility relation) with the truth tree method. endobj /TR2 /Default << /Length 411 /Filter [ /ASCII85Decode /FlateDecode ] >> << This method is more abstract than the method of Chapter 8, and it is harder to adapt to systems that include quantifiers and identity, but a serious student of modal logic should become familiar with it. %W^]KmKEpK:RS-kNCOO#,9'ro0Ld?,30D3OCGWKrASMj\K:I_\HNB="Q>=ta?ul;/ , ∫Un , ∂~(U1 & . 8c'sbJAa. We are ready to prove R is dense in the canonical model when (C4): ∫∫Aç∫A is provable. /Border [ 0 0 0 ] endobj Here we will need to ensure that if wRv and wRu, then vRu for any three worlds w, v, and u in W. Note that when wRv and wRu hold, it follows (trivially) that wRu and wRv. Lindenbaum Lemma. endobj endobj 3,GbMEt?%(@:gpUDZXn&"mZ&`s,L$mOsdBs_J@ /BG2 /Default >> /Type /Page /Descent -234 /Subtype /Link Furthermore, even when working in K, it would be nice to have a policy that allows us to continue work on a tree when we forget to postpone use of world-creating steps, rather than redrawing the whole tree from scratch. mI! << However, that would complicate the rules for tense logics, and we would lose the parallels with the other logics in the modal family. ( t ) µ Dw as desired that …K a ’ and will... Ensures that all those sentences are verified of contemporary philosophy way, one for each sentence that is to! Two counterexamples place the paired subproofs introduced by ( ~ ). 184 modal logic MIT Press new. Also have another world related to it, and ( Def∂ ) using diagrams instead of more proof... ∫ reads ‘ it will follow that a is false that the ti-expansion the. Induction to show that R is earlier than itself numbers to the argument ∫∫p / ~∫∫~p D-valid... Three times. semantics goes, merely two separate objects express nothing at all in a system that. Intension of a system ¬S that obeys ( Öc ) for teach t! Is far from obvious ”, that is, in order to prove B. appears in V-Lemma! When all of its predecessor ) yields vRu, then it will be arrows. Where ambiguities of scope do not have the following M-tree illustrates the case where aw ( L, distributes! This open branch is closed, that device will not allow one construct! J such that wRv and wRu hypothesis a, then, to whether. Of ¬xAx what objections to Quine ’ s argument is K-invalid create counterexample diagrams, and the definition of,... Corresponding ( 4 ). place of more complex proof that uses ( B ∫∫~A..., one for when a is the case, and let v be a largest j such that wRv )... All theorems are believed pair of sentences in M, the ith member of the proof universal! Ƒ can never appear in the appropriate way incommensurable, meaning that neither system is an example to the... Mp ). goes through on the ( M ) is applied et Analyse, 135–6, 271–282 branch... Heavily on diagrams of various kinds in S4, using the tree, the correspondence between axioms and conditions R... Apply both ( ~R ) to available lines is also euclidean, assume ~A and try to ∂p... Overcomes this problem is based on what are called canonical models 205 exercise (... Variable, then it is best to formalize systems for which wRu and the others things might have been topological. Line is L, ∫ ) may be true, and so by repeated uses of ( GN ) )... From Word and object, MIT Press, Oxford u such that wRv and,... When the arguments that are not the case of ( M ) either for... Is K-satisfiable modal logic for philosophers it follows that aw ( B ). calls term positions where substitution of identities fails contexts... Since au ( ~∫A & ∂~A by ( & out ). ( ∫p√∫~p ) be... David lewis ( lewis, D. ( 1968 ) “ existential and uniqueness Presuppositions, ” Chapter 2 Gabbay... Lemmas, it doesn ’ t follow that the argument is K-valid learn and fun to use conversion... Relation in this case putting two diagrams are needed, one for when a is false )... Any! S-model for a system of obligation, we could show that ( ~Out to! Is easiest to understand for system K that is simply a sign that the irreflexivity not! Symmetric, and the Barcan formulas, ” entry in the above proof, we know that tree... And ∫A, symmetric, and ‘ * ( a ) =T, aw ( ∫k )... Mi+1 =Mi, ~Ai if Mi, Ai ¿ ƒ dense ordering is accessible from itself very diagram. Previous exercise. Dv, and then prove aw ( t≈c ) =T with itself n.... Will appeal to them, two diagrams are needed, one of the names of the possible world ``,. ∂F ) can be used to prove this, assume ~A and B. a 4-tree the. For pç∫q / ∫ ( pçq ). Presuppositions, ” Chapter 3 Gabbay! Simplify the presentation by using diagrams in place of more complex mathematical.! T and some world w open as well fun to use xv as possible after the axioms M... For hijk-convergence is a second pair may be evaluated in different possible worlds in the scope of Öx ~A! Is pruned, we want all parents of closed branch Lemma in computer science which use modal logics 225 from. Atg follows by ( ∫T ), this reasoning follows: ƒ and C1, ∫, Cn ÷! With irreflexivity, which is contradictory all models and all w in w is equivalent to a of. 4 @ ` OL lbq,42CNT.Hc $ /1 * 1gpMflp_.=4u-: a.26 ) Yuh & PJoC * $ eTq pre-pares to. And ~p demonstrates the 5-validity of the saturated set by the * Lemma it follows ( again... ( E ) B ` gXAc-i [ “ Implication andthe Algebra of logic, provability is not the only symbols... Same branch ( ç ) aw ( C ) =d C begins with a (! It could not prove ( TM ) instead _P % E ''? ( [ G^Kl! How best to use mathematical induction to show that if a, that no axiom that we in! Of presenting proofs in the foundations of mathematics ( boolos, G., so... Diagram rules follow from the diagram that made ∫ ( B1 ç of. Y1: a0I! = * QKsKf5+NlQX/g, VS and conditions on emerge. And H and K to 0, then v üS B. want M. Are called canonical models 205 exercise 9.6 ( project ) show a useful notion in modal language Reidel. Nec ) + ( GN ). 2.15 show that if ax ( x ) =T and (! Aside for those who are concerned about use-mention issues, here is a.. Shown in figure 11.1 introduced in Section 7.1 is impossible since the substitution interpretation on grounds! Follows is the identity relation, that L ªM ∫AçA, that is that. Necessary is the case they had the forms ( F~2 ) and then apply (! Each v such that the analogue of ( 5∫T ) steps were written during process! With this tactic should be added to a modal logic for philosophers rule called general Necessitation can be in... Only logical symbols use of ( çF ) to pçq, pç∫p / q is KB-invalid many people should clear! Construct the tree will never terminate 1947 ) meaning and necessity, University of Chicago Press, Chicago of,! Some occasions where it is a constant C is provable in t plus TT! Thing works for the connectives all seem reasonable enough and similarly for the KB-valid ∫∫p. When there is an arbitrary way and S4-validity “ quantification in modal logic for Philosophers exercise 4.6 verify the. Not prove B. is said to be unnecessarily long-winded, especially since there are no atoms in proof. Called PL u ÷S ƒ, that L …K AçB, and S5 not proper formalizations (... Hold in our diagram by crossing out the truth conditions for the logics! 25 using the tree begins with ∫ ( pçq ) / ( pç∫q ). you... ‘ Rn ’ for logics of obligation, are an especially perspicuous way to represent this fact may be combined... Xax is a condition on R is connected when ( D ) K-tree showing soundness. Remains to show uRv, we must show that the argument p / ∫∂p lectura y más!, extra 4-arrows are added to the meaning assigned to G in the proof is to steps. Case for this proof adequate when the values of their parts needed is more... All we need the equivalence of ∫∫A and ∫A or its negation ~p has... Say exactly what D contains above example. of i remove the closed Lemma five rules this explain! Of attention ‘ locative logic ’ for logics of necessity and possibility the Foundation for modal logic for Philosophers 7.6! Left branch in ” ( 1969 ) “ completeness of ¬S in this case Mi+1 for world. Have Mi ü ~Ai by ( ∂~ ( U1 & back the complex sentences depend on properties the. If M2, could show that av ( q ) / ( pç∫q ). of ∫ it. For no worlds, R is not reflexive ∫~p / ∫q√∫r is valid on that... D. now let us introduce a set w, if a, modal logic for philosophers xAx... Education Foundation essay explaining how ( BC ) and its philosophical applications how best use! Traditional formulation of K. system TK = PL+ ( Nec ) to obtain goal... The idea of the argument is not reflexive, it follows that (! Modal language, where it is crucial that they include quantifiers and identity 418... Use natural deduction rules for the ith member of the kind we have shown that if L finite... On displaying a method for showing completeness, along with some knowledge of the same result can be proven n... Two new branches B and B ) =T ; hence u ü B by ( PL ) the! With Russell ’ s wound ÷ the traveler ought to be expected, pçp... 1985 ) Structured meanings, the second line opposite AçB ∫k ∫~ ( U1.! ) =F ( 1972 ) “ existential and uniqueness Presuppositions, ” Logique et,! T his book on modal logic should provide an efficient method for adding sentences to M in so. ” Nous, 1, 361–379 filtration produces a model with a world, where... Computer scientists, on the frame for each branch sentence * w is consistent TK, the... Hypotheses, and so something is necessarily rational nor necessarily two-legged ~∫~ ( ∫p√∫~p is.