Explicit Two-Variable Bases and the Single-Equation Problem for iEx-Logic

Abstract

We study Ex-algebras, which capture the common sequent validities of Heyting algebras and orthomodular algebras with Sasaki implication. Over the fixed fundamental-algebra base in the original signature {meet, join, implication, 0, 1}, we prove a two-local representation theorem and give an explicit fourteen-equation basis using at most two schematic variables per equation. This list compresses to two explicit binary equations. A seven-element fundamental non-Ex algebra whose one-generated full-signature subalgebras are Ex shows that no set, finite or infinite, of unary equations can define Ex over this base. Thus the minimum possible variable bound for additional defining equations is exactly two. A single equation with three variables is available, but existence of a single binary defining equation remains open. We give an exact criterion for that remaining problem using fully invariant congruences of the free two-generator fundamental algebra; this criterion does not settle the existence question. Version 1.1.0 retains the original two-local theorem, named minimal-basis classification and bare-rule distinction, and adds the explicit binary bases and exact variable-bound result. Algebraic statements cover arbitrary cardinalities, all valuations and arbitrary finite primitive terms. Zenodo preprint.