R-CALCULUS, VI: Finite Injury Method

LI Wei and SUI Yuefei

Springer 2025, ISBN978-981-99-6459-8

R-Calculus, VI: Finite Injury Priority Method | Springer Nature Link

Preface 

In the spring of 2014, we walked in Prof. Li’s garden. Since 2010 we worked in possible ways of developing R-calculus, almost to every decidable logic. Main problem is to decompose axiom of first-order logic into atomic form which is not decidable and seems impossible to decompose, where l is atomic. Suddenly Li asked me whether I knew the finite injury priority method. I asked him how he knew the method. He told me that Prof. Wang Wenqi once told him the story that two men Friedberg (US) and Muchnik (USSR) invented the method independently to solve Post problem in recursion theory. Prof. Li remembered how importance of this method in recursion theory and developed into more complex forms: infinite injury priority method, tree-construction, and so on. He asked me whether it is impossible to use this method to decompose the axiom. I told him that I studied recursion theory in my master and ph.D studies, and I thought it was possible.

  After two months, a paper was written, and submitted to and accepted by 2015 2nd International Conference on Artificial Intelligence (ICOAI2015).

  In this book, we will apply finite injury priority method to R-calculi and obtain (in)completeness theorem for binary-valued, Post three-valued, B²₂-valued and L₄-valued first-order logics,

and extend the method to infinite injury priority method and 0‘-method for default logic to produce pseudo-extensions of a default theory, corresponding to R-calculi R^t, S^t, Q_t and P_t :

and

  Li Wei, Sui Yuefei

            2023,6,30

Contents

1 Introduction 11

1.1 Validity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

1.2 R-calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

1.3 Variant maximally/minimally valid sets . . . . . . . . . . . . 15

1.3.1 Minimally M^t-valid sets . . . . . . . . . . . . . . . . . 16

1.3.2 Minimally N^t-valid sets . . . . . . . . . . . . . . . . . 17

1.3.3 Maximally L_t-valid sets . . . . . . . . . . . . . . . . . 17

1.3.4 Minimally K_t-valid sets . . . . . . . . . . . . . . . . . 18

1.4 Deduction systems . . . . . . . . . . . . . . . . . . . . . . . . 19

1.5 Finite injury priority method . . . . . . . . . . . . . . . . . . 20

1.6 Sequence R-calculi . . . . . . . . . . . . . . . . . . . . . . . . 24

1.6.1 R-calculus P _t . . . . . . . . . . . . . . . . . . . . . . . 24

1.6.2 R-calculus Q _t . . . . . . . . . . . . . . . . . . . . . . . 25

1.6.3 R-calculus S ^t. . . . . . . . . . . . . . . . . . . . . . . 26

1.6.4 R-calculus R ^t. . . . . . . . . . . . . . . . . . . . . . . 27

1.7 An Application to default logic . . . . . . . . . . . . . . . . . 27

1.7.1 Normal default theories . . . . . . . . . . . . . . . . . 27

1.7.2 Default theories . . . . . . . . . . . . . . . . . . . . . . 30

1.8 Notions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33

2 Finite injury priority method 36

2.1 Primitively recursive functions . . . . . . . . . . . . . . . . . 36

2.2 Turing machines . . . . . . . . . . . . . . . . . . . . . . . . . 38

2.3 Partially computable functions . . . . . . . . . . . . . . . . . 40

2.4 Relative Turing machines . . . . . . . . . . . . . . . . . . . . 41

2.5 Turing reducibility and Turing degrees . . . . . . . . . . . . . 41

2.6 Finite injury priority method . . . . . . . . . . . . . . . . . . 42

2.6.1 Post’s problem . . . . . . . . . . . . . . . . . . . . . . 43

2.6.2 Construction with oracle . . . . . . . . . . . . . . . . . 43

2.6.3 Finite injury priority method . . . . . . . . . . . . . . 44

3 Binary-valued first-order logic 48

3.1 R-calculus R^t_1/2. . . . . . . . . . . . . . . . . . . . . . . . . . 50

3.1.1 Deduction system M ^t_1/2. . . . . . . . . . . . . . . . . 50

3.1.2 R-calculus R ^t_1/2. . . . . . . . . . . . . . . . . . . . . . 51

3.1.3 Sequence R-calculus R ^t_1/2. . . . . . . . . . . . . . . . 54

3.2 R-calculus S ^t_1/2. . . . . . . . . . . . . . . . . . . . . . . . . . 55

3.2.1 Deduction system N ^t_1/2. . . . . . . . . . . . . . . . . 56

3.2.2 R-calculus S ^t_1/2 . . . . . . . . . . . . . . . . . . . . . 56

3.2.3 Sequence R-calculus S ^t_1/2. . . . . . . . . . . . . . . . 59

3.3 R-calculus Q _t^1/2. . . . . . . . . . . . . . . . . . . . . . . . . 60

3.3.1 Incomplete deduction system L _t^1/2. . . . . . . . . . . 61

3.3.2 R-calculus Q _t^1/2. . . . . . . . . . . . . . . . . . . . . . 61

3.3.3 Sequence R-calculus Q _t^1/2. . . . . . . . . . . . . . . . 64

3.4 R-calculus P _t^1/2. . . . . . . . . . . . . . . . . . . . . . . . . . 65

3.4.1 Incomplete deduction system K _t^1/2. . . . . . . . . . . 65

3.4.2 R-calculus P _t^1/2. . . . . . . . . . . . . . . . . . . . . . 66

3.4.3 Sequence R-calculus P _t^1/2. . . . . . . . . . . . . . . . 69

3.5 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70

3.6 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71

4 R-calculus for L₃-valued first-order logic 75

4.1 Post L₃-valued FOL . . . . . . . . . . . . . . . . . . . . . . . 78

4.2 R-calculus R ^t_1/3. . . . . . . . . . . . . . . . . . . . . . . . . . 80

4.2.1 Deduction system M ^t_1/3 . . . . . . . . . . . . . . . . 80

4.2.2 R-calculus R ^t_1/3. . . . . . . . . . . . . . . . . . . . . . 82

4.3 R-calculus S ^t_1/3. . . . . . . . . . . . . . . . . . . . . . . . . . 86

4.3.1 Deduction system N ^t_1/3 . . . . . . . . . . . . . . . . 86

4.3.2 R-calculus S ^t_1/3 . . . . . . . . . . . . . . . . . . . . . 87

4.4 R-calculus Q _t^1/3. . . . . . . . . . . . . . . . . . . . . . . . . 92

4.4.1 Incomplete deduction system L _t^1/3. . . . . . . . . . . 92

4.4.2 R-calculus Q _t^1/3. . . . . . . . . . . . . . . . . . . . . 93

4.5 R-calculus K _t^1/3. . . . . . . . . . . . . . . . . . . . . . . . . . 96

4.5.1 Incomplete deduction system K _t^1/3. . . . . . . . . . . 96

4.5.2 R-calculus P _t^1/3. . . . . . . . . . . . . . . . . . . . . 97

4.6 Sequence R-calculus . . . . . . . . . . . . . . . . . . . . . . . 99

4.7 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

4.8 Conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101

5 R-calculus for B₂₂-valued FOL 104

5.1 B₂₂-valued FOL . . . . . . . . . . . . . . . . . . . . . . . . . 107

5.2 R-calculus R⁼_4/22 . . . . . . . . . . . . . . . . . . . . . . . . . 110

5.2.1 Deduction system M⁼_4/22 . . . . . . . . . . . . . . . . . 111

5.2.2 R-calculus R⁼_4/22 . . . . . . . . . . . . . . . . . . . . . 113

5.2.3 σ ( R⁼⁰_4/22) = M⁼_4/22 ⊕ Q₌^4/22. . . . . . . . . . . . . . . . 117

5.3 R-calculus S⁼_4/22 . . . . . . . . . . . . . . . . . . . . . . . . . . 119

5.3.1 Deduction system N⁼_4/22 . . . . . . . . . . . . . . . . . 120

5.3.2 R-calculus S⁼_4/22 . . . . . . . . . . . . . . . . . . . . . 122

5.4 R-calculus Q₌^4/22 . . . . . . . . . . . . . . . . . . . . . . . . . 126

5.4.1 Incomplete Deduction system L₌^4/22 . . . . . . . . . . 127

5.4.2 R-calculus Q₌^4/22 . . . . . . . . . . . . . . . . . . . . . 129

5.5 R-calculus P₌^4/22 . . . . . . . . . . . . . . . . . . . . . . . . . 133

5.5.1 Incomplete Deduction system K₌^4/22. . . . . . . . . . 134

5.5.2 R-calculus P₌^4/22 . . . . . . . . . . . . . . . . . . . . . 136

5.6 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140

5.7 Sequence R-calculus . . . . . . . . . . . . . . . . . . . . . . . 142

5.8 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145

6 R-calculus for L₄-valued FOL 149

6.1 L₄-valued FOL . . . . . . . . . . . . . . . . . . . . . . . . . . 152

6.2 R-calculus R⁼_4/4 . . . . . . . . . . . . . . . . . . . . . . . . . . 155

6.2.1 Deduction system M⁼_4/4 . . . . . . . . . . . . . . . . . 156

6.2.2 R-calculus R⁼_4/4 . . . . . . . . . . . . . . . . . . . . . . 159

6.3 R-calculus S⁼_4/4 . . . . . . . . . . . . . . . . . . . . . . . . . . 162

6.3.1 Deduction system N⁼_4/4 . . . . . . . . . . . . . . . . . 163

6.3.2 R-calculus S⁼_4/4 . . . . . . . . . . . . . . . . . . . . . . 165

6.4 R-calculus Q₌^4/4 . . . . . . . . . . . . . . . . . . . . . . . . . . 169

6.4.1 Incomplete Deduction system L₌^4/4 . . . . . . . . . . . 170

6.4.2 R-calculus Q₌^4/4 . . . . . . . . . . . . . . . . . . . . . . 172

6.5 R-calculus P₌^4/4 . . . . . . . . . . . . . . . . . . . . . . . . . . 174

6.5.1 Incomplete Deduction system K₌^4/4 . . . . . . . . . . . 175

6.5.2 R-calculus P₌^4/4 . . . . . . . . . . . . . . . . . . . . . . 178

6.6 Sequence R-calculus . . . . . . . . . . . . . . . . . . . . . . . 180

6.7 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 182

7 Default logic: finite injury priority method 185

7.1 Basic properties of ⊨ . . . . . . . . . . . . . . . . . . . . . . . 186

7.2 Four kinds of Default logics . . . . . . . . . . . . . . . . . . . 187

7.3 Normal Default logics . . . . . . . . . . . . . . . . . . . . . . . 189

7.3.1 Default logic R^t . . . . . . . . . . . . . . . . . . . . . 191

7.3.2 Default logic S^t . . . . . . . . . . . . . . . . . . . . . . 193

7.3.3 Default logic Q_t . . . . . . . . . . . . . . . . . . . . . 195

7.3.4 Default logic P_t . . . . . . . . . . . . . . . . . . . . . 196

7.3.5 Examples . . . . . . . . . . . . . . . . . . . . . . . . . 198

7.4 Default logics . . . . . . . . . . . . . . . . . . . . . . . . . . . 199

7.4.1 Default logic R^t . . . . . . . . . . . . . . . . . . . . . 202

7.4.2 Default logic P_t . . . . . . . . . . . . . . . . . . . . . 205

7.4.3 Examples . . . . . . . . . . . . . . . . . . . . . . . . . 206

7.5 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 208

8 Default logic: tree construction 210

8.1 Tree constructions . . . . . . . . . . . . . . . . . . . . . . . . 210

8.1.1 Minimal pairs . . . . . . . . . . . . . . . . . . . . . . . 210

8.1.2 Promptly simple sets . . . . . . . . . . . . . . . . . . . 212

8.1.3 simultaneously interval permitting . . . . . . . . . . . 214

8.2 Normal default theory: Tree constructions . . . . . . . . . . . 217

8.2.1 Extensions of normal default theory: R^t . . . . . . . . 217

8.2.2 Extensions of normal default theory: P_t . . . . . . . . 220

8.3 Default theories . . . . . . . . . . . . . . . . . . . . . . . . . . 222

8.3.1 Extensions of default theory: S^t . . . . . . . . . . . . 223

8.3.2 Extensions of default theory: Q_t . . . . . . . . . . . . 225

8.4 Conclusions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 228