Provability multilattice logic.

In this paper, we introduce provability multilattice logic P M L n and multilattice arithmetic M P A n which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that P M L n has the provability interpretation with respect to M P A n and prove the arithmetic completeness theorem for it. We formulate P M 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 P M L n on its basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for P M L n and establish the Kripke completeness theorem via syntactical and semantic embeddings from P M L n into G L and vice versa. Last but not least, the decidability of P M L n is shown. [ABSTRACT FROM AUTHOR]