 In place of this last “∏ U0 ⋅ ∏ U1”, we could equally well have written “∏ (U0 ∪ U1)”, of course. The form as written is more suggestive of the many variations on the semantic treatment of disjunction in the literature—the Beth semantics for intuitionistic logic, for instance, and the treatment of disjunction for relevant (or ‘relevance’) and other substructural logics to be found in Ono and Komori (1985), Orłowska (1985, 455), and Bell (1986), to cite only some papers from the 1980s.[17] We will not discuss other connectives from this perspective here, or comment further on Garson’s program. See Garson (2001) for a discussion of the global ranges of the usual sets of introduction and elimination rules for →, ¬ and  ↔.[18]  Garson’s approach to these matters has, it should be noted, undergone further evolution since the publications cited in this discussion: see Garson (2013).