Canonical rules.

*(English)*Zbl 1186.03045One of Friedman’s famous problems [see H. Friedman, J. Symb. Log. 40, 113–129 (1975; Zbl 0318.02002)] was whether admissibility of rules in intuitionistic logic is decidable. This problem was investigated seriously by Rybakov, whose results on admissibility are summarized in his book [V. V. Rybakov, Admissibility of logical inference rules. Studies in Logic and the Foundations of Mathematics. 136. Amsterdam: Elsevier (1997; Zbl 0872.03002)]. On the other hand, the concept of multiple-conclusion rules [D. J. Shoesmith and T. J. Smiley, Multiple-conclusion logic. Cambridge: Cambridge University Press (1978; Zbl 0381.03001); B. Boričić, J. Philos. Logic 14, 359–377 (1985; Zbl 0572.03033), Notre Dame J. Formal Logic 29, No. 4, 563–568 (1988; Zbl 0668.03010)] was developed in order to get an appropriate context for treating normalization in natural deduction for classical and superintuitionistic systems.

In this paper, the author develops certain frame-based multiple-conclusion rules, called the canonical rules, and establishes that every system of rules extending the modal logic K4 or Heyting propositional logic IPC can be axiomatized by canonical rules. The author applies this approach to admissible rules of basic transitive or linearly ordered logics (K4, S4, GL, IPC, K4.3, S4.3, GL.3) as well as all logics inheriting their admissible rules. It is shown that, for these logics, there exists a simple combinatorial criterion to recognize which canonical rules are admissible. An alternative proof of decidability of admissibility in each of these systems is obtained in this way, as well as a description of a basis of admissible rules. A new result, a dichotomy property, about admissible rules in these logics can be formulated as follows: every canonical rule is either admissible or equivalent to a rule without assumptions. The canonical rules are used to develop the theory of modal companions of intuitionistic rule systems and consequence relations, making it possible to get some of the well-known properties of modal companions of superintuitionistic logics. In the last section of the paper the author considers the generalization of canonical rules to nontransitive modal logics making it possible to give a description of splitting in the lattices of rule systems or consequence relations extending a given rule system with the finite model property. The canonical rules admissible in K are characterized, and a simple set of axioms from which they are derivable is presented.

In this paper, the author develops certain frame-based multiple-conclusion rules, called the canonical rules, and establishes that every system of rules extending the modal logic K4 or Heyting propositional logic IPC can be axiomatized by canonical rules. The author applies this approach to admissible rules of basic transitive or linearly ordered logics (K4, S4, GL, IPC, K4.3, S4.3, GL.3) as well as all logics inheriting their admissible rules. It is shown that, for these logics, there exists a simple combinatorial criterion to recognize which canonical rules are admissible. An alternative proof of decidability of admissibility in each of these systems is obtained in this way, as well as a description of a basis of admissible rules. A new result, a dichotomy property, about admissible rules in these logics can be formulated as follows: every canonical rule is either admissible or equivalent to a rule without assumptions. The canonical rules are used to develop the theory of modal companions of intuitionistic rule systems and consequence relations, making it possible to get some of the well-known properties of modal companions of superintuitionistic logics. In the last section of the paper the author considers the generalization of canonical rules to nontransitive modal logics making it possible to give a description of splitting in the lattices of rule systems or consequence relations extending a given rule system with the finite model property. The canonical rules admissible in K are characterized, and a simple set of axioms from which they are derivable is presented.

Reviewer: Branislav Boričić (Beograd)

Full Text:
DOI

##### References:

[1] | Modal logic 35 (1997) · Zbl 0871.03007 |

[2] | On the admissible rules of intuitionistic propositional logic 66 pp 281– (2001) |

[3] | DOI: 10.1007/BF02259858 · Zbl 0782.03005 |

[4] | Canonical formulas for K4. Part I: Basic results 57 pp 1377– (1992) · Zbl 0774.03005 |

[5] | On the degree of incompleteness in modal logics and the covering relation in the lattice of modal logics (1978) |

[6] | DOI: 10.1070/SM1991v068n01ABEH002104 · Zbl 0709.03017 |

[7] | ACM Transactions on Computational Logic 9 (2008) |

[8] | Handbook of modal logic 3 (2007) |

[9] | DOI: 10.1006/jsco.2000.0426 · Zbl 0970.68166 |

[10] | DOI: 10.1002/malq.19960420113 · Zbl 0858.03019 |

[11] | DOI: 10.1007/11753728_33 · Zbl 1185.03022 |

[12] | DOI: 10.1093/logcom/exi025 · Zbl 1091.03002 |

[13] | Logical consecutions in discrete linear temporal logic 70 pp 1137– (2005) · Zbl 1110.03010 |

[14] | Admissibility of logical inference rules 136 (1997) |

[15] | DOI: 10.1007/BF02021134 · Zbl 0453.03017 |

[16] | DOI: 10.1007/BF01463150 · Zbl 0315.02027 |

[17] | Einführung in die operative Logik und Mathematik 78 (1955) · Zbl 0066.24802 |

[18] | DOI: 10.1305/ndjfl/1012429722 |

[19] | DOI: 10.1007/BF00370158 · Zbl 0732.03012 |

[20] | Commentationes Mathematicae Universitatis Carolinae 8 pp 432– (1967) |

[21] | DOI: 10.1093/jigpal/jzn004 · Zbl 1146.03008 |

[22] | DOI: 10.1007/s00153-006-0028-9 · Zbl 1115.03010 |

[23] | DOI: 10.1016/j.apal.2006.04.001 · Zbl 1101.03038 |

[24] | DOI: 10.1093/logcom/exi029 · Zbl 1077.03011 |

[25] | Mathematics of the USSR, Doklady 4 pp 1203– (1963) |

[26] | DOI: 10.1007/s00153-006-0320-8 · Zbl 1096.03025 |

[27] | DOI: 10.1305/ndjfl/1107220674 · Zbl 1102.03032 |

[28] | Logics containing K4, Part 11 50 pp 619– (1985) |

[29] | Theoria 40 pp 110– (1974) |

[30] | Logical inference. Proceedings of the USSR symposium on the theory of logical inference pp 147– (1979) |

[31] | Canonical formulas for K4. Part III: the finite model property 62 pp 950– (1997) |

[32] | The theory of ultrafilters 211 (1974) |

[33] | DOI: 10.1016/S0168-0072(99)00032-9 · Zbl 0949.03010 |

[34] | Unification in intuitionistic logic 64 pp 859– (1999) · Zbl 0930.03009 |

[35] | One hundred and two problems in mathematical logic 40 pp 113– (1975) |

[36] | Canonical formulas for K4. Part IT. Cofinalsubframe logics 61 pp 421– (1996) |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.