New User Special Price Expires in

Let's log you in.

Sign in with Facebook


Don't have a StudySoup account? Create one here!


Create a StudySoup account

Be part of our community, it's free to join!

Sign up with Facebook


Create your account
By creating an account you agree to StudySoup's terms and conditions and privacy policy

Already have a StudySoup account? Login here

Modal Logic

by: Ms. Jada Ernser

Modal Logic PHIL 511

Ms. Jada Ernser
GPA 3.83


Almost Ready


These notes were just uploaded, and will be ready to view shortly.

Purchase these notes here, or revisit this page.

Either way, we'll remind you when they're ready :)

Preview These Notes for FREE

Get a free preview of these Notes, just enter your email below.

Unlock Preview
Unlock Preview

Preview these materials now for free

Why put in your email? Get access to more of this material and other relevant free materials for your school

View Preview

About this Document

Class Notes
25 ?




Popular in Course

Popular in PHIL-Philosophy

This 4 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 22 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
2 Modal System K Modal logic is not the name of a single logical system there are a number of different logical systems that make use of the signs D and ltgt each with its own set of rules Each system re ects a different understanding or conception of D and ltgt or the logical properties of necessity and possibility We begin with System K which forms the basis for many other systems le those systems are formed by adding additional rules to K System K is named after the logician philosopher Saul Kripke who was among the first to systematize formal semantics for modal logic The rules of K are consistent with many differ ent understandings of D and ltgt including among others deontic ones It should perhaps be noted that Garson s method for formalizing K is different from the usual way or Kripke s way but it results in the same theorems and derivability results 21 Syntax The logical language of System K is derived from that of PL by adding a single primitive monadic proposi tional operator D It behaves syntactically precisely as N does lts scope is on y what immediately comes after it Np gt a means if not p then a whereas p gt a means it s not true that if p then 11 Similarly Up gt a means if necessarily p then 11 whereas p gt a means necessarily if p then a The sign for possibility is not taken as primitive but defined in terms of D we ll also define signs for socalled strict implication and strict equivalence Def ltgt ltgtA abbreviates NDNA Def 3 A 3 B abbreviates DA gt B Def 2 3 A 2 3 B abbreviates A 3 B amp B 3 A The sign 3 was introduced by Cl Lewis in his pioneering work on modal logic much of which was motivated by the desire to define a logical notion of if M then i i that did not share the oddities of the material conditional A 3 B can be read A strictly implies B or A entails B 22 Boxed Subproofs The inference rules of K involve the notion of a boxed subproof which is a subproof that is headed not with a hypothesis but rather simply with the sign D lnformally the Dheader indicates that every line in the subproof is shown to be necessarily true We cannot bring statements into boxed subproofs using the Reit ruleithat would result in our regarding every true or assumedtrue statement as necessarily true Instead we have another rule DOut DOut i if a line of the form DA is available in the subproof previous to a given boxed subproof one may infer A within the boxed subproof The purpose of a boxed subproof is to be able to prove statements of the form DA Hence we have Dln i if a statement A is derived within a boxed subproof the boxed subproof may be closed and one may infer DA outside of that subproof System K consists only of the two rules above along with the rules of PL As an example proof in K below we prove that every instance of the Distribution schema is a theorem K O Dist tK mm gt B gt DA gt DB Proof 1 DA a B 2 DA 3 DA a B 1 Reit 4 D 5 A 2 DOut 6 A gt B 3 DOut 7 B 56 MP 8 DB 477 Dln 9 DA gt DB 278 CP 10 DA a B gt DA gt DB 19 CP Using boxed subproofs and PL rules it is possible to derive DA in K for any truthtable tautology A For example here is a proof of Dp gt q gt p 1 D 2 p 3 q 4 h 2 Reit 5 q a p 34 CP 6 P a q a p 25 CP 7 DO n 7 n 13 1765111 Indeed any theorem of K something that can be proven without use of premises or undischarged hy potheses can be proven to be necessary in K The Rule of Necessitation Nec if K A then PK D Indeed the usual formulation of K is to take Nec as a primitive inference rule along with every instance of Dist as an axiom ie something that can be written into any line of a proof or subproof with no other line as justification these two together are equivalent to having DIn and DOut The rule of necessitation coheres with almost all conceptions of necessity if something can be proven using the rules of logic alone then it must be neces sar Do not confuse this rule with the untrue claim that K A gt DA Indeed those conceptions of necessity that are con sistent with the rules of System K can roughly be characterized by two features i what can be proven true without assumptions is necessary ie Nec and ii that which necessarily follows from neces sary truths is also necessary ie Dist You ll notice that from here on out I ll almost never give proofs involving lowercase statement letters like 73 q and r but rather schematic letters like A B and C This makes the results proven general so that they can be applied in other contexts Moreover if all instances of a certain schema are shown to be theorems we shall allow ourselves to introduce one into any proof at any time rather than duplicate the steps of the proof already given 23 Inferences Involving Possibility Becuase ltgt is defined in terms of D no special basic 1 rules are needed for ltgt Here are some easy derived rules NO From ltgtA infer DNA Reallyjust DN ND From NBA infer ltgtA Proof 1 NBA 2 DNNA 3 NBA 1 Reit 4 D 5 A 2 mom 6 A 5 DN 7 DA 476 Dln 8 I 371In 9 NDNNA 278 IP 10 ltgtA 9 Def ltgt Because such statements are actually negations of statements with D if ltgt occurs on both sides of a conditional it may be easier to prove the contrapos itive of the result you re after Distltgt K mm gt B gt ltgtA gt ltgtB Proof 1 DA a B 2 7 ENE 3 DA a B 1 Reit 4 D 5 NB 2 DOut 6 A gt B 3 DOut 7 NA 56 MT 8 DNA 477 DIn 9 ENE gt DNA 278 CP 10 NDNA gt NDNB 9 CN 11 ltgtA a ltgtB 10 Def ltgt 12 DA a B a ltgtA a ltgtB 1711CP The above theorem schema is also important for obtaining the following derived rule represented schematically ltgtB ltgtOut In short if we know that A is possible and within a boxed subproof can prove that B would be true if we assumedA were true we are allowed to conclude that B is possible This is because we cold fill in the remainder of this proof schema as follows ltgtA A a B CP DA gt B Dln DA a B a ltgtA a ltgtB Distltgt ltgtA a ltgtB MP ltgtB MP Proofs of this form are quite common So common in fact that it is worthwhile to introduce a further abbre viated notation for representing the two subproofs involved in an application of ltgtOut as though it were a single subproof Garson does this as follows DA This kind of subproof is called a worldesubproof If we understand necessity as truth in all possible worlds a normal boxed subproof represents what we can prove about all possible worlds absolutely A worldsubproof represents what we can prove about all those possible worlds in which a certain hypoth esis holdsiin this case all those where A is true We shall generalize this style of abbreviation to other contexts in which we have subproofs within subproofs so that for example A BC D A gt B gt C gt D CP can be used as a convenient shorthand for three em bedded conditional proofs of the form CgtD CP BgtCgtD AgtBgtCgtD One must simply be careful with regard to Reit and DOut for subproofs with multiple headers Reit cannot be used with any header list containing i i DP i i and DOut can only traverse past one such D unless it is applied to something of the form EDA or D D D A etc If it is convenient to have the multiple headers on separate lines so that they can be cited separately for example we also use the abbreviated notation to the same effect Here s ltgtOut in action Let s show Distltgtamp K ltgtA amp B a ltgtA amp ltgtB 1 ltgtA amp B 2 DA amp B 3 b 3 ampOut 4 ltgtA 1273 ltgtOut 5 DA amp B 6 5 ampOut 7 ltgtB 1576 ltgtOut 8 ltgtA amp ltgtB 47 ampln 9 ltgtA amp B a ltgtA amp ltgtB 14 CP The converse of the above however does not hold but we do have PK DA amp ltgtB gt ltgtA amp B 1 DA amp ltgtB 2 DA 1 ampOut 3 ltgtB 1 ampOut 4 a B 5 A 2 mom Reit 6 A amp B 45 ampln 7 ltgtA amp B 3476 ltgtOut 8 DA amp ltgtB a ltgtA amp B 177 CP 3 Extensions of K T B S4 S5 Logical systems capturing stronger or at least more specific conceptions of necessity can be obtained by adding additional inference rules or axioms to K Consider the following schemata M DA a A B A gt DltgtA 4 DA gt EDA 5 ltgtA gt DltgtA According to M whatever is necessary is true This axiom should hold for any system codifying a con ception of alethic modality where necessity is under stood in terms of necessary truth An obvious de rived rule which we ll also abbreviate as M allows us to conclude A from EA within the same subproof Notice that rule DOut of K does not allow this M stands for modality where this word is understood in the narrow sense According to B what is actually true is necessarily possible This is named after L E Brouwer According to 4 if something is necessary it is nec essarily necessary This is one of the original axioms used by C 1 Lewis in codifying modal logic and retains the number used in his numbering of axioms According to 5 if something is possible it is neces sarily possible This the strongest of these principles coheres with the understanding of necessity as truth in all possible worlds absolutely For something to be possible is for it to be true at some world If it is true at some world it is true at all worlds that it is true at some world which is what it is for it to be necessarily possible Again the numbering comes from Lewis We can define a number of systems by adding the instances of one or more of the above to K System T the system obtained from K by allowing every instance of M as an an axiom System M another name for System T System B the system obtained from T by allowing every instance of B as an axiom System 4 the system obtained from T by allowing every instance of 4 as an axiom System 5 the system obtained from T by allowing every instance of 5 as an axiom Note that these systems add every instance of certain axiom schemata not individual axioms Axiom M covers not only UP A P but everything of that form including pr gt Np map A Up Dp gt gt11 gt Np gt 011 etc In the first proof scheme below we shall write DNA gt NA and cite M This is not confusing a statement with its negation but rather making use of a more specific schema all of whose instances are also instances of a more general schema


Buy Material

Are you sure you want to buy this material for

25 Karma

Buy Material

BOOM! Enjoy Your Free Notes!

We've added these Notes to your profile, click here to view them now.


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'

Why people love StudySoup

Steve Martinelli UC Los Angeles

"There's no way I would have passed my Organic Chemistry class this semester without the notes and study guides I got from StudySoup."

Amaris Trozzo George Washington University

"I made $350 in just two days after posting my first study guide."

Bentley McCaw University of Florida

"I was shooting for a perfect 4.0 GPA this semester. Having StudySoup as a study aid was critical to helping me achieve my goal...and I nailed it!"


"Their 'Elite Notetakers' are making over $1,200/month in sales by creating high quality content that helps their classmates in a time of need."

Become an Elite Notetaker and start selling your notes online!

Refund Policy


All subscriptions to StudySoup are paid in full at the time of subscribing. To change your credit card information or to cancel your subscription, go to "Edit Settings". All credit card information will be available there. If you should decide to cancel your subscription, it will continue to be valid until the next payment period, as all payments for the current period were made in advance. For special circumstances, please email


StudySoup has more than 1 million course-specific study resources to help students study smarter. If you’re having trouble finding what you’re looking for, our customer support team can help you find what you need! Feel free to contact them here:

Recurring Subscriptions: If you have canceled your recurring subscription on the day of renewal and have not downloaded any documents, you may request a refund by submitting an email to

Satisfaction Guarantee: If you’re not satisfied with your subscription, you can contact us for further help. Contact must be made within 3 business days of your subscription purchase and your refund request will be subject for review.

Please Note: Refunds can never be provided more than 30 days after the initial purchase date regardless of your activity on the site.