The purpose of this paper is to define a new logic $${\mathcal {SI}}$$ called semi-intuitionistic logic such that the semi-Heyting algebras introduced in [ 4 ] by Sankappanavar are the semantics for $${\mathcal {SI}}$$ . Besides, the intuitionistic logic will be an axiomatic extension of $${\mathcal {SI}}$$.

Provability, Computability and Reflection.

Semi-intuitionistic logic is the logic counterpart to semi-Heyting algebras, which were defined by H. P. Sankappanavar as a generalization of Heyting algebras. We present a new, more streamlined set of axioms for semi-intuitionistic logic, which we prove translationally equivalent to the original one. We then study some formulas that define a semi-Heyting implication, and specialize this study to the case in which the formulas use only the lattice operators and the intuitionistic implication. We prove then that all the logics thus (...) obtained are equivalent to intuitionistic logic, and give their Kripke semantics. (shrink)