Conditions for "Basis convexity" (?) of a theory
- Dear UACTers,
Luca Aceto asked me yesterday, in the context of results of his about
theories of parallel composition, about conditions for a finitely based
theory to remain so after removal of any operation.
It occurred to me that his question could be usefully formulated in terms
of a suitable notion of basis convexity. Call a theory *basis convex*
when its axiom rank (minimum size of axiomatization, e.g. fewest axioms
in the case of equational theories) is no smaller than that of any theory
it conservatively extends. Useful variants or extensions would involve
cardinality conditions or restrictions, e.g. only allowing limit ordinals
for axiom rank in order to immunize the notion against mere finite increases
This seems like a simple and natural notion. For example the equational
theory of regular expressions, viewed as a monotonic fixpoint logic with
a conjunction ab, a disjunction a+b, and a fixpoint operator *, is not
finitely based (Redko 1964, Conway 1971), but its conservative extension
with (nonmonotonic) implication x->y is, proved by borrowing Tarski and
Ng's axiom (x\x)* < x\x for their system RAT, RA with transitive closure.
Had this adjective occurred to me (slaps forehead with flat of hand) when I
wrote this up for JELIA'90, not only could whole sentences have been shrunk
down to just this adjective, the result could have been title of the paper:
"The Theory of Conditional Regular Expressions is Not Basis Convex."
Does this concept exist already? If so what is known about it, e.g.
necessary or sufficient conditions? And does it relate to other convexity
notions such as what Joyal calls softness and the Nelson-Oppen-Shostak
theorem-proving crowd calls convexity? This is the condition:
if a&b -> cvd is in the theory,
then so is one of a -> c, a -> d, b -> c, or b -> d.
(In the classical case with a,b,c,d literals it is enough to require just
a&b -> c or a&b -> d, true for Nelson-Oppen but not for Joyal.)
Orthomodularity might be another candidate for some kind of nonconvexity
(concavity?), by analogy with regular expressions -- neither metrical
completeness of inner product spaces (Goldblatt, JSL 1984) nor transitive
closure of binary relations as respective associated dual notions are
elementary, a phenomenon that could conceivably play a role in basis