  We give a novel approach to proving soundness and completeness for a logic
(henceforth: the object-logic) that bypasses truth-in-a-model to work directly
with validity. Instead of working with specific worlds in specific models, we
reason with eigenworlds (i.e., generic representatives of worlds) in an
arbitrary model. This reasoning is captured by a sequent calculus for a
meta-logic (in this case, first-order classical logic) expressive enough to
capture the semantics of the object-logic. Essentially, one has a calculus of
validity for the object-logic. The method proceeds through the perspective of
reductive logic (as opposed to the more traditional paradigm of deductive
logic), using the space of reductions as a medium for showing the behavioural
equivalence of reduction in the sequent calculus for the object-logic and in
the validity calculus. Rather than study the technique in general, we
illustrate it for the logic of Bunched Implications (BI), thus IPL and MILL
(without negation) are also treated. Intuitively, BI is the free combination of
intuitionistic propositional logic and multiplicative intuitionistic linear
logic, which renders its meta-theory is quite complex. The literature on BI
contains many similar, but ultimately different, algebraic structures and
satisfaction relations that either capture only fragments of the logic (albeit
large ones) or have complex clauses for certain connectives (e.g., Beth's
clause for disjunction instead of Kripke's). It is this complexity that
motivates us to use BI as a case-study for this approach to semantics.
