| Summary: | We axiomatize strictly positive fragments of modal logics with the confluence axiom. We consider unimodal logics such as <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi mathvariant="bold">K</mi><mo>.</mo><mn mathvariant="bold">2</mn></mrow></semantics></math></inline-formula>, <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi mathvariant="bold">D</mi><mo>.</mo><mn mathvariant="bold">2</mn></mrow></semantics></math></inline-formula>, <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi mathvariant="bold">D</mi><mn mathvariant="bold">4</mn><mo>.</mo><mn mathvariant="bold">2</mn></mrow></semantics></math></inline-formula> and <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mi mathvariant="bold">S</mi><mn mathvariant="bold">4</mn><mo>.</mo><mn mathvariant="bold">2</mn></mrow></semantics></math></inline-formula> with unimodal confluence <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo>⋄</mo><mo>□</mo><mi>p</mi><mo>→</mo><mo>□</mo><mo>⋄</mo><mi>p</mi></mrow></semantics></math></inline-formula> as well as the products of modal logics in the set <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mfenced separators="" open="{" close="}"><mi mathvariant="bold">K</mi><mo>,</mo><mi mathvariant="bold">D</mi><mo>,</mo><mi mathvariant="bold">T</mi><mo>,</mo><mi mathvariant="bold">D</mi><mn mathvariant="bold">4</mn><mo>,</mo><mi mathvariant="bold">S</mi><mn mathvariant="bold">4</mn></mfenced></semantics></math></inline-formula>, which contain bimodal confluence <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mo>⋄</mo><mn>1</mn></msub><msub><mo>□</mo><mn>2</mn></msub><mi>p</mi><mo>→</mo><msub><mo>□</mo><mn>2</mn></msub><msub><mo>⋄</mo><mn>1</mn></msub><mi>p</mi></mrow></semantics></math></inline-formula>. We show that the impact of the unimodal confluence axiom on the axiomatisation of strictly positive fragments is rather weak. In the presence of <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo>⊤</mo><mo>→</mo><mo>⋄</mo><mo>⊤</mo></mrow></semantics></math></inline-formula>, it simply disappears and does not contribute to the axiomatisation. Without <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo>⊤</mo><mo>→</mo><mo>⋄</mo><mo>⊤</mo></mrow></semantics></math></inline-formula> it gives rise to a weaker formula <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo>⋄</mo><mo>⊤</mo><mo>→</mo><mo>⋄</mo><mo>⋄</mo><mo>⊤</mo></mrow></semantics></math></inline-formula>. On the other hand, bimodal confluence gives rise to more complicated formulas such as <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><msub><mo>⋄</mo><mn>1</mn></msub><mi>p</mi><mo>∧</mo><msubsup><mo>⋄</mo><mn>2</mn><mi>n</mi></msubsup><mo>⊤</mo><mo>→</mo><msub><mo>⋄</mo><mn>1</mn></msub><mrow><mo>(</mo><mi>p</mi><mo>∧</mo><msubsup><mo>⋄</mo><mn>2</mn><mi>n</mi></msubsup><mo>⊤</mo><mo>)</mo></mrow></mrow></semantics></math></inline-formula> (which are superfluous in a product if the corresponding factor contains <inline-formula><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline"><semantics><mrow><mo>⊤</mo><mo>→</mo><mo>⋄</mo><mo>⊤</mo></mrow></semantics></math></inline-formula>). We also show that bimodal confluence cannot be captured by any <i>finite set</i> of strictly positive implications.
|
|---|