R-CALCULUS, III: Post Three-Valued Logic

LI Wei and SUI Yuefei

Springer 2022, ISBN 978-981-19-4269-3

 R-Calculi for Post Three-Valued Logic | Springer Nature Link

PREFACE

Post three-valued logic has sound and complete tableau proof systems, Gentzen deduction systems for sequents and Gentzen-typed deduction systems for multisequents, which other three-valued logics do not have. For Post three-valued logic there are deduction systems at different levels: at the theory level, at the sequent level and at the multisequent level. At each level, the validity has complementary validity and dual validity, and correspondingly there are sound and complete deduction systems for validity, co-validity and dual validity, respectively. Correspondingly, there are R-calculi at the three levels. At each level, an R-calculus has a complementary R-calculus and a dual R-calculus, which are proved to be sound and complete. Therefore, we have the following table for all levels of deduction systems and R-calculi:

deduction dual deduction R-calculus dual R-calculus

theories T^∗ [=]  S ^∗ [≠] R^∗ [=] Q^∗ [≠]

T_∗(≠) S_∗(=) R_∗(≠) Q_∗(=)

sequents G^∗ [≠ ∨ =] F ^∗ [= ∨ ≠] E^∗ [≠ ∨ =] D^∗ [= ∨ ≠]

G_∗(= ∨ ≠) F_∗(≠ ∨ =) E_∗(= ∨ ≠) D_∗(≠ ∨ =)

multisequents M ⁼L ^≠ K ⁼J ^≠

M≠ L= K≠ J=

where ∗ ∈ {t, m, f}, [=] denotes the revision preserving validity and (=) denotes the revision preserving satisfiability.

Other kinds of multisequents are considered. For uniform quantifiers, there are eight kinds of validities and R-calculi:

M⁼ _QQQ,L ^≠ _QQQ , K ⁼_QQQ, J ^≠ QQQ

M^QQQ _≠ ,L ^QQQ ₌ , K ^QQQ _≠ , J ^QQQ ₌

As quantifiers are not uniform, there are many kinds of validities and R-calculi:

M⁼ _Q1Q2Q3 ,L ^≠ _Q1Q2Q3 , K ⁼_Q1Q2Q3 , J ^≠ _Q1Q2Q3

M^Q1Q2Q3 _≠ ,L ^Q1Q2Q3 = , K ^Q1Q2Q3 _≠ , J ^Q1Q2Q3 =

These deduction systems and R-calculi will be proved to be sound and complete.

Li Wei, Sui Yuefei

2021,10,30

Contents

1 Introduction 10

1.1 Three-valued logics . . . . . . . . . . . . . . . . . . . . . . . . 10

1.2 Deduction systems . . . . . . . . . . . . . . . . . . . . . . . . 11

1.3 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

1.4 More . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

1.5 Basic definitions . . . . . . . . . . . . . . . . . . . . . . . . . 19

1.5.1 Post three-valued logic . . . . . . . . . . . . . . . . . . 19

1.5.2 Post three-valued description logic . . . . . . . . . . . 23

1.5.3 Remarks . . . . . . . . . . . . . . . . . . . . . . . . . . 31

1.6 Types of deduction rules . . . . . . . . . . . . . . . . . . . . . 33

1.7 Notations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41

2 Many-Placed Sequents 44

2.1 Zach’s Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . 44

2.2 Analysis of Zach’s theorem . . . . . . . . . . . . . . . . . . . 49

2.3 Tableau proof systems . . . . . . . . . . . . . . . . . . . . . . 52

2.3.1 Tableau proof system T^t. . . . . . . . . . . . . . . . 52

2.3.2 Tableau proof system T^m. . . . . . . . . . . . . . . . 53

2.3.3 Tableau proof system T^f. . . . . . . . . . . . . . . . 5

2.4 Incompleteness of deduction system T’’. . . . . . . . . . . . 54

3 Modalized Three-Valued Logics 56

3.1 Bochvar three-valued logic . . . . . . . . . . . . . . . . . . . . 56

3.1.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . 56

3.1.2 Multisequent deduction system M^b . . . . . . . . . . 58

3.2 Kleene three-valued logic . . . . . . . . . . . . . . . . . . . . . 60

3.2.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . 60

3.2.2 Gentzen deduction system G^k. . . . . . . . . . . . . 61

3.3 L ukasiewicz’s three-valued logic . . . . . . . . . . . . . . . . . 63

3.3.1 Basic definitions . . . . . . . . . . . . . . . . . . . . . 63

3.3.2 Tableau proof system T^l. . . . . . . . . . . . . . . . . 64

4 Post three-valued logic 71

4.1 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

4.1.1 Tableau proof system T^t. . . . . . . . . . . . . . . . 72

4.1.2 Tableau proof system T^m. . . . . . . . . . . . . . . . 73

4.1.3 Tableau proof system T^f. . . . . . . . . . . . . . . . 74

4.1.4 Transformations . . . . . . . . . . . . . . . . . . . . . 75

4.1.5 Tableau proof system T_t . . . . . . . . . . . . . . . . 77

4.1.6 Tableau proof system T_m . . . . . . . . . . . . . . . . 78

4.1.7 Tableau proof system T_f . . . . . . . . . . . . . . . . 79

4.2 Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79

4.2.1 Gentzen deduction system G^t. . . . . . . . . . . . . . 80

4.2.2 Gentzen deduction system G^m. . . . . . . . . . . . . . 81

4.2.3 Gentzen deduction system G^f. . . . . . . . . . . . . . 83

4.2.4 Gentzen deduction system G_t . . . . . . . . . . . . . . 84

4.2.5 Gentzen deduction system G_m . . . . . . . . . . . . . . 86

4.2.6 Gentzen deduction system G_f . . . . . . . . . . . . . . 87

4.3 Multisequents . . . . . . . . . . . . . . . . . . . . . . . . . . . 89

4.3.1 Gentzen deduction system M⁼ . . . . . . . . . . . . . 91

4.3.2 simplified M⁼_s. . . . . . . . . . . . . . . . . . . . . . 96

4.3.3 Gentzen deduction system M_≠ . . . . . . . . . . . . . 99

4.3.4 Simplified M^s_≠. . . . . . . . . . . . . . . . . . . . . . 101

4.3.5 Cut elimination theorem . . . . . . . . . . . . . . . . . 102

5 R-Calculi for Post Three-valued logic 108

5.1 R-calculus for theories . . . . . . . . . . . . . . . . . . . . . . 109

5.1.1 R-calculus R^t. . . . . . . . . . . . . . . . . . . . . . . 109

5.1.2 R-calculus R_t . . . . . . . . . . . . . . . . . . . . . . . 111

5.2 R-calculi E^∗ for sequents . . . . . . . . . . . . . . . . . . . . . 114

5.2.1 R-calculus E^t. . . . . . . . . . . . . . . . . . . . . . . 114

5.2.2 R-calculus E_m . . . . . . . . . . . . . . . . . . . . . . . 120

5.2.3 Basic Theorems . . . . . . . . . . . . . . . . . . . . . . 124

5.3 R-calculi for multisequents . . . . . . . . . . . . . . . . . . . . 128

5.3.1 R-calculus K⁼ . . . . . . . . . . . . . . . . . . . . . . 129

5.3.2 Simplified K⁼_s. . . . . . . . . . . . . . . . . . . . . . . 134

5.3.3 R-calculus K_≠ . . . . . . . . . . . . . . . . . . . . . . 136

5.3.4 R-calculus K^s_≠. . . . . . . . . . . . . . . . . . . . . . 142

6 Post Three-valued description logic 146

6.1 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 146

6.1.1 Tableau proof system S^t. . . . . . . . . . . . . . . . . 147

6.1.2 Tableau proof system S_t . . . . . . . . . . . . . . . . . 148

6.2 Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149

6.2.1 Gentzen deduction system F^t. . . . . . . . . . . . . . 150

6.2.2 Gentzen deduction system F_t . . . . . . . . . . . . . . 152

6.3 Multisequents . . . . . . . . . . . . . . . . . . . . . . . . . . . 154

6.3.1 Gentzen deduction system L^≠ . . . . . . . . . . . . . . 155

6.3.2 simplied L^≠_s . . . . . . . . . . . . . . . . . . . . . . . . 159

6.3.3 Gentzen deduction system L₌ . . . . . . . . . . . . . . 160

6.3.4 Simplified L^s₌ . . . . . . . . . . . . . . . . . . . . . . . 163

7 R-calculi for Post three-valued description logic 166

7.1 R-calculus for theories . . . . . . . . . . . . . . . . . . . . . . 167

7.1.1 R-calculus Q^t. . . . . . . . . . . . . . . . . . . . . . . 167

7.1.2 R-calculus Q_t . . . . . . . . . . . . . . . . . . . . . . . 171

7.2 R-calculi for sequents . . . . . . . . . . . . . . . . . . . . . . . 175

7.2.1 R-calculus D^t. . . . . . . . . . . . . . . . . . . . . . . 176

7.2.2 R-calculus D_m . . . . . . . . . . . . . . . . . . . . . . . 184

7.3 R-calculi for multisequents . . . . . . . . . . . . . . . . . . . . 192

7.3.1 R-calculus J ^≠. . . . . . . . . . . . . . . . . . . . . . . 193

7.3.2 Simplified J^≠_s . . . . . . . . . . . . . . . . . . . . . . . 203

7.3.3 Simplified J₌ . . . . . . . . . . . . . . . . . . . . . . . 207

8 R-calculi for corner multisequents 212

8.1 Corner multisequents M⁼_QQQ . . . . . . . . . . . . . . . . . . 213

8.1.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 213

8.1.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 214

8.1.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 216

8.2 Corner multisequents M^≠_QQQ. . . . . . . . . . . . . . . . . . 217

8.2.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 217

8.2.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 218

8.2.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 220

8.3 R-calculi K⁼_QQQ/K^QQQ_≠. . . . . . . . . . . . . . . . . . . . . 221

8.3.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 221

8.3.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 222

8.3.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 226

8.4 R-calculi J^≠_QQQ/J^QQQ₌ . . . . . . . . . . . . . . . . . . . . . . 226

8.4.1 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . 227

8.4.2 Deduction rules . . . . . . . . . . . . . . . . . . . . . . 227

8.4.3 Deduction systems . . . . . . . . . . . . . . . . . . . . 230

9 General multisequents 232

9.1 General multisequents . . . . . . . . . . . . . . . . . . . . . . 234

9.2 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234

9.2.1 Axioms for M⁼/M_≠ . . . . . . . . . . . . . . . . . . . 235

9.2.2 Axioms for L^≠/L₌-validity . . . . . . . . . . . . . . . 241

9.3 Deduction rules . . . . . . . . . . . . . . . . . . . . . . . . . . 244

9.4 Deduction systems . . . . . . . . . . . . . . . . . . . . . . . . 249

10 R-calculi for general multisequents 252

10.1 R-calculi K⁼_Q1Q2Q3/K^Q1Q2Q3_≠/J^≠_Q1Q2Q3/J^Q1Q2Q3₌ . . . . . . . . 252

10.2 Axioms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 253

10.2.1 Axioms for K⁼ _Q1Q2Q3/K^Q1Q2Q3_≠. . . . . . . . . . . . . 254

10.2.2 Axioms for J^≠_Q1Q2Q3/J^Q1Q2Q3₌ . . . . . . . . . . . . . . 257

10.3 Deduction rules . . . . . . . . . . . . . . . . . . . . . . . . . . 260

10.3.1 R⁺₌ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 261

10.3.2 R⁺_≠. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 266

10.3.3 R⁻₌ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 271

10.3.4 R⁻_≠. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 275

10.4 Deduction systems . . . . . . . . . . . . . . . . . . . . . . . . 281