R-CALCULUS, II: Many-Valued Logics

LI Wei and SUI Yuefei

Springer 2022, ISBN 978-981-16-9293-2

PREFACE

R-Calculus for PL | Springer Nature Link

R-calculus is a Gentzen-type deduction system which is nonmonotonic, and is a concrete belief revision   operator which is proved to satisfy the AGM postulates and the DP postulates. This book is to show that in many-valued logics, each R-calculus is a combination of one monotonic tableau proof system and one nonmonotonic one. We consider R-calculi in propositional logic, description logic, threevalued logic, B2 2 -valued propositional logic. For each value ∗, 

• there is a monotonic tableau proof system T^∗ and a nonmonotonic tableau proof system S∗, which compose of an R-calculus R∗; and 

• there is a  monotonic tableau proof system T∗ and a nonmonotonic tableau proof system S ^∗ , which compose of an R-calculus R^∗ . Hence, each R-calculus is nonmonotonic. We also consider the product and sum of two logics. 

For product, we will show that 

  (i) at the value-level, B2² -valued PL is the product of two B2-valued PL; 

  (ii) at the logical level, each tableau proof system in B2² -valued PL is the product of two tableau proof systems in B2-valued PL, and 

  (iii) at the revision level, each R-calculus in B2 ² -valued PL is the product of two R-calculi in B2-valued PL. 

 For sum without common element, we will show that 

   (i) L3-valued PL is the sum of two B2-valued PL; 

  (ii) each tableau proof system in L3-valued PL is the sum of two tableau proof systems in B2-valued PL, and 

  (iii) each R-calculus in L3-valued PL is the sum of two R-calculi in B2- valued PL; 

 and for sum with common element, we will show that 

  (iv) L4-valued PL is the sum of two B2-valued PL; 

  (v) each tableau proof system in L4-valued PL is the sum of two tableau proof systems in B2-valued PL, and

 (vi) each R-calculus in L₄-valued PL is the sum of two R-calculi in B2- valued PL; 

 We consider the algebraical and logical properties of tableau proof systems and R-calculi in many-valued logics. We wish that the contents in this book will inspire new ideas in logical research of this century. 

Li Wei, Sui Yuefei 

2018,9,30

Contents

1 Introduction 10

  1.1 R-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

  1.2 Many-valued logics . . . . . . . . . . . . . . . . . . . . . . . . 11

  1.3 Contents in the first volume . . . . . . . . . . . . . . . . . . . 12

  1.4 Contents in this volume . . . . . . . . . . . . . . . . . . . . . 15

  1.5 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

2 R-Calculus For PL 22

  2.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 23

  2.2 Monotonic tableau proof systems . . . . . . . . . . . . . . . . 24

    2.2.1 Tableau proof system T^f. . . . . . . . . . . . . . . . 24

    2.2.2 Tableau proof system T^t. . . . . . . . . . . . . . . . 27

  2.3 Nonmonotonic tableau proof systems . . . . . . . . . . . . . . 29

    2.3.1 Tableau proof system S^t. . . . . . . . . . . . . . . . . 30

    2.3.2 Tableau proof system S^f. . . . . . . . . . . . . . . . . 32

  2.4 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

    2.4.1 R-calculus R^t. . . . . . . . . . . . . . . . . . . . . . . 34

    2.4.2 R-calculus R^f. . . . . . . . . . . . . . . . . . . . . . . 38

  2.5 Projecting R-calculi to tableau proof systems . . . . . . . . . 39

  2.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40

3 R-Calculus For Description Logic 42

  3.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 43

  3.2 Monotonic tableau proof systems . . . . . . . . . . . . . . . . 45

    3.2.1 Tableau proof system T^t . . . . . . . . . . . . . . . . 45

    3.2.2 Tableau proof system T^f . . . . . . . . . . . . . . . . 48

  3.3 Nonmonotonic tableau proof systems . . . . . . . . . . . . . . 49

    3.3.1 Tableau proof system S^t. . . . . . . . . . . . . . . . . 49

    3.3.2 Tableau proof system S^f. . . . . . . . . . . . . . . . . 52

  3.4 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53

    3.4.1 R-calculus R^t. . . . . . . . . . . . . . . . . . . . . . . 53

    3.4.2 R-calculus R^f. . . . . . . . . . . . . . . . . . . . . . . 55

  3.5 Projecting R-calculi to tableau proof systems . . . . . . . . . 57

4 R-Calculus For L₃-Valued PL 61

  4.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 62

  4.2 Monotonic tableau proof systems . . . . . . . . . . . . . . . . 65

    4.2.1 Tableau proof system T_t . . . . . . . . . . . . . . . . 65

    4.2.2 Tableau proof system T_m . . . . . . . . . . . . . . . . 66

    4.2.3 Tableau proof system T_f . . . . . . . . . . . . . . . . 67

  4.3 Nonmonotonic tableau proof systems . . . . . . . . . . . . . . 68

    4.3.1 Tableau proof system S^t. . . . . . . . . . . . . . . . . 70

    4.3.2 Tableau proof system S^m. . . . . . . . . . . . . . . . . 70

    4.3.3 Tableau proof system S^f. . . . . . . . . . . . . . . . . 71

  4.4 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

    4.4.1 R-calculus R^t. . . . . . . . . . . . . . . . . . . . . . . 73

    4.4.2 R-calculus R^m. . . . . . . . . . . . . . . . . . . . . . . 75

    4.4.3 R-calculus R^f. . . . . . . . . . . . . . . . . . . . . . . 77

  4.5 Satisfiability and unsatisfiability . . . . . . . . . . . . . . . . 79

    4.5.1 t-satisfiability and t-unsatisfiability . . . . . . . . . . 80

    4.5.2 m-satisfiability and m-unsatisfiability . . . . . . . . . . 81

    4.5.3 f-satisfiability and f-unsatisfiability . . . . . . . . . . 82

  4.6 Projecting R-calculi to tableau proof systems . . . . . . . . . 84

  4.7 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86

5 R-Calculus For L₃-Valued PL,II 89

  5.1 Monotonic tableau proof systems . . . . . . . . . . . . . . . . 89

    5.1.1 Tableau proof system T^t. . . . . . . . . . . . . . . . 90

    5.1.2 Tableau proof system T^m. . . . . . . . . . . . . . . . 91

    5.1.3 Tableau proof system T^f. . . . . . . . . . . . . . . . 92

  5.2 Nonmonotonic tableau proof systems . . . . . . . . . . . . . . 93

    5.2.1 Tableau proof system S_t . . . . . . . . . . . . . . . . . 93

    5.2.2 Tableau proof system S_m . . . . . . . . . . . . . . . . . 94

    5.2.3 Tableau proof system S_f . . . . . . . . . . . . . . . . . 95

  5.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 96

    5.3.1 R-calculus R_t . . . . . . . . . . . . . . . . . . . . . . . 96

    5.3.2 R-calculus R_m . . . . . . . . . . . . . . . . . . . . . . . 98

    5.3.3 R-calculus R_f . . . . . . . . . . . . . . . . . . . . . . . 100

  5.4 Validity and invalidity . . . . . . . . . . . . . . . . . . . . . . 102

    5.4.1 t-invalidity and t-validity . . . . . . . . . . . . . . . . 102

    5.4.2 m-invalidity and m-validity . . . . . . . . . . . . . . . . 104

    5.4.3 f-invalidity and f-validity . . . . . . . . . . . . . . . . 106

  5.5 Projecting R-calculi to tableau proof systems . . . . . . . . . 107

6 R-Calculus For B22-Valued PL 110

  6.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 112

  6.2 Monotonic tableau proof systems . . . . . . . . . . . . . . . . 113

    6.2.1 Tableau proof system T_t . . . . . . . . . . . . . . . . 115

    6.2.2 Tableau proof system T_⊤ . . . . . . . . . . . . . . . . 116

    6.2.3 Tableau proof system T_⊥ . . . . . . . . . . . . . . . . 118

    6.2.4 Tableau proof system T_f . . . . . . . . . . . . . . . . 119

  6.3 Nonmonotonic tableau proof systems . . . . . . . . . . . . . . 121

    6.3.1 Tableau proof system S^t. . . . . . . . . . . . . . . . . 123

    6.3.2 Tableau proof system S^⊤ . . . . . . . . . . . . . . . . 125

    6.3.3 Tableau proof system S^⊥ . . . . . . . . . . . . . . . . 126

    6.3.4 Tableau proof system S^f. . . . . . . . . . . . . . . . . 127

  6.4 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 129

    6.4.1 R-calculus R^t. . . . . . . . . . . . . . . . . . . . . . . 129

    6.4.2 R-calculus R^⊤ . . . . . . . . . . . . . . . . . . . . . . 132

    6.4.3 R-calculus R^⊥ . . . . . . . . . . . . . . . . . . . . . . 136

    6.4.4 R-calculus R^f. . . . . . . . . . . . . . . . . . . . . . . 139

  6.5 Projecting R-calculi to tableau proof systems . . . . . . . . . 142

  6.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145

7 R-Calculus For B²₂-Valued PL,II 147

  7.1 Monotonic tableau proof systems T^∗1∗2. . . . . . . . . . . . 149

    7.1.1 Tableau proof system T^t⊤ . . . . . . . . . . . . . . . . 152

    7.1.2 Tableau proof system T^t⊥ . . . . . . . . . . . . . . . . 153

    7.1.3 Tableau proof system T_t⊤ . . . . . . . . . . . . . . . . 155

    7.1.4 Tableau proof system T_t⊥ . . . . . . . . . . . . . . . . 157

  7.2 Nonmonotonic tableau proof systems . . . . . . . . . . . . . . 158

    7.2.1 Tableau proof system S^t⊤ . . . . . . . . . . . . . . . . 158

    7.2.2 Tableau proof system S^t⊥ . . . . . . . . . . . . . . . . 159

    7.2.3 Tableau proof system S_t⊤ . . . . . . . . . . . . . . . . 160

    7.2.4 Tableau proof system S_t⊥ . . . . . . . . . . . . . . . . 161

  7.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 162

    7.3.1 R-calculus R^t⊤ . . . . . . . . . . . . . . . . . . . . . . 163

    7.3.2 R-calculus R^t⊥ . . . . . . . . . . . . . . . . . . . . . . 164

    7.3.3 R-calculus R^f⊤ . . . . . . . . . . . . . . . . . . . . . . 166

    7.3.4 R-calculus R^f⊥ . . . . . . . . . . . . . . . . . . . . . . 167

  7.4 Projecting R-calculi to tableau proof systems . . . . . . . . . 169

  7.5 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170

8 Co-R-Calculus For PL 173

  8.1 Co-R-calculi in propositional logic . . . . . . . . . . . . . . . 174

    8.1.1 Co-R-calculus U^t. . . . . . . . . . . . . . . . . . . . . 174

    8.1.2 Co-R-calculus U^f. . . . . . . . . . . . . . . . . . . . . 176

  8.2 Co-R-calculi in L₃-valued PL . . . . . . . . . . . . . . . . . . 178

    8.2.1 Co-R-calculus U^t. . . . . . . . . . . . . . . . . . . . . 178

    8.2.2 Co-R-calculus U^m. . . . . . . . . . . . . . . . . . . . . 181

    8.2.3 Co-R-calculus U^f. . . . . . . . . . . . . . . . . . . . . 183

  8.3 Co-R-calculi in B²₂-valued propositional logic . . . . . . . . . 185

    8.3.1 Co-R-calculus U^t₄. . . . . . . . . . . . . . . . . . . . . 186

  8.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 190

9 Product of Two R-Calculi 192

  9.1 Tableau proof systems in modalized PL . . . . . . . . . . . . 193

    9.1.1 Monotonic tableau proof systems P^t₂/P^f₂. . . . . . . . 194

    9.1.2 Nonmonotonic tableau proof systems Q^t₂/Q^f₂. . . . . 194

  9.2 Product of B₂-valued PLs . . . . . . . . . . . . . . . . . . . . 195

    9.2.1 Tableau proof system P^t₄. . . . . . . . . . . . . . . . 198

    9.2.2 Tableau proof system P_t⁴. . . . . . . . . . . . . . . . 200

    9.2.3 Tableau proof system Q^t₄. . . . . . . . . . . . . . . . 205

  9.3 Product of two R-calculi . . . . . . . . . . . . . . . . . . . . . 208

    9.3.1 R-calculi R^t₂ and R^f₂. . . . . . . . . . . . . . . . . . . 208

    9.3.2 R-calculus U^t₄. . . . . . . . . . . . . . . . . . . . . . . 209

  9.4 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 213

10 Sum of Two R-Calculi 220

  10.1 The sum with one common element . . . . . . . . . . . . . . 221

    10.1.1 B₂[f, m] ⊕ B₂[m, t] . . . . . . . . . . . . . . . . . . . . 221

    10.1.2 Operators on tableau proof systems . . . . . . . . . . 222

    10.1.3 Sum of tableau proof systems . . . . . . . . . . . . . . 224

  10.2 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 226

    10.2.1 R-calculi in PL . . . . . . . . . . . . . . . . . . . . . . 226

    10.2.2 R-calculi R^∗₃. . . . . . . . . . . . . . . . . . . . . . . 228

  10.3 L₄-valued PL . . . . . . . . . . . . . . . . . . . . . . . . . . . 230

    10.3.1 Tableau proof system T^t₄. . . . . . . . . . . . . . . . 232

    10.3.2 Tableau proof system T⊤₄. . . . . . . . . . . . . . . . 234

    10.3.3 Tableau proof system T^⊥₄. . . . . . . . . . . . . . . . 235

    10.3.4 Tableau proof system T^f₄. . . . . . . . . . . . . . . . 237

  10.4 Sum of tableau proof systems . . . . . . . . . . . . . . . . . . 238

    10.4.1 T^t₄ =∼²(T^t₂) ⊕ T^t₂. . . . . . . . . . . . . . . . . . . . 238

    10.4.2 T⁴_t = T²_⊥ ⊕ T²_t. . . . . . . . . . . . . . . . . . . . . . 240

    10.4.3 S^t₄= S^⊥₂ ⊕ S^t₂. . . . . . . . . . . . . . . . . . . . . . . 241

  10.5 Sum of R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . 243

    10.5.1 R^t₄ ≡ R^⊥₂ ⊕ R^t₂. . . . . . . . . . . . . . . . . . . . . . 243

  10.6 Notes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246