Project topics and materials
Get Complete Project Material File(s) Now! »
The sequent calculus G3cp
The sequent calculus G3cp for classical propositional logic closely resembles Gentzen’s original sequent calculus in [32], and was introduced in [102]. For p atomic formula, A and B formulas of the language, the set of formulas of classical propositional logic is generated by the following grammar: p j ? j :A j A ^ B j A _ B j A ! B. To de ne a system of sequent calculus we introduce the notion of sequent, specify its interpretation in the language of the logic and provide the set of initial sequents and inference rules2. De nition 2.2.1. A G3cp sequent is an expression of the form For a treatment of natural deduction, refer to [74]. We shall here treat only sequent calculus. the consequent of the sequent. Both antecedent and consequent can possibly be empty or constituted of just one formula occurrence. A sequent ) is interpreted in the language of classical propositional logic as follows:
^ _ ( ) )int = ! .
The symbol ) represents in the object language the metalinguistic notion of con-sequence relation, describing how some formulas (the assumptions) entail some other formulas (the conclusions). The comma in the antecedent represents conjunction at the meta-level, while the comma in the consequent represents disjunction. Thus, a se-quent can be read as: \from the conjunction of formulas in the antecedent follows the disjunction of formulas in the consequent ».
An empty antecedent is a conjunction of empty formulas (which conventionally stands for the truth >) and an empty consequent is a disjunction of empty formu-las (which conventionally stands for a generic contradiction ?). A sequent with both antecedent and consequent empty stands for a generic contradiction (> ! ?).
Desirable properties of sequent calculus
Given a well-formed formula we are interested in knowing whether this formula is valid in a certain system of logic L. If we have a sequent calculus S which is sound and complete with respect to L, we can decide the validity of the formula by trying to construct a derivation for it. Thus, a system of sequent calculus can be fruitfully employed to provide a decision procedure for the logic. One of the main interests of a proof theorist is to obtain – where possible – rules which facilitate the de nition of an e cient and automated decision procedure. Thus, it is useful to consider derivations bottom-up, in what is called root- rst proof search. The formula to be checked is placed at the root, and one tries to construct a derivation for it applying the inference rules of the system. There are several desirable require-ments allowing an e cient root- rst proof search. Here follows a non-exhaustive list of properties.
Analyticity. This property – de ned in the previous section – is essential for root- rst proof search: if the calculus is analytic, each formula occurring in a derivation is a subformula of the formulas occurring lower in the derivation branch. Thus, at each step of the derivation no new formulas are introduced, and all formulas can be ultimately traced down to the root of the derivation tree. All the (analytic) logical rules of G3cp are straightforwardly applicable bottom-up: it su ces to \decompose » the main formula of each rule into its active (sub)formulas. Conversely, applying bottom-up the cut rule requires to perform a guess on what formula should be chosen as cut-formula.
Avoidance of backtrack. In root- rst proof search, \backtracking » is the action of going back to a certain sequent and apply a di erent rule to it. In some calculi the order of application of the rules, or the formula to which a certain rule is applied, can determine the derivability of the formula at the root. In such calculi, to check the derivability of a formula we have to check all possible derivation trees – for if we end up with a failed proof search, it might be that we applied the wrong rules, or in the wrong order, to the sequents.
Usually, it is possible to avoid backtracking by means of an attentive de nition of the inference rules. If there is no need to backtrack, construction of just one derivation tree is enough to decide derivability of a sequent. Sequent calculi composed only of invertible rules avoid backtrack. If a rule is invertible, no pieces of information are lost when going from the conclusion to the premiss(es). For this reason, the invertible version of rule R_ (on the left) is preferred over its non-invertible version (on the right, composed of a pair of rules)7. ) ;A;B ) ; A R_0 ) ; B R_00 R_ ) ; A _ B ) ; A _ B ) ; A _ B. Observe that, if we were to apply root- rst rule R_0, we would loose formula B, which could have been the formula allowing to obtain an initial sequent. As explained in [70], invertible inference rules preserve both the validity and the refutability of sequents, allowing to construct only one derivation tree to asses the derivability of the sequent placed at the root. Conversely, non-invertible inference rules preserve only the validity of the sequent and thus possibly lead to a division of the proof search tree into multiple derivation trees, which are all to be tested in order to ascertain the refutability of the endsequent.
Preferential conditional logic
The preferential conditional logic PCL was rst studied by Burgess in [18] and Halpern and Friedman in [28]. This logic is weaker than Lewis’ systems, and it can be adapted to capture non-monotonic conditionals: as explained in Chapter 1, the non-monotonic logic P introduced by Kraus, Lehman and Magidor corresponds to the at fragment of PCL. De nition 3.1.1. The set of well formed formulas of PCL and its extensions is de ned by means of the following grammar, for p 2 Atm propositional variable and A; B 2 F>: F> ::= p j ? j A ^ B j A _ B j A ! B j A > B.
The conditional operator > can be read as expressing either a non-monotonic con-ditional, a counterfactual or a deontic conditional, depending on the system under con-sideration. When treating logics of Lewis’ family we will add to the language the com-parative plausibility operator, 4, where for A; B 2 F> the well-formed formula A 4 B reads \A is at least as plausible as B ».
The semantics of preferential conditional logics is usually de ned in terms of prefer-ential models, introduced in De nition 1.4.3 of Chapter 1. De nition 3.1.2. Extensions of preferential models are de ned by specifying the fol-lowing conditions [28]:
Normality: For all x 2 W , Wx is non-empty.
Total re exivity: For all x 2 W it holds that x 2 Wx.
Weak centering: For all x 2 W , for all y 2 Wx, it holds that x x y.
Centering: For all x 2 W , for all y 2 Wx, it holds that x x y and if there is w 2 Wx such that for all y 2 Wx, w x y, then w = x.
Local uniformity: For all x 2 W , for all y 2 Wx it holds that Wy = Wx.
Local absoluteness: For all x 2 W , for all y 2 Wx it holds that Wy = Wx and for all w1; w2 2 Wx we have w1 x w2 if and only if w1 y w2. Connectedness: For all x 2 W , for all w1; w2 2 Wx it holds that w1 x w2 or w2 x w1.
Table of contents :
Introduction
1 Conditional logics: a gentle introduction
1.1 Conditionals in natural language
1.2 Truth-functional implication
1.3 Possible worlds account of conditionals
1.4 A semantic account
1.5 An axiomatic account
1.6 Conditional logics and modal logics
1.7 Problems of the possible worlds account of conditionals
1.A Appendix: Modal logics
2 Proof methods for modal and conditional logics
2.1 Structural proof theory
2.2 The sequent calculus G3cp
2.3 Desirable properties of sequent calculus
2.4 Sequent calculi for modal logics
2.5 A semantic approach
2.6 A syntactic approach
2.7 To conclude
2.8 State of the art
3 Labelled sequent calculi for PCL and extensions
3.1 Preferential conditional logic
3.2 From preferential models to neighbourhood models (and back)
3.3 A family of labelled sequent calculi
3.4 Structural properties
3.5 Termination
3.6 Semantic completeness
3.7 Nesting
3.8 Absoluteness
3.9 To conclude
3.A Appendix: derivations of the axioms
4 Internal calculi for Lewis’ conditional logics
4.1 Lewis’ family of conditional logics
4.2 Nested sequent calculi for basic systems
4.3 Cut elimination for IV
4.4 An invertible version: Ii Base
4.5 Semantic completeness
4.6 Logic VTU and extensions
4.7 Hypersequent calculi SHi Strong
4.8 Semantic completeness of SHi VTU, SHi VWU and SHi VCU
4.9 Head-hypersequents calculi HHi StrongA
4.10 Semantic completeness of HHi StrongA
4.11 To sum up
5 Relations between proof systems
5.1 A case study
5.2 Sequent calculi G3V and Ii
5.3 From the internal to the labelled sequent calculus
5.4 From the labelled to the internal calculus
5.5 To conclude
6 Conditional epistemic logics
6.1 Multi-agent modal epistemic logic
6.2 Axiomatization and semantics
6.3 Adequacy of the axiomatization
6.4 Sequent calculus G3CDL
6.5 Termination and completeness
6.6 Relating the old and the new
6.7 Other epistemic and doxastic modalities
6.8 To conclude
Conclusions
Bibliography
