Loading ...
Sorry, an error occurred while loading the content.

Conditions for "Basis convexity" (?) of a theory

Expand Messages
  • Vaughan Pratt
    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
    Message 1 of 1 , Apr 16, 2004
    • 0 Attachment
      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
    Your message has been successfully submitted and would be delivered to recipients shortly.