ABSTRACT
In this paper, we introduce provability multilattice logic and multilattice arithmetic
which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that
has the provability interpretation with respect to
and prove the arithmetic completeness theorem for it. We formulate
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
on its basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for
and establish the Kripke completeness theorem via syntactical and semantic embeddings from
into
and vice versa. Last but not least, the decidability of
is shown.
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 , where
.
2 As follow from Poggiolesi (Citation2011, Lemma 10.1), the first initial nested sequent can be generalised for any formula A: .
3 See Lemmas 10.2–10.5, 10.7 in Poggiolesi (Citation2011) 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 (Citation1986) and used by Negri and von Plato (Citation2001) as well as Troelstra and Schwichtenberg (Citation1996). For the discussion about sequent rules for equality as well as for a new approach to it see Indrzejczak's paper (Indrzejczak, Citation2021).
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 into
and vice versa which is needed for the proof of the arithmetical completeness theorem for
. 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, Citation2016).
6 Note that can be replaced with
or
.
7 Kamide and Shramko (Citation2017) call it paraconsistent valuation. We prefer the term paradefinite (i.e. both paraconsistent and paracomplete, see Arieli and Avron (Citation2017)), since this valuation is not only paraconsistent, but paracomplete as well.
8 Again, in contrast to Kamide and Shramko (Citation2017), by the same reasons we prefer the term paradefinite rather than paraconsistent.
9 Note that (EquationI∪-elimination(I∪-elimination)
(I∪-elimination) ) is the algebraic version of the formula
.