Provability multilattice logic

ABSTRACT

In this paper, we introduce provability multilattice logic ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ and multilattice arithmetic ${\mathbf{M}\mathbf{P}\mathbf{A}}_n$ which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ has the provability interpretation with respect to ${\mathbf{M}\mathbf{P}\mathbf{A}}_n$ and prove the arithmetic completeness theorem for it. We formulate ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ in the form of a nested sequent calculus and show that cut is admissible in it. We introduce the notion of a provability multilattice and develop algebraic semantics for ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ on its basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ and establish the Kripke completeness theorem via syntactical and semantic embeddings from ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ into $\mathbf{G}\mathbf{L}$ and vice versa. Last but not least, the decidability of ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$ is shown.

KEYWORDS:

• Multilattice logic
• provability logic
• nested sequent calculus
• Peano arithmetic
• embedding theorem

Acknowledgments

I would like to thank an anonymous reviewer for useful comments.

Disclosure statement

No potential conflict of interest was reported by the author(s).

Notes

1 A relation R is conversely well-founded iff there are no infinite ascending sequences, that is sequences of the form $w_{1}R{w}_{2}R{w}_{3}R\dots$, where $w_1,w_2,w_3\in W$.

2 As follow from Poggiolesi (2011, Lemma 10.1), the first initial nested sequent can be generalised for any formula A: $\mathfrak{N}[A,\mathrm{\Gamma }\Rightarrow \mathrm{\Delta },A]$.

3 See Lemmas 10.2–10.5, 10.7 in Poggiolesi (2011) for the proofs. The names of the rules are read as follows: internal and external weakening, necessitation rule, and contraction. As follows from Lemma 10.6, all the propositional rules, the modal rules and the special logical rule are invertible.

4 These rules were suggested by Gallier (1986) and used by Negri and von Plato (2001) as well as Troelstra and Schwichtenberg (1996). For the discussion about sequent rules for equality as well as for a new approach to it see Indrzejczak's paper (Indrzejczak, 2021).

5 This nested sequent formulation of PA is obviously far from being proof-theoretically impeccable, but we need it for technical reasons: for the syntactical embedding of ${\mathbf{M}\mathbf{P}\mathbf{A}}_n$ into ${\mathbf{P}\mathbf{A}}_n$ and vice versa which is needed for the proof of the arithmetical completeness theorem for ${\mathbf{P}\mathbf{M}\mathbf{L}}_n$. For a more proof-theoretically perfect sequent formulation of PA (based yet on a non-standard version of Gentzen's LK) see Ramanayake's paper (Ramanayake, 2016).

6 Note that $(A_1{\wedge }_j\dots {\wedge }_j{A}_l){\to }_j(B_1{\vee }_j\dots {\vee }_j{B}_m)$ can be replaced with ${\mathrm{\neg }}_k{\mathrm{\neg }}_j(A_1{\wedge }_j\dots {\wedge }_j{A}_l){\vee }_j(B_1{\vee }_j\dots {\vee }_j{B}_m)$ or ${\mathrm{\neg }}_k{\mathrm{\neg }}_j\left(\right(A_1{\wedge }_j\dots {\wedge }_j{A}_l\left){\wedge }_j{\mathrm{\neg }}_k{\mathrm{\neg }}_j\right(B_1{\vee }_j\dots {\vee }_j{B}_m\left)\right)$.

7 Kamide and Shramko (2017) call it paraconsistent valuation. We prefer the term paradefinite (i.e. both paraconsistent and paracomplete, see Arieli and Avron (2017)), since this valuation is not only paraconsistent, but paracomplete as well.

8 Again, in contrast to Kamide and Shramko (2017), by the same reasons we prefer the term paradefinite rather than paraconsistent.

9 Note that (I∪-elimination(I∪-elimination) $\begin{array}{rl}{I}_j\left({-}_k{-}_{j}a{\cup }_{j}b\right)& {⩽}_j{I}_j\left({-}_k{-}_{j}a\right){\cup }_j{C}_j\left(b\right).\end{array}$(I∪-elimination) ) is the algebraic version of the formula ${◻}_j\left(A{\to }_{j}B\right){\to }_j\left({◊}_{j}A{\to }_j{◊}_{j}B\right)$.

Additional information

Funding

The research is supported by Russian Science Foundation [grant number 21-18-00195].