A is true when there is some
true proposition that implies all x-instantiations
of A. Formulae are
modelled as functions from variable-assignments to propositions,
where a proposition is a set of worlds in a relevant model structure.
A completeness proof is given for a basic quantificational system QR
from which RQ is obtained by adding the axiom EC of `extensional
confinement':
∀x(A ∨ B) → (A ∨ ∀xB),
with x not free in A. Validity of EC requires an
additional model condition involving the boolean difference of
propositions. A QR-model falsifying EC is constructed by forming
the disjoint union of two natural arithmetical structures in which
negation is interpreted by the minus operation.