Modal Logic PHIL 511
Popular in Course
Popular in PHIL-Philosophy
This 3 page Class Notes was uploaded by Ms. Jada Ernser on Friday October 30, 2015. The Class Notes belongs to PHIL 511 at University of Massachusetts taught by Staff in Fall. Since its upload, it has received 17 views. For similar materials see /class/232337/phil-511-university-of-massachusetts in PHIL-Philosophy at University of Massachusetts.
Reviews for Modal Logic
Report this Material
What is Karma?
Karma is the currency of StudySoup.
You can buy or earn more Karma at anytime and redeem it for class notes, study guides, flashcards, and more!
Date Created: 10/30/15
9 3 Tree Conversion Converting trees to proofs in quanti ed modal logic is both possible and straightforward Indeed it is not worth our time to go over all the details The basic procedure is the same as for proposi tional logic The tree rules for identity logic correspond directly to inference rules or axiomsl The rules for true Vstatements and false 3 statements correspond to VOut or QVOut in the latter case you can use NHOut to change N Hz A1 to V1 NAz beforehand The rules for true Hstatements and false V statements correspond to the HOut or QHOut de rived rules In the latter case you can use NVOut to change NVI A1 to SI NAz beforehand The only tricky thing has to do with occasions in which we have to reapply a rule of the former kind in an earlier world box after applying a rule of the latter kind in a later world box If converted directly the constant introduced for HOut or QHOut may not be new thus making the derived rule inapplicablel Earlier we saw this example for classical quanti cation NVXWyDRyX A DVyRyX W NVyD Rya A DVy Rya VyDRya NDVyRya The way around this is to note that since b was new when we introduced it it must not occur in any of the hypotheses above when converted Hypotheses occur only with premises the negation of the conclusion branches and the rst lines in a world box but this structure must already be in place when the rule was rst used Rather than using it we may take the result of the QHOut as a new assumptionl It leads to L so we may take this as a reductio of the result Since the constant does not occur in any hypotheses we may use Vln The result will be the opposite of the existential statement or false universal statement with which we began For the above we get 11 w NVnyDRyXH DVyRyx 2 XNWyDRyXHDVyRyx 3 NVy D Rya A D Vy Rya 2 QHOut 4 Vy D Rya 3 51 N D Vy Rya 3 6 D Raa 4 QVOut 7 D Rba 4 QVOut 8 O N Vy Rya 5 N D 9 V D NVy Rya 101 Raa 6 DOut 111 NRba 121 Rba 7 Reit DOut 131 L 1112 Lln 141 Rba 11713 IP 151 Vy Rya l4 QVln 161 L 915 Lln 171 L 89716 ltgt L 181 VnyDRyx A DVyRyx 1717 ll This or a similar procedure should handle all tree conversions 10 Metatheory for Quanti ed Modal Logic For the most part the results we are after are similar to those we saw in our earlier unitl Indeed I donlt think it is worth our time to examine the metalin guistic proofs in as much detail as we did then since much of it would be redundant Assigning you to ll in the details might make an excellent nal exam question however Things are a bit more complicated as well by the fact that welve looked at three ways of doing for mal semantics for quanti ed modal logic Proving soundness and completeness results separately for each would be time consuming In class I shall focus on establishing the following square of results 56 A1iHAnHKBgtA1HiAnliKB Thetreefor A17 7 n7 closes lt A1 i i i An HK B As well as similar results for l39T fB fS4 fSS qK qS5 etci Put together these results establish both sound ness and completeness for fK visavis both substitu tional and intensional semantics as well as the ex tensional equivalence of those two approaches to se manticsi The results will also point the way towards nd ing similar results for objectual semantics since oK models can be de ned as a subspecies of iK models For all intents and purposes we have already sketched the proof for the left side of this square since closed trees can be converted into reductio proofsi Provided we have drawn the right kind of trees the results hold not just for fK but also l39T FB fK4 fSS etc as well as qK qB qS5 and the others What remains are the three other sidesi We shall content ourselves with mere sketchesi 101 Tree Modeling Taking things somewhat out of order from Garson7s presentation of this material jumping ahead to chapi 16 we now move on to the bottom part of the square ire that if a given argument is valid on substitutionaltruth value semantics then the tree for it closes As before we establish this by proving the cantmpasz39tive ie that if tree for an argument 1 H has an open branch then it is in valid ie there is a tK or tT or tS5 etci coun terexample to it The argument for this is almost exactly the same as the argument we saw for it in propositional logici We de ne the Tree Model as the model W R agt where W is the set of worlds that have world boxes on the tree R is the accessibility relation between them as shown on the Tree and a makes an atomic statement true for a given world if and only if it appears in the world box for a given world To count as a tK model the model must obey the rule t stated on page 48 of the handoutsi Notice that this will be guaranteed by the application of the identity tree rules If rules for rigid constants systems have been ap plied then the Tree Model will count as a rtK model ie a tK model in which awb c avb c for all worlds W and V in W since this atomic statement will appear in all world boxes if it appears in any gain we use wff induction to show that for every sentence C if C appears on the open branch in the world box for a given world W in W then awC T The base case is true by the de nition of the tree model and the fact that the branch is open For the induction step we assume as inductive hy pothesis that this holds for all sentences shorter than C and need to prove that it holds for C as well For the cases in which C takes one of the forms DD D1 4 D27 NP7517 7tn7 N D D ND1 A D27 Niv we get the result the same as with our propositional soundness proofi We need only show the same for statements of the forms VI DI and NVI Dzi We are assuming that all de ned notation has been elim inate i i Suppose C takes the form VI Dzi If all tree rules have been applied then for every constant c i EC appears on the tree branch in the world box for W then so does Dci By the inductive hypoth esis this means if aw EC T then aw Dc Ti By the semantics for the quanti er in substitu tional models this means that awVz Dz T ire awC Ti 7 Suppose C takes the form N VI Dzi If all tree rules have been applied there is a constant c such that both EC and NDC appears on the tree in the world box It follows by inductive hypothesis that aw T and aw NDC T It follows that awDc Fl Hence it is not the case that for all c if awEc T then awDc Ti By the semantics for the quanti er aw VI Dz F and therefore awVz Dz T iiei awC T This completes the induction Hence the premises at the top of the tree are true in the starting world and the negation of the conclusion is also true and thefore the conclusion is false It follows that the tree model is a countermodeli 10 2 Soundness We now turn to the top of our rectange and establish that if a given argument A1 i i i An B has an fK or l39T fB fS4 fSS proof then it is is iK or iT iB iS4 iS5 respectively valid ie for all worlds W in W in an iK model WR lDIa if aw A1 T and and aw An T then awB T as well Again we assume we have a proof in the appro priate system from A1 i i i An to B We require the proof be written out in full with no derived rules or notation or theorems citedi Assume also that for an arbitrary intensional model W R ll I a and world w in W awA1 T and i H and awAn T We need to show that aw B T as well We prove by proof induction that every line in the proof has the property 45 ie that it is true in all worlds V in W that makes all the relevant assump tions for that line true The relevant assumptions are de nedjust as we did for propositional logic see page 34 of the handoutsi We assume as inductive hypothesis that 45 holds of all steps prior to the current step C in the proof We need to show that it holds of C as well Suppose that V makes all relevant assumptions truer Let us show that aVC T We tackle this by cases If line C is a hypothesis an MP step a DN step a CP step a DOut step a Uln step a Reit step or a modal axiom we obtain the result in precisely the same way as in propositional logici There are four more cases to consider a New case 1 C is an ln step and takes the form t ti Since avtavt is in aVI it follows that aVC Ti New case 2 C is an Out stepi Hence C takes the form Pu1i i i un tv1 i i i vm and we have in the same subproof s t and Pu1i i i un s vm By the inductive hypothesis avs t T which means that avs avti Also by the inductive v1ui hypothesis avPu17H 7un757v17Hwvm T7 SO ltavu17 7 aVun7aVS7aVv17 vavvmgt is in aVP i But this is the same as ltavltu1gtp i 7 avltungtavlttgtavltv1gt i avwm and so aV P u1xiuntv1ixvm T iiei aVC T a New case 5 C is an VOut stepi Hence C takes the form Be A Dc and we have a previous step of the form VI DI and by the inductive hypothesis aV VI Dz Ti There are two subcases to consider Suppose avc is not in DVi Then avEc F and hence aVEc A Dc Ti Suppose instead that avc is in DVi For each constant c the intension ac of c in the model is a member i of I and because avc is in DV iV is in DVi Hence by the semantics for quanti ed statements for the hybrid Di we have aVDi Ti Since i is the intension of c it follows that avDc T and therefore aV EC A Dc Ti Either way aVC T a New case 4 C is an Vln stepi Hence C takes the form VI DI and we have a previous line of the form EC A Dc where c does not appear in any hypothesisi Since 5 is a constant there is an intension i in I such that avEi A Di in fact since no special assumptions were made about 5 the same must be true for any intension i in I1 So for every such intension either aVEi F or avDi T For those such that iV is in DV it cannot be that aVEi F and so for those aVDi Ti By the semantics for the quanti er we get that aVV1Dz T iiei aVC Ti That exhausts the rules present in fK at least Hence 45 holds for every line C in our proof This is true of the last line ie E Hence B is true in every world V in our model that makes the premises truer Hence the argument from An to B is valid in the appropriate sense If we want to cover those proofs that utilize addi tional like axiom schemata like RC we must com pare their validity not to fK or qK models directly but only a limited subset such as with RC those in which aw c avc for every constant c and worlds W and V in the model It then follows that any in stance of RC has 45 because any instance of RC is true in every world in every model with rigid con stants We can show this as follows Suppose for reductio that avb c A D b c amp I f c A Db y 5 F in some such world Then it must be that either avb c A Db c F or avb c A Db c Fl Neither option is possible in the kind of model we have to consider If it were the case that avb c A D b c F then avb c T but avDb c F This means that avb avci It also means that there is some world u such that VRu and an I c F This means that aub auci But this is impossible since aub avb and auc avci For homework you need to show that it is also im possible that avb c A D b y c F which is the same as exercise 153 in the book This completes our discussion of soundnessi 17m7 1A more rigorous proof of this is given in the book
Are you sure you want to buy this material for
You're already Subscribed!
Looks like you've already subscribed to StudySoup, you won't need to purchase another subscription to get this material. To access this material simply click 'View Full Document'