\newpage \begin{center} {\Large\bf IV} \vspace{3mm} {\large\bf MODELLING LOGIC} \end{center} \vspace{15mm}\noindent {\large\bf \S4.1\hs{3mm}Propositional Structures} \bigskip A propositional or sentential logic is a consequence relation of some kind defined on a language whose features finer than those of whole clauses do not affect the relation. The language, then, is constructed from a set of {\em atoms} $$ p,\,q,\,r\,\ldots $$ by the application of {\em connectives}. A connective is a function taking sentences to sentences within a language. Each connective has a fixed {\em adicity\/} or number of argument places. Thus such familiar connectives of English as \ `\ldots and\ldots' \ or \ `\ldots because\ldots' \ are dyadic since they require two input sentences to produce an output one, while `it is not the case that\ldots' and `necessarily\ldots' are monadic since they only require one. The language, then, is specified by laying down what are to be the atoms and then by giving a well-ordering of the connectives. The sentences of the language are just those obtainable by closing the set of atoms under the connectives. The logical consequence relation holds between certain collections of sentences (premises of possible valid inferences) and certain single sentences (the conclusions of such). In general these ``collections" need not be {\em sets}, though they might be, for in the contexts of many logics it makes more sense to bunch premises in multisets, sequences, nests of lists or compound structures of more general sorts. What is essential, to logics as envisaged for the purposes of MaGIC, is that there be some notion of the consequences of a single premise---of a collection consisting of just the one sentence taken once---and that one of those consequences be that premise itself. It is also assumed that a version of ``cut" holds, in that where collection $X$ entails conclusion $A$ and where collection $Z$ is just $Y$ with some occurrence of $A$ (not as a proper sub-formula of anything) replaced by $X$, if $Y$ entails $B$ then $Z$ entails $B$. One upshot of this is that entailment by single premises is transitive: if $A$ entails $B$ and $B$ entails $C$ then $A$ entails $C$. Hence the relation of single-premise entailment is a pre-order (transitive and reflexive). MaGIC's matrix modelling technique also assumes, though the general definition of a logic does not, that the connectives are well-behaved with respect to logical consequence in that whenever $A$ and $B$ are logically equivalent so are all compounds built up with the connectives in which $A$ is replaced by $B$. That is, where $C(B)$ is just $C(A)$ with some occurrence of $A$ as sub-formula replaced by $B$, if $A$ and $B$ entail each other then so do $C(A)$ and $C(B)$. This principle, called the law of replacement of equivalents, is central to what follows. \smallskip An {\em interpretation\/} of the language at least assigns some sort of content to each sentence, inducing an equivalence relation on the language: sentences are equivalent on an interpretation iff they are assigned the same content by that interpretation. The contents of sentences all men call {\em propositions}, and sentences with the same content on an interpretation express the same proposition on that interpretation. Now given that we are working with a logic satisfying the replacement law, we can so choose our propositions that whenever $A$ and $B$ express the same proposition $C(A)$ and $C(B)$ express the same proposition as well. In such a case the connectives map in a natural way to functions defined on the set of propositions. We then call the set of propositions (i.e.\ of values which get assigned to sentences) together with the well-ordered set of functions corresponding to the connectives a {\em propositional structure}. To be exact, let the {\em formula algebra\/} of a language be the pair $$ \langle{\cal S},\,\Omega\rangle $$ where $\cal S$ is the set of sentences and $\Omega$ is the set of generating connectives indexed by an ordinal $\alpha$. Let \ $\approx$ \ be the relation of equivalence (co-entailment) in a logic based on that language. Then a {\em quasi-propositional structure\/} appropriate for the logic in question is an algebra $$ \langle\Sigma,\,\omega\rangle $$ similar to \ $\langle{\cal S},\,\Omega\rangle$ \ in that the set $\omega$ is also indexed by $\alpha$. An interpretation $\cal I$ of the language in the quasi-propositional structure is a homomorphism from the formula algebra into it in the sense that for any $n$-adic connective $\Omega_i$ and for all $A_1\ldots A_n$ in $\cal S$ $$ {\cal I}(\Omega_i(A_1\ldots A_n))\,=\, \omega_i({\cal I}(A_1)\ldots{\cal I}(A_n)) $$ A quasi-propositional structure is a {\em pre-propositional structure\/} iff for every such $\cal I$ and for all $A,B\in{\cal S}$, if \ $A\approx B$ \ then \ ${\cal I}(A)={\cal I}(B)$\@. What this comes to is that the relation $\Leq$ modelling single-premise entailment in a pre-propositional structure is a partial order: \begin{enumerate} \item\hs{3mm} $a\Leq a$ \item\hs{3mm} $a\Leq b\;\mt\;b\Leq c\imp a\Leq c$ \item\hs{3mm} $a\Leq b\;\mt\;b\Leq a\imp a=b$ \end{enumerate} It is very important to MaGIC that every pre-propositional structure comes equipped with a partial order representing the relation of implication. \smallskip Some, but not all, propositions are true. The true ones form a subset of $\Sigma$ closed under the relation $\Leq$, since surely whatever is implied on interpretation by a true proposition is likewise a true proposition. Implication, that is, should never lead us into error. It may be that by drawing out consequences of assumptions we bring hidden or unsuspected or unobvious errors to light, but logically acceptable inference itself cannot be destructive of truth. In the usual terminology of matrix modelling the true propositions are called {\em designated values}. Every value is either designated or undesignated and not both, so there is a sense in which bivalence is written into the matrix method. Of course, we are free if our philosophical predelictions so prompt us, to stipulate not only which propositions are true but also which are false, and there is no reason why we have to make the false coincide with the undesignated, so bivalence in stronger senses is not so easy to motivate. For purposes of defining logical validity, however, the designated/undesignated distinction is the important one. A {\em propositional structure\/} in the full sense, for MaGICAL purposes, is therefore a pre-propositional structure together with a chosen set D of designated values. In tuple-talk, then, a propositional structure is a quadruple $$ \langle\Sigma,\,\omega,\,\Leq,\,{\rm D}\rangle $$ Where $\Sigma$ is a set, $\omega$ a well ordered set of finitary operations on $\Sigma$, $\Leq$ a partial order on $\Sigma$ and D a subset of $\Sigma$ closed under $\Leq$\@. A formula is {\em valid\/} in an algebraic model for a system of logic iff it is true on all interpretations. That is, iff its value on every homomorphism from the formula algebra into the target algebra is designated. Validity in a particular propositional structure for logic L need not be the same thing as provability in L as syntactically defined, for the propositional structure may not be {\em characteristic\/} for L. What is minimally required is that every theorem of L be valid in each L propositional structure. \smallskip Among propositional structures appropriate to a logic one very special one is the {\em Lindenbaum algebra\/} of the logic. The elements of the Lindenbaum algebra are, or correspond to, the sets of logically equivalent sentences. That is, the Lindenbaum algebra is the quotient of the formula algebra under the congruence relation of co-entailment. We may think of the elements of the Lindenbaum algebra in the fullest sense as the propositions expressible in the language. Smaller propositional structures---for instance, finite ones---are typically homomorphic images of the Lindenbaum algebra. For the purposes of MaGIC we are not directly interested in Lindenbaum algebras, since these are in the usual cases infinite. The concept is important, however, and needs to be mentioned. \smallskip MaGIC, as the acronym suggests, is concerned with logics which have not only an implication {\em relation\/} but also an implication {\em connective}. An operation $\CC$ in a propositional structure is an implication iff for all elements $a$ and $b$ of $\Sigma$ $$ a\C b\,\in\,D\iff a\Leq b $$ That is, `That $p$ implies that $q$' is to be true if and only if the proposition that $p$ implies the proposition that $q$, which is surely not an unreasonable condition. Back in the logic, we expect $A\C B$ to be a theorem iff $A$ entails $B$. This is a minimal sort of {\em deduction theorem\/} for the logic---one which in standard cases can be improved somewhat, but all we actually demand at this stage. \smallskip As an example of a propositional structure consider {\bf 2}, the familiar truth-table structure of classical logic. This is now being read as a small (2-element) Boolean algebra. Let us label the true proposition 1 and the false one 0. Then the partial order of implication is the relation of material implication: $$ \mbox{\begin{tabular}{c|cc} $\Leq$ & 0 & 1 \\\hline 0 & + & + \\ 1 & $-$ & + \end{tabular}} $$ There is only one possible implication that fits this structure. Not surprisingly, it is the familiar one: $$ \mbox{\begin{tabular}{c|cc} $\C$ & 0 & 1 \\\hline 0 & 1 & 1 \\ 1 & 0 & 1 \end{tabular}} $$ What may be unfamiliar is the thought that the `0' and the `1' stand for {\em propositions}. Since all the true sentences express the same proposition on an interpretation in {\bf 2}, as do all the false ones, the division by propositional content on such an interpretation coincides with the division by truth value. It is therefore possible, in that very special case, to omit mention of the algebra of propositions and let the truth values do all the work. In a more general setting this is not possible. A small algebraic model structure such as {\bf 2} is got by imposing a congruence on the Lindenbaum algebra of the appropriate logic. The effect of this is to conflate what are in the absolute sense distinct propositions. So a proposition in the small structure is the result of waiving distinctions which are not semantically significant for the purposes at hand. Classical logic outside the structure {\bf 2} allows for infinitely many distinct propositions; there the division into propositions cuts finely. But inside {\bf 2} it cuts coarsely, since no distinctions are drawn except for that of truth value. It is a remarkable fact that we lose no logical generality by restricting attention to this one tiny algebra: we should find such things surprising. \smallskip Here is another small partial order, this one with three elements: $$ \begin{picture}(0,4)(0,-2) \put(-5,0){\begin{picture}(0,0)(0,0) \Dt 2,1 \Dt -2,1 \Dt 0,-1 \Ln 2,1,-1,-1 \Ln -2,1,1,-1 \put(-2.75,0.8){1} \put(2.5,0.8){2} \put(0.5,-1.2){0} \end{picture}} \put(5,0){\makebox(0,0) {\begin{tabular}{c|ccc} $\Leq$ & 0 & 1 & 2 \\\hline 0 & + & + & + \\ 1 & $-$ & + & $-$ \\ 2 & $-$ & $-$ & + \end{tabular}}} \end{picture} $$ Let us take 1 and 2 to be designated values. Now, in contrast to the earlier case, we have many possible implication operations. For example: $$ \mbox{\begin{tabular}{c|ccc} $\C_1$ & 0 & 1 & 2 \\\hline 0 & 1 & 1 & 1 \\ 1 & 0 & 1 & 0 \\ 2 & 0 & 0 & 1 \end{tabular}} \hs{15mm} \mbox{\begin{tabular}{c|ccc} $\C_2$ & 0 & 1 & 2 \\\hline 0 & 2 & 2 & 2 \\ 1 & 0 & 1 & 0 \\ 2 & 0 & 0 & 1 \end{tabular}} \hs{15mm} \mbox{\begin{tabular}{c|ccc} $\C_3$ & 0 & 1 & 2 \\\hline 0 & 1 & 2 & 1 \\ 1 & 0 & 2 & 0 \\ 2 & 0 & 0 & 1 \end{tabular}} $$ MaGIC's technique is to pick the order structure first and then to generate all possible ways of filling in the table for $\CC$ which give an implication connective satisfying whatever extra postulates are chosen by the user. As in the above examples, it always represents the elements as the first few natural numbers with the partial order embedded in the numerical order. \newpage\noindent {\large\bf \S4.2\hs{3mm}Vocabulary} \bigskip MaGIC is aimed primarily at De Morgan groupoid logics (see \cite{AAE} and \cite{GLOG}) such as the Anderson-Belnap relevant systems and their relatives. Thus it makes certain assumptions about vocabulary and about additional postulates. These are slightly complicated and must be explained. Firstly, some connectives in addition to the arrow are pre-defined. These are: \begin{tabbing} 99.xxx \= monadic xxx\= connectives \kill 1. \> 0-adic: \> t, \ f, \ T, \ F \\ 2. \> Monadic: \> $\N$ \\ 3. \> Dyadic: \> \&, \ $\A$, \ $\fs$ \end{tabbing} \smallskip The sentential constant t (``the true" as Frege has it) is a minimal logical truth. Semantically it gets mapped to the least designated value. That is $$ {\rm D} = \{x:\;{\rm t}\Leq x\} $$ Thus any fragment in which t is defined requires the set D to have a unique minimum. The 3-element structure pictured above is an example of one where t is not definable. The constant f (``the false") is the negation of t. According to MaGIC it is not defined unless both t and $\N$ \ are. T is the top element in the implication order and F the bottom element. These too are not always definable. In the sample structure above, F exists but T does not. Clearly T and t need not coincide: in {\bf 2} they do, but then {\bf 2} is special. \smallskip The {\em lattice connectives\/} are conjunction and disjunction, \ \& \ and \ $\A$\@. They pick out greatest lower and least upper bounds under the implication order. That is \begin{eqnarray*} a\Leq b\K c & \iff & a\Leq b\mbox{ \ and \ }a\Leq c \\ a\A b\Leq c & \iff & a\Leq c\mbox{ \ and \ }b\Leq c \end{eqnarray*} Clearly these are not defined on most partial orders, since they force implication to configure logical space as a lattice. In affixing logics (see \S4.3 below) the lattice connectives interact with the implication operation, satisfying the stronger lattice ordering postulates \begin{eqnarray*} a\CC b\K c & = & (a\C b)\K(a\C c) \\ a\A b\CC c & = & (a\C c)\K(b\C c) \end{eqnarray*} Another optional extra is the distribution law \begin{eqnarray*} a\A(b\K c) & = & (a\A b)\K(a\A c) \\ a\K(b\A c) & = & (a\K b)\A(a\K c) \end{eqnarray*} the two versions of which are equivalent in context. MaGIC gives a choice between lattice order and distributive latice order. Wherever \ \& \ is explicitly included as part of the fragment being modelled, the set D of designated values is required to be closed under it. This is obviously well motivated as whenever two conjuncts are true so is their conjunction. A consequence of this is that any fragment with \ \& \ also gives t as an available connective. \smallskip Negation in the world of MaGIC is an involution: a dual automorphism of period 2. So it satisfies the two basic postulates \begin{eqnarray*} \N\;\N a & = & a \\ a\Leq b & \imp & \N b\Leq\!\N a \end{eqnarray*} It follows that where the lattice connectives are defined the De Morgan duality laws \begin{eqnarray*} \N(a\K b) & = & \N a\A\!\N b \\ \N(a\A b) & = & \N a\K\!\N b \end{eqnarray*} hold. Not all partial orders, lattices or distributive lattices allow such an operation to be defined. Those that do are symmetrical about a horizontal axis. In the stronger logics, from {\bf DW} up, negation also satisfies \begin{eqnarray*} a\C b & = & \N b\C\,\N a \end{eqnarray*} This imposes a symmetry not only on the partial order but on the implication operation, greatly speeding up the search for models. \smallskip The final connective intrinsic to MaGIC is fusion, $\fs$. This is a kind of intensional conjunction satisfying the condition $$ a\fs b\Leq c\iff a\Leq b\C c $$ See \cite{AAE} and \cite{GLOG} for accounts of how important this connective is to logics of the sort associated with MaGIC. Whether fusion is definable or not depends not on the partial order structure but mainly on the details of the implication matrix. MaGIC has fairly efficient ways of forcing fusion to be defined in the cases of affixing logics, but for weaker systems these do not work; It is not recommended that you ask MaGIC to search for {\bf FD} matrices with fusion defined, as it will probably be unbearably slow. In {\bf C} and its supersystems fusion is directly definable by $$ a\fs b\Df\N(a\C\,\N b) $$ so in those systems all fragments involving negation already allow fusion to be used, for instance in additional axioms. \newpage\noindent {\large\bf \S4.3\hs{3mm}Some Postulates and Systems} \bigskip The basic system is {\bf FD} (for ``First Degree"), in many ways the {\bf S0.5} of the relevant logics. {\bf FD} may be presented in Hilbertian style with the following axiom schemes \begin{enumerate} \item \hs{3mm} $A\C A$ \item \hs{3mm} $A\K B\CC A$ \item \hs{3mm} $A\K B\CC B$ \item \hs{3mm} $A\CC A\A B$ \item \hs{3mm} $B\CC A\A B$ \item \hs{3mm} $A\K(B\A C)\CC(A\K B)\A C$ \item \hs{3mm} $\N\;\N A\CC A$ \item \hs{3mm} $A\C T$ \item \hs{3mm} $F\C A$ \end{enumerate} To these are applied the rule schemes \begin{enumerate} \item \hs{3mm} $A,\;B\imp A\K B$ \item \hs{3mm} $A\C B,\;A\imp B$ \item \hs{3mm} $A\C B,\;B\C C\imp A\C C$ \item \hs{3mm} $A\C B,\;A\C C\imp A\CC B\K C$ \item \hs{3mm} $A\C C,\;B\C C\imp A\A B\CC C$ \item \hs{3mm} $A\C\,\N B\imp B\C\,\N A$ \item \hs{3mm} $A\imp {\rm t}\C A$ \item \hs{3mm} ${\rm t}\C A\imp A$ \item \hs{3mm} $A\Cdot B\C C\imp A\fs B\CC C$ \item \hs{3mm} $A\fs B\CC C\imp A\Cdot B\C C$ \item \hs{3mm} $A\C B,\;B\C A\imp A\C C\Cdot B\C C$ \item \hs{3mm} $A\C B,\;B\C A\imp C\C A\Cdot C\C B$ \end{enumerate} The double arrow in the rule statements is a metalogical conditional. Rule 1, for example, is read `If $A$ is a theorem and $B$ is a theorem then $A\K B$ is a theorem'. The only particle not given explicit postulates is the false constant f which is introduced by definition as $\N$ t. {\bf FD} algebras are propositional structures with operations corresponding to the given connectives and with an implication operation in particular, such that all instances of the axioms map into D and such that D is closed under the algebraic correlate of each of the rules. Rules 11 and 12 go over into the requirement that the implication order be anti-symmetric. \smallskip MaGIC recognises many fragments of logics got by choosing subsets of the available connectives. All include the implication connective of course, and some particles or combinations of particles bring others in their train. Specifically, the user chooses some or all of the following: \begin{enumerate} \item \hs{3mm} t \item \hs{3mm} T \item \hs{3mm} F \item \hs{3mm} \& and $\A$ \item \hs{3mm} $\fs$ \item \hs{3mm} $\N$ \end{enumerate} Any fragment with \& and $\A$ has t, T and F, while any with $\N$ \ has both T and F if either. In some of the stronger logics certain fragments collapse together anyway. For instance in {\bf C} and its supersystems fusion is definable in terms of implication and negation, and in {\bf R} the constant T always exists even in the pure implication fragment. All fragments satisfy axiom 1 and rules 2, 3, 11 and 12. In addition, each fragment satisfies all the given postulates which explicitly involve one of its connectives other than $\CC$\@. \smallskip By an {\em affixing logic\/} we mean one which strengthens {\bf FD} at least by converting rules 4 and 5 into axiom schemes \begin{enumerate}\setcounter{enumi}{9} \item \hs{3mm} $(A\C B)\K(A\C C)\Cdot A\CC B\K C$ \item \hs{3mm} $(A\C C)\K(B\C C)\Cdot A\A B\CC C$ \end{enumerate} and dropping one of the inputs from each of rules 11 and 12 to leave \begin{enumerate}\setcounter{enumi}{10} \item \hs{3mm} $B\C A\imp A\C C\Cdot B\C C$ \item \hs{3mm} $A\C B\imp C\C A\Cdot C\C B$ \end{enumerate} Given these new affixing rules, old rule 3 is redundant. The minimal affixing logic, resulting from {\bf FD} by making just these changes, is the basic relevant logic {\bf B}, featured in \cite{RLR} and \cite{AAE}. The available fragments of {\bf B} are the same as those of {\bf FD}. \smallskip The weakest logic considered in \cite{GLOG} is the system {\bf DW} which differs from {\bf B} just in that rule 6 of the above list is strengthened to the axiom form \begin{enumerate}\setcounter{enumi}{12} \item \hs{3mm} $A\C\;\N B\Cdot B\C\;\N A$ \end{enumerate} Stronger still is the system {\bf TW} which results from {\bf DW} by strengthening the affixing rules to axioms \begin{enumerate}\setcounter{enumi}{13} \item \hs{3mm} $B\C C\Cdot A\C B\Cdot A\C C$ \item \hs{3mm} $A\C B\Cdot B\C C\Cdot A\C C$ \end{enumerate} The pure implication fragment of {\bf TW} is, for somewhat obscure reasons, known as \PW. It may conveniently be axiomatised with axioms 1, 14 and 15 and with rule 2 alone. For any fragment with conjunction rule 1 is needed; the rest can all be done with the appropriate axioms, the other rules being otiose. \smallskip All the further logics offered by MaGIC as pre-defined are supersystems of {\bf TW}. Over those systems the logic of conjunction, disjunction and negation is rather stable; they differ mostly in their postulates concerning the arrow of implication. The systems are: \begin{enumerate} \item {\bf T}\@. This is Anderson and Belnap's system of ``Ticket Entailment" and adds to {\bf TW} the contraction axiom $$ (A\Cdot A\C B)\Cdot A\C B $$ known to its friends and foes as {\bf W}\@.\footnote{This helps to explain the nomenclature: {\bf TW} was originally ``{\bf T$-$W}", meaning {\bf T} without contraction.} For negation {\bf T} also adds the strong ``reductio" axiom $$ A\C\,\N A\CC\,\N A $$ which is related to contraction and suffices to give as theorems all the classical tautologies in the $\K,\,\A,\,\N$ vocabulary. At the time of writing (1989) the decision problem for the pure implication fragment of T is still open. \item {\bf E}\@. Another Anderson-Belnap relevant logic, this was their preferred system in \cite{ENT}\@. The `E' stands for `Entailment'. It adds to {\bf T} the ``necessitation" or ``restricted assertion" axiom $$ {\rm t}\C A\CC A $$ In fragments lacking t the equivalent postulate is the rule $$ A\imp A\C B\CC B $$ This encapsulates the effect of the axiom $$ A\C A\C B\CC B $$ and the rule $$ A\imp A\C A\CC A $$ Anderson and Belnap give this axiom as part of their basis for E and cite this rule as the motivation for their further axiom $$ (A\C A\C A)\K(B\C B\C B)\Cdot A\K B\C A\K B\CC A\K B $$ the effect of which, however, is strictly weaker in context. They regard t as being subject to the conditions MaGIC places upon it where it is officially part of the language fragment but not where it just happens to exist (e.g.\ because the lattice connectives do). So MaGIC does not find all the {\bf E} matrices in the sense of Anderson and Belnap, but it finds all the ones which satisfy their motivational talk. If you want matrices for {\bf E} in the sense of \cite{ENT} you must select logic {\bf T} and add the two Anderson-Belnap axioms to it. The folk wisdom has it that {\bf E} is difficult. Certainly the main focus of research in relevant logic has drifted away from it. Certainly also MaGIC finds it hard to come up with {\bf E} matrices. The postulates seem to be just strong enough to make such matrices fairly rare but not strong enough to impose useful regularities on the search space. \item {\bf R}\@. This ``system of Relevant Implication" is the most intensively investigated of the relevant logics. The most readily available introduction to {\bf R} is the essay by Dunn \cite{RLE}\@. To axiomatise {\bf R} add to {\bf E} the principle that antecedents of nested implications may be permuted. The shortest axiom giving this effect in the context of {\bf E} is $$ A\Cdot{\rm t}\C A $$ Equivalently the restricted assertion axiom can be strengthened to the unrestricted form $$ A\Cdot A\C B\CC B $$ or the full principle of permutation $$ (A\Cdot B\C C)\CC(B\Cdot A\C C) $$ With fusion in the vocabulary, what these amount to is that the propositional operation of fusion be fully associative and commutative, thus giving it the combinatory properties of multiset union. \item {\bf C}\@. Originally ``{\bf R$-$W}", this system is {\bf TW} with the extra stipulation that ${\rm t}\C A$ is equivalent to $A$. Like {\bf R}, {\bf C} allows permutation, and in fact permutation added as an axiom to {\bf DW} gives {\bf C}. {\bf C} without the distribution of conjunction over disjunction is, bar a few quibbles about modality, Girard's ``linear logic". In {\bf C}, as in {\bf R}, fusion is associative and commutative. The addition of almost any contraction-related postulate such as any one of \begin{center} $(A\C B)\K A\CC B$ \\[1mm] $A\C\,\N A\CC\,\N A$ \\[1mm] $(A\C B)\K(B\C C)\Cdot A\C C$ \\[1mm] $A\K\!\N B\CC\,\N(A\C B)$ \end{center} will convert {\bf C} into {\bf R}. \item {\bf S4}\@. The familiar modal logic, with the arrow as strict implication. Matrix representations of model structures for modal logics are not really the most efficient, since ``possible worlds" frames encapsulate the same information much more tightly. The system is offered by MaGIC, though, as its axiomatisation is very simple. It is {\bf T} or {\bf E} plus the axiom K$'$ $$ {\rm T}\C{\rm t} $$ or equivalently $$ A\Cdot B\C B $$ Among other things, this forces distributive lattice orders for the system to be Boolean algebras. Certain smaller fragments of {\bf S4} as axiomatised are of interest. The positive (negation-free) fragments, for instance, are not confined to Boolean order structures, and there are some axiomatic extensions of the pure implication fragment which escape treatment in terms of binary relation Kripke frames. \item {\bf CK}\@. This is the result of adding K$'$ to {\bf C}. It is particularly of interest as a strong and stable subsystem of the \L ukasiewicz many-valued logics, offering good chances of an account of the logic of vague discourse. For an account of this application of systems close to {\bf CK} see \cite{VR}. \end{enumerate} In addition to all this, the various systems may be weakened by dropping the distribution axiom (axiom 6). Where {\bf X} is any of the logical systems known to MaGIC, {\bf LX} is the corresponding non-distributive system.\footnote{`L' is for `Lattice'. The termionology was invented by Thistlewaite {\it et al\/} for the purposes of referring to {\bf LR} in particular in \cite{ATP}.} {\bf LC} (not to be confused with the super-intuitionist system of that name) is noted above. {\bf LCK} is very close to the system generally called {\bf BCK}---to be exact, {\bf BCK} is the \ $\C,\,\K,\,\A,\,{\rm F}$ \ fragment of {\bf LCK}. MaGIC additionally offers to find {\em totally\/} ordered algebras for the various systems. These are easy to generate and easy to read. They therefore have many uses in logic as an empirical science: at the least perusal of them can suggest results to the imaginative logician. \medskip The inclusion relation between the various systems is as follows, the arrow indicating increasing strength: $$ \begin{picture}(0,10)(0,-5) \put(0,0){\circle{1.2}} \put(-3,0){\circle{1.2}} \put(-6,0){\circle{1.2}} \put(-9,0){\circle{1.2}} \put(4.5,2){\circle{1.2}} \put(3,-2){\circle{1.2}} \put(6,-2){\circle{1.2}} \put(9,0){\circle{1.2}} \put(9,4){\circle{1.2}} \put(9,-4){\circle{1.2}} % \put(-8.4,0){\vector(1,0){1.8}} \put(-5.4,0){\vector(1,0){1.8}} \put(-2.4,0){\vector(1,0){1.8}} \put(0.5,-0.3){\vector(3,-2){2}} \put(0.6,0.2){\vector(2,1){3.3}} \put(3.6,-2){\vector(1,0){1.8}} \put(5.1,2.2){\vector(2,1){3.3}} \put(5.1,1.8){\vector(2,-1){3.3}} \put(6.5,-1.7){\vector(3,2){2}} \put(6.5,-2.3){\vector(3,-2){2}} % \put(0,0){\makebox(0,0){{\fns TW}}} \put(-3,0){\makebox(0,0){{\fns DW}}} \put(-6,0){\makebox(0,0){{\fns B}}} \put(-9,0){\makebox(0,0){{\fns FD}}} \put(4.5,2){\makebox(0,0){{\fns C}}} \put(3,-2){\makebox(0,0){{\fns T}}} \put(6,-2){\makebox(0,0){{\fns E}}} \put(9,0){\makebox(0,0){{\fns R}}} \put(9,4){\makebox(0,0){{\fns CK}}} \put(9,-4){\makebox(0,0){{\fns S4}}} \end{picture} $$ There is a similar diagram for the non-distributive systems and another for the totally ordered ones.