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 in rank. 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 convexity. Vaughan Pratt
participants (1)
-
Vaughan Pratt