# Non-finitely axiomatisable modal product logics with infinite canonical axiomatisations

## TL;DR

This paper demonstrates that certain modal product logics, specifically Diff x Diff and its square version, cannot be finitely axiomatised but can be characterized by infinite sets of canonical Sahlqvist axioms, revealing limits of finite axiomatisability.

## Contribution

It provides the first examples of finitely axiomatisable modal logic products that are not finitely axiomatisable but can be axiomatized by infinite canonical axioms.

## Key findings

- Diff x Diff is non-finitely axiomatisable but has an infinite Sahlqvist axiomatisation.
- The square version of Diff x Diff is also non-finitely axiomatisable but admits an infinite Sahlqvist axiomatisation.
- These are the first known examples of such non-finitely axiomatisable product logics with explicit infinite axiomatizations.

## Abstract

Our concern is the axiomatisation problem for modal and algebraic logics that correspond to various fragments of two-variable first-order logic with counting quantifiers. In particular, we consider modal products with Diff, the propositional unimodal logic of the difference operator. We show that the two-dimensional product logic Diff x Diff is non-finitely axiomatisable, but can be axiomatised by infinitely many Sahlqvist axioms. We also show that its `square' version (the modal counterpart of the substitution and equality free fragment of two-variable first-order logic with counting to two) is non-finitely axiomatisable over Diff x Diff, but can be axiomatised by adding infinitely many Sahlqvist axioms. These are the first examples of products of finitely axiomatisable modal logics that are not finitely axiomatisable, but axiomatisable by explicit infinite sets of canonical axioms.