Provability, Computability and Reflection.

The goal of this two-part series of papers is to show that constructive logic with strong negation N is definitionally equivalent to a certain axiomatic extension NFL ew of the substructural logic FL ew . In this paper, it is shown that the equivalent variety semantics of N (namely, the variety of Nelson algebras) and the equivalent variety semantics of NFL ew (namely, a certain variety of FL ew -algebras) are term equivalent. This answers a longstanding question of Nelson [30]. (...) Extensive use is made of the automated theorem-prover Prover9 in order to establish the result. The main result of this paper is exploited in Part II of this series [40] to show that the deductive systems N and NFL ew are definitionally equivalent, and hence that constructive logic with strong negation is a substructural logic over FL ew. (shrink)

Motivated by an old construction due to J. Kalman that relates distributive lattices and centered Kleene algebras we define the functor K • relating integral residuated lattices with 0 with certain involutive residuated lattices. Our work is also based on the results obtained by Cignoli about an adjunction between Heyting and Nelson algebras, which is an enrichment of the basic adjunction between lattices and Kleene algebras. The lifting of the functor to the category of residuated lattices leads us to study (...) other adjunctions and equivalences. For example, we treat the functor C whose domain is cuRL, the category of involutive residuated lattices M whose unit is fixed by the involution and has a Boolean complement c. If we restrict to the full subcategory NRL of cuRL of those objects that have a nilpotent c, then C is an equivalence. In fact, C M is isomorphic to C e M, and C e is adjoint to, where assigns to an object A of IRL0 the product A × A 0 which is an object of NRL. (shrink)

This paper is a contribution toward developing a theory of expansions of semi-Heyting algebras. It grew out of an attempt to settle a conjecture we had made in 1987. Firstly, we unify and extend strikingly similar results of [ 48 ] and [ 50 ] to the (new) equational class DHMSH of dually hemimorphic semi-Heyting algebras, or to its subvariety BDQDSH of blended dual quasi-De Morgan semi-Heyting algebras, thus settling the conjecture. Secondly, we give a criterion for a unary expansion (...) of semi-Heyting algebras to be a discriminator variety and give an algorithm to produce discriminator varieties. We then apply the criterion to exhibit an increasing sequence of discriminator subvarieties of BDQDSH . We also use it to prove that the variety DQSSH of dually quasi-Stone semi- Heyting algebras is a discriminator variety. Thirdly, we investigate a binary expansion of semi-Heyting algebras, namely the variety DblSH of double semi-Heyting algebras by characterizing its simples, and use the characterization to present an increasing sequence of discriminator subvarieties of DblSH . Finally, we apply these results to give bases for “small” subvarieties of BDQDSH , DQSSH , and DblSH. (shrink)

Motivated by the definition of semi-Nelson algebras, a propositional calculus called semi-intuitionistic logic with strong negation is introduced and proved to be complete with respect to that class of algebras. An axiomatic extension is proved to have as algebraic semantics the class of Nelson algebras.

In this paper we prove that the free algebras in a subvariety equation image of the variety equation image of semi-Heyting algebras are directly decomposable if and only if equation image satisfies the Stone identity.