DOC PREVIEW
CMU CS 15816 - Lecture Notes on Sequent Calculus

This preview shows page 1-2-3-24-25-26 out of 26 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 26 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

IntroductionSearching for VerificationsVerifications and SequentsCut EliminationIdentityTruth and Verifications, RevisitedModal Sequent CalculusProperties of the Modal Sequent CalculusUnprovable PropositionsLecture Notes onSequent Calculus15-816: Modal LogicFrank PfenningLecture 8February 9, 20101 IntroductionIn this lecture we present the sequent calculus and its theory. The sequentcalculus was originally developed by Gentzen [Gen35] as a means to estab-lish properties of a system of natural deduction. In particular, this includedconsistency, which means that not every proposition is provable. But thereare many other properties that naturally follow from the sequent calculusthat are much more difficult to see on natural deduction.For us, the sequent calculus provides a bridge between the truth andverification judgments. It will finally let us finish the internal global sound-ness and completeness theorems for the eliminations with respect to theintroductions discussed in earlier lectures.2 Searching for VerificationsIn ordinary intuitionistic logic, when searching for a verification we are ina situationA1↓ . . . An↓...C ↑where we try to select introductions to deduce C ↑ and eliminations to ap-ply to Ai↓ until we meet in the middle. The sequent calculus codifies thesethree kinds of steps as inference rules that are all read from the conclusionto the premises.LECTURE NOTES FEBRUARY 9, 2010L8.2 Sequent CalculusA sequent is a particular form of hypothetical judgmentA1left, . . . , Anleft ` C rightwhere A left corresponds to a proposition that can be used (A ↓) and C rightcorresponds to a proposition we have to verify (C ↑). The right rules de-compose C in analogy with the introduction rules, while the left rules de-compose one of the hypotheses, in analogy with the elimination rules, but“upside-down”. For the moment, we ignore the fine structure of proofsand do not label the hypotheses. We return to this in Exercise 2.We now go through each of the rules for verifications, constructing anal-ogous sequent rules. We still write Γ for a collection of hypotheses, wherein the sequent calculus they all have the form A left.Judgmental rule. The ruleP ↓P ↑↓↑means that if we have P on the left we can conclude P on the right.Γ, P left ` P rightinitConjunction. The introduction rule translates straightforwardly to theright rule.Γ ` A right Γ ` B rightΓ ` A ∧ B right∧RThe elimination ruleΓ ` A ∧ B ↓Γ ` A ↓∧ELmeans that if we have license to use A ∧ B, then we are justified in using A.During proof search, we are still licensed in using A ∧ B again, since we dohave a justification for using A ∧ B. So we obtain the following left rule:Γ, A ∧ B left, A left ` C rightΓ, A ∧ B left ` C right∧L1Here, A ∧ B is called the principal formula of the inference. Even thoughwe always write this as if it were on the right end of the hypotheses, theLECTURE NOTES FEBRUARY 9, 2010Sequent Calculus L8.3rule can be applied to any hypothesis since we consider their order to beirrelevant. If we ignore the additional assumption A ∧ B left, this is just theelimination rules upside-down, on the left of the hypothetical judgmentrather than to the right. We also obtain a second left rule, from the secondelimination rule.Γ, A ∧ B left, B left ` C rightΓ, A ∧ B left ` C right∧L2Implication. As is typical, the introduction rule translates straightforwardlyto a right rule.Γ, A ↓ ` B ↑Γ ` A ⊃ B ↑⊃IΓ, A left ` B rightΓ ` A ⊃ B right⊃RTo transcribe the elimination rule into a left rule, we just have to followcarefully the idea of bidirectional proof construction with introductionsand eliminations.Γ ` A ⊃ B ↓ Γ ` A ↑Γ ` B ↓⊃EIn order to use A ⊃ B we have to verify A, which then licenses us to use B.Γ, A ⊃ B left ` A right Γ, A ⊃ B left, B left ` C rightΓ, A ⊃ B left ` C right⊃LThere is some redundancy in this rule. The hypothesis A ⊃ B left in the sec-ond premise is not needed, because the assumption B left is strictly stronger.We retain it in this calculus for two reasons. For one, it makes the con-nections to verifications stronger, because in the construction of a verifica-tion one could re-use the assumption even if that is not strictly necessary.Secondly, this means that all rules (in the non-modal case) preserve mono-tonicity of hypotheses: an assumption, once made, will be available in theremainder of the bottom-up proof construction process.Disjunction. Again, the introduction rules correspond directly to the fol-lowing right rules.Γ ` A rightΓ ` A ∨ B right∨R1Γ ` B rightΓ ` A ∨ B right∨R2LECTURE NOTES FEBRUARY 9, 2010L8.4 Sequent CalculusPerhaps surprisingly, the somewhat awkward elimination ruleΓ ` A ∨ B ↓ Γ, A ↓ ` C ↑ Γ, B ↓ ` C ↑Γ ` C ↑∨Ebecomes much more similar to the other left rules.Γ, A ∨ B left, A left ` C right Γ, A ∨ B left, B left ` C rightΓ, A ∨ B left ` C right∨LAgain, we accept the redundancy for the sake of uniformity.Truth. There is no elimination rule, so we only have a right rule corre-sponding to the introduction rule.Γ ` A right>RFalsehood. There is no introduction rule, so we only have a left rule cor-responding the the elimination rule.Γ ` ⊥ ↓Γ ` C ↑⊥EΓ, ⊥ left ` C right⊥LThis concludes the rule for the purely (non-modal) intuitionistic se-quent calculus. Instead ofA1left, . . . , Anleft ` C rightwe writeA1, . . . , An=⇒ Cbecause with the new notation for sequents, the judgments left and rightare determined by the position of the formula in the sequent. The rules aresummarized in Figure1.We take weakening and contraction properties for the sequent assump-tions for granted; their proof is entirely straightforward and just followsfrom the general principles behind hypothetical judgments.LECTURE NOTES FEBRUARY 9, 2010Sequent Calculus L8.5Γ, P =⇒ PinitΓ =⇒ A Γ =⇒ BΓ =⇒ A ∧ B∧RΓ, A ∧ B, A =⇒ CΓ, A ∧ B =⇒ C∧L1Γ, A ∧ B, B =⇒ CΓ, A ∧ B =⇒ C∧L2Γ, A =⇒ BΓ =⇒ A ⊃ B⊃RΓ, A ⊃ B =⇒ A Γ, A ⊃ B, B =⇒ CΓ, A ⊃ B =⇒ C⊃LΓ =⇒ AΓ =⇒ A ∨ B∨R1Γ =⇒ BΓ =⇒ A ∨ B∨R2Γ, A ∨ B, A =⇒ C Γ, A ∨ B, B =⇒ CΓ, A ∨ B =⇒ C∨LΓ =⇒ >>Rno >L ruleno ⊥R rule Γ, ⊥ =⇒ C⊥LFigure 1: Intuitionistic Sequent Calculus3 Verifications and SequentsThe meaning of propositions is defined by their verifications. To show thatthe sequent calculus is sound with respect to


View Full Document

CMU CS 15816 - Lecture Notes on Sequent Calculus

Download Lecture Notes on Sequent Calculus
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Lecture Notes on Sequent Calculus and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Lecture Notes on Sequent Calculus 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?