\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.