Paraconsistent double negation as a modal operator

A paraconsistent modal-like logic, , is defined as a Gentzen-type sequent calculus. The modal operator in the modal logic can be simulated by the paraconsistent double negation in . Some theorems for embedding into a Gentzen-type sequent calculus for and vice versa are proved. The cut-elimination and completeness theorems for are also proved.