This paper treats a kind of a modal logic based on the intuitionistic propositional logic which arose from the provability predicate in the first order arithmetic. The semantics of this calculus is presented in both a relational and an algebraic way.Completeness theorems, existence of a characteristic model and of a characteristic frame, properties of FMP and FFP and decidability are proved.

We make use of a Theorem of Burris-McKenzie to prove that the only decidable variety of diagonalizable algebras is that defined by 0=1. Any variety containing an algebra in which 01 is hereditarily undecidable. Moreover, any variety of intuitionistic diagonalizable algebras is undecidable.

I give several characterizations of the set V₀ proposed in [3] as the set of meaningful and true sentences of first order arthimetic, and show that in Peano arithmetic the Σ₂ completeness of V₀ is provable.

I give several characterizations of the set V₀ proposed in [3] as the set of meaningful and true sentences of first order arthimetic, and show that in Peano arithmetic the Σ₂ completeness of V₀ is provable.