<html><head><meta name="color-scheme" content="light dark"></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">
\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$ &amp;  0  &amp; 1 \\\hline
     0 &amp;  +  &amp; + \\
     1 &amp; $-$ &amp; + \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$ &amp; 0 &amp; 1 \\\hline
   0 &amp; 1 &amp; 1 \\
   1 &amp; 0 &amp; 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$ &amp;  0  &amp;  1  &amp;  2  \\\hline
                         0 &amp;  +  &amp;  +  &amp;  +  \\
                         1 &amp; $-$ &amp;  +  &amp; $-$ \\
                         2 &amp; $-$ &amp; $-$ &amp;  +
             \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$ &amp; 0 &amp; 1 &amp; 2 \\\hline
              0 &amp; 1 &amp; 1 &amp; 1 \\
              1 &amp; 0 &amp; 1 &amp; 0 \\
              2 &amp; 0 &amp; 0 &amp; 1
         \end{tabular}} \hs{15mm}
   \mbox{\begin{tabular}{c|ccc}
         $\C_2$ &amp; 0 &amp; 1 &amp; 2 \\\hline
              0 &amp; 2 &amp; 2 &amp; 2 \\
              1 &amp; 0 &amp; 1 &amp; 0 \\
              2 &amp; 0 &amp; 0 &amp; 1
         \end{tabular}} \hs{15mm}
   \mbox{\begin{tabular}{c|ccc}
         $\C_3$ &amp; 0 &amp; 1 &amp; 2 \\\hline
              0 &amp; 1 &amp; 2 &amp; 1 \\
              1 &amp; 0 &amp; 2 &amp; 0 \\
              2 &amp; 0 &amp; 0 &amp; 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. \&gt; 0-adic:  \&gt; t, \ f, \ T, \ F \\
2. \&gt; Monadic: \&gt; $\N$ \\
3. \&gt; Dyadic:  \&gt; \&amp;, \ $\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, 
\ \&amp; \ and \ $\A$\@.  They pick out greatest lower and least 
upper bounds under the implication order.  That is
\begin{eqnarray*}
a\Leq b\K c &amp; \iff &amp; a\Leq b\mbox{ \ and \ }a\Leq c \\
a\A b\Leq c &amp; \iff &amp; 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 &amp; = &amp; (a\C b)\K(a\C c) \\
a\A b\CC c &amp; = &amp; (a\C c)\K(b\C c)
\end{eqnarray*}
Another optional extra is the distribution law
\begin{eqnarray*}
a\A(b\K c) &amp; = &amp; (a\A b)\K(a\A c) \\
a\K(b\A c) &amp; = &amp; (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 \ \&amp; \ 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 \ \&amp; \ 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 &amp; = &amp; a \\
a\Leq b &amp; \imp &amp; \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) &amp; = &amp; \N a\A\!\N b \\
\N(a\A b) &amp; = &amp; \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 &amp; = &amp; \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} \&amp; and $\A$
\item \hs{3mm} $\fs$
\item \hs{3mm} $\N$
\end{enumerate}
Any fragment with \&amp; 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.
</pre></body></html>