R-CALCULUS, IV: Propositional Logic

LI Wei and SUI Yuefei

Springer 2023, ISBN 978-981-19-8632-1

 R-Calculi for  $$\rightsquigarrow $$ -Propositional Logic | Springer Nature Link

PREFACE

Propositional logic is basic. R-calculus is a belief revision operator satisfying

AGM postulates. Combining propositional logic and R-calculus produces

a new point of view to consider belief revision.

   A sequent Γ ⇒ ∆ is valid if for any assignment v, either there is a

formula A false in v or there is a formula B ∈ ∆ true in v. There are variant

definitions of the validity of a sequent. For example, a sequent Γ ⇒ ∆

is G^Q1iQ2j-valid if for any assignment v, either Q₁A ∈ Γ(v(A) = i) or

Q₂B ∈ ∆(v(B) = j), where Q₁, Q₂ ∈ {A, E} and i, j ∈ {0, 1}.

   The negation of G^Q1iQ2j-validity is G_{Q1(1−i)Q2(1−j)}-validity, that is, a

co-sequent Γ↦∆ is G^Q1iQ2j -valid if there is an assignment v such that

Q₁A ∈ Γ(v(A) = i) and Q₂B ∈ ∆(v(B) = j). 

   There are sound and complete Gentzen deduction systems G^Q1iQ2j/G_Q1iQ2j

for G^Q1iQ2j/G_Q1iQ2j -validity, which are monotonic in Γ iff Q₁ = E, and

nonmonotonic in ∆ iff Q₂ = A.

   R-calculus is a Gentzen-typed deduction system which is nonmonotonic,

 and is a concrete belief revision operator which is proved to satisfy

AGM postulates and DP postulates. Corresponding to Gentzen deduction

 system G^Q1iQ2j/G_Q1iQ2j , there is a sound and complete R-calculus

R^Q1iQ2j/R_Q1iQ2j .

   R_Q1iQ2j preserves the ⊆-minimal change. Let R, Q, P denote the ⊆-,

≼- and ⊢_≼-minimal change, respectively. For any Y₁, Y₂ ∈ {R, Q, P}, there

are sound and complete R-calculi R^Y1Q1iY2Q2j and R_Y1Q1iY2Q2j .

   Applications of R-calculus in -propositional logic and logic of supersequents

are given.

Li Wei, Sui Yuefei

Contents

1 Introduction 10

1.1 Propositional logic . . . . . . . . . . . . . . . . . . . . . . . . 10

1.2 Variant deduction systems . . . . . . . . . . . . . . . . . . . . 11

1.3 R-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

1.4 R-calculi in this volume . . . . . . . . . . . . . . . . . . . . . 14

1.4.1 R-calculi for weak propositional logics . . . . . . . . . 14

1.4.2 R-calculi for tableau proof/Gentzen deduction systems 14

1.4.3 R-calculi for deduction systems G^Q1Q2 /G_Q1Q2. . . . 16

1.4.4 R-calculi for deduction systems G^Q1iQ2j/G_Q1iQ2j . . . 16

1.4.5 R-calculi for deduction systems G^Y1Q1iY2Q2j/G_Y1Q1iY2Q2j 17

1.5 Applications of R-calculi . . . . . . . . . . . . . . . . . . . . . 18

1.5.1 R-calculus for ↝-propositional logic . . . . . . . . . . 18

1.5.2 R-calculi for supersequents . . . . . . . . . . . . . . . 20

1.6 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21

 2 R-calculus for simplified propositional logics 24

2.1 Weak propositional logics . . . . . . . . . . . . . . . . . . . . 25

2.1.1 Gentzen deduction system G^¬ . . . . . . . . . . . . . 25

2.1.2 Gentzen deduction system G_¬ . . . . . . . . . . . . . 27

2.1.3 Gentzen deduction system G^∧ . . . . . . . . . . . . . 28

2.1.4 Gentzen deduction system G_∧ . . . . . . . . . . . . . 30

2.1.5 Gentzen deduction system G^∨ . . . . . . . . . . . . . 31

2.1.6 Gentzen deduction system G_∨ . . . . . . . . . . . . . 32

2.2 R-calculus for weak propositional logics . . . . . . . . . . . . 33

2.2.1 R-calculus R^¬ . . . . . . . . . . . . . . . . . . . . . . 34

2.2.2 R-calculus R_¬ . . . . . . . . . . . . . . . . . . . . . . 34

2.2.3 R-calculus R^∧ . . . . . . . . . . . . . . . . . . . . . . 35

2.2.4 R-calculus R_∧ . . . . . . . . . . . . . . . . . . . . . . 36

2.2.5 R-calculus R^∨ . . . . . . . . . . . . . . . . . . . . . . 37

2.2.6 R-calculus R_∨ . . . . . . . . . . . . . . . . . . . . . . 38

2.3 Variant propositional logics . . . . . . . . . . . . . . . . . . . 39

2.3.1 Gentzen deduction system G^¬→ . . . . . . . . . . . . 39

2.3.2 Gentzen deduction system _G¬→ . . . . . . . . . . . . 43

2.3.3 Gentzen deduction system G^⊗⊕ . . . . . . . . . . . . 44

2.3.4 Gentzen deduction system G_⊕⊗ . . . . . . . . . . . . 50

2.4 R-calculi for variant propositional logics . . . . . . . . . . . . 51

2.4.1 R-calculus R^¬→ . . . . . . . . . . . . . . . . . . . . . 51

2.4.2 R-calculus R_¬→ . . . . . . . . . . . . . . . . . . . . . 53

2.4.3 R-calculus R^⊕⊗ . . . . . . . . . . . . . . . . . . . . . . 55

2.4.4 R-calculus R_⊕⊗ . . . . . . . . . . . . . . . . . . . . . . 58

 3 R-calculi for tableau/Gentzen deduction systems 62

3.1 Tableau proof systems . . . . . . . . . . . . . . . . . . . . . . 65

3.1.1 Tableau proof system T^f. . . . . . . . . . . . . . . . 67

3.1.2 Tableau proof system T_t. . . . . . . . . . . . . . . . 69

3.1.3 Tableau proof system T^t . . . . . . . . . . . . . . . . 71

3.1.4 Tableau proof system T_f . . . . . . . . . . . . . . . . 73

3.2 R-calculi for theories . . . . . . . . . . . . . . . . . . . . . . . 75

3.2.1 R-calculus S^f. . . . . . . . . . . . . . . . . . . . . . . 75

3.2.2 R-calculus S_t. . . . . . . . . . . . . . . . . . . . . . . 78

3.2.3 R-calculus S^t . . . . . . . . . . . . . . . . . . . . . . . 79

3.2.4 R-calculus S_f . . . . . . . . . . . . . . . . . . . . . . . 82

3.3 Gentzen deduction systems . . . . . . . . . . . . . . . . . . . 83

3.3.1 Gentzen deduction system G^t. . . . . . . . . . . . . . 84

3.3.2 Gentzen deduction system G^f. . . . . . . . . . . . . . 87

3.3.3 Gentzen deduction system G_t . . . . . . . . . . . . . . 88

3.3.4 Gentzen deduction system G_f . . . . . . . . . . . . . . 92

3.4 R-calculi for sequents . . . . . . . . . . . . . . . . . . . . . . . 93

3.4.1 R-calculus R^t. . . . . . . . . . . . . . . . . . . . . . . 93

3.4.2 R-calculus R^f. . . . . . . . . . . . . . . . . . . . . . . 96

3.4.3 R-calculus R_t . . . . . . . . . . . . . . . . . . . . . . . 98

3.4.4 R-calculus R_f . . . . . . . . . . . . . . . . . . . . . . . 103

3.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

 4 R-calculi R^Q1Q2 /R_Q1Q2 109

4.1 Gentzen deduction systems G^Q1Q2. . . . . . . . . . . . . . . 110

4.1.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 111

4.1.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 113

4.1.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 113

4.2 R-calculi R^Q1Q2. . . . . . . . . . . . . . . . . . . . . . . . . . 114

4.2.1 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 114

4.2.2 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 117

4.2.3 Deduction systems R^Q1Q2. . . . . . . . . . . . . . . . 119

4.3 Gentzen deduction systems G_Q1Q2. . . . . . . . . . . . . . . 122

4.3.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 122

4.3.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 123

4.3.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 123

4.4 R-calculi R_Q1Q2. . . . . . . . . . . . . . . . . . . . . . . . . . 124

4.4.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 124

4.4.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 126

4.4.3 Deduction systems R_Q1Q2. . . . . . . . . . . . . . . . 129

4.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 130

 5 R-calculi R^Q1iQ2j/R_Q1iQ2j 132

5.1 Gentzen deduction systems G^E0∗/G_E1∗ . . . . . . . . . . . . 134

5.1.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 134

5.1.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 136

5.1.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 137

5.1.4 Monotonicity of G^E0∗ and G_A1∗ . . . . . . . . . . . . 138

5.2 Gentzen deduction systems G^Q1iQ2j. . . . . . . . . . . . . . 140

5.2.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 141

5.2.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 146

5.2.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 147

5.3 R-calculi R^Q1iQ2j. . . . . . . . . . . . . . . . . . . . . . . . . 148

5.3.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 148

5.3.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 152

5.3.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 152

5.4 Gentzen deduction systems G_Q1iQ2j . . . . . . . . . . . . . . 153

5.4.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 153

5.4.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 156

5.4.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 157

5.5 R-calculi R_Q1iQ2j . . . . . . . . . . . . . . . . . . . . . . . . . 158

5.5.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 158

5.5.2 deduction rules . . . . . . . . . . . . . . . . . . . . . . 161

5.5.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 161

5.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162

 6 R-Calculi: R^Y1Q1iY2Q2j/R_Y1Q1iY2Q2j 166

6.1 Variant R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . 167

6.1.1 R-calculus R_t . . . . . . . . . . . . . . . . . . . . . . . 167

6.1.2 R-calculus R_f . . . . . . . . . . . . . . . . . . . . . . . 168

6.1.3 R-calculus Q_t . . . . . . . . . . . . . . . . . . . . . . . 169

6.1.4 R-calculus Q_f . . . . . . . . . . . . . . . . . . . . . . . 170

6.1.5 R-calculus P_t . . . . . . . . . . . . . . . . . . . . . . . 171

6.1.6 R-calculus P_f . . . . . . . . . . . . . . . . . . . . . . . 172

6.2 R-calculi R^Y1Q1iY2Q2j. . . . . . . . . . . . . . . . . . . . . . . 173

6.2.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 173

6.2.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 174

6.2.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 180

6.3 R-calculi R^Y1Q1iY2Q2j . . . . . . . . . . . . . . . . . . . . . . . 181

6.3.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 181

6.3.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 181

6.3.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . 181

6.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182

 7 R-calculi for supersequents 184

7.1 Supersequents . . . . . . . . . . . . . . . . . . . . . . . . . . . 186

7.1.1 Supersequent Gentzen deduction system G⁺ . . . . . 186

7.2 Reduction of supersequents to sequents . . . . . . . . . . . . 190

7.2.1 Gentzen deduction system G^ft. . . . . . . . . . . . . 190

7.2.2 Gentzen deduction system G^ff. . . . . . . . . . . . . 191

7.3 R-calculus R⁺ . . . . . . . . . . . . . . . . . . . . . . . . . . 192

7.3.1 R^ft. . . . . . . . . . . . . . . . . . . . . . . . . . . . 196

7.3.2 R^ff. . . . . . . . . . . . . . . . . . . . . . . . . . . . 199

7.4 Gentzen deduction system G₋ . . . . . . . . . . . . . . . . . 201

7.5 Reduction of supersequents to sequents . . . . . . . . . . . . 203

7.5.1 Gentzen deduction system G_ff . . . . . . . . . . . . . 203

7.5.2 Gentzen deduction system G_ft . . . . . . . . . . . . . 204

7.6 R-calculus R₋ . . . . . . . . . . . . . . . . . . . . . . . . . . 204

7.6.1 R_ff . . . . . . . . . . . . . . . . . . . . . . . . . . . . 209

7.6.2 R_ft . . . . . . . . . . . . . . . . . . . . . . . . . . . . 211

7.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213

 8 R-calculi for ↝-propositional logic 216

8.1 ↝-propositional logic . . . . . . . . . . . . . . . . . . . . . . . 217

8.1.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . 217

8.2 Tableau proof systems . . . . . . . . . . . . . . . . . . . . . . 218

8.2.1 T^t_↝. . . . . . . . . . . . . . . . . . . . . . . . . . . . 219

8.2.2 T^f_↝. . . . . . . . . . . . . . . . . . . . . . . . . . . . 220

8.2.3 Tableau proof systems T^↝ _t /T^↝_f. . . . . . . . . . . . . 221

8.3 R-calculi R^∗_↝. . . . . . . . . . . . . . . . . . . . . . . . . . . 222

8.3.1 R-calculus R^t_↝ . . . . . . . . . . . . . . . . . . . . . . 222

8.3.2 R-calculus R^f_↝ . . . . . . . . . . . . . . . . . . . . . . 225

8.4 Other minimal changes . . . . . . . . . . . . . . . . . . . . . . 228

8.4.1 R-calculus R^↝_t. . . . . . . . . . . . . . . . . . . . . . 229

8.4.2 R-calculus Q^↝_t. . . . . . . . . . . . . . . . . . . . . . 233

8.4.3 R-calculus P^↝_t. . . . . . . . . . . . . . . . . . . . . . 237

8.5 Gentzen deduction systems . . . . . . . . . . . . . . . . . . . 239

8.5.1 Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . 239

8.5.2 Gentzen deduction system G^t_↝ . . . . . . . . . . . . . 242

8.6 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246

8.6.1 R-calculus R_t . . . . . . . . . . . . . . . . . . . . . . . 246

8.6.2 R-calculus Q_t . . . . . . . . . . . . . . . . . . . . . . . 248

8.6.3 R-calculus P_t . . . . . . . . . . . . . . . . . . . . . . . 251

8.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 252