# Connexive Logic

*First published Fri Jan 6, 2006; substantive revision Tue Oct 10, 2006*

Connexive logic is a comparatively little-known and to some extent
neglected branch of nonclassical logic. Systems of connexive logic are
neither subsystems nor extensions of classical logic. Connexive logics
have a standard logical vocabulary and comprise certain non-theorems
of classical logic as theses. Since classical propositional logic is
Post-complete, any additional axiom in its language gives rise to the
trivial system, so that any non-trivial system of connexive logic will
have to leave out some theorems of classical logic. The name
‘connexive logic’ suggests that systems of connexive logic
are motivated by some ideas about coherence or connection between
premises and conclusions of valid inferences or between formulas of a
certain shape. The kind of coherence in question concerns the meaning
of implication and negation. One basic idea is that no formula
provably implies or is implied by its own negation. This conception
may be expressed by requiring that for every formula *A*,

⊬ ~A→Aand ⊬A→ ~A,

but usually the underlying intuitions are expressed by requiring that certain schematic formulas are theorems:

AT: ~(~A →A) and

AT′: ~(A→~A).

The first formula is often called *Aristotle's Thesis*. If this
non-theorem of classical logic is found plausible, then the second
principle, AT′, would seem to enjoy the same degree of
plausibility. Indeed, also AT′ is sometimes referred to as
Aristotle's Thesis. As McCall (1975, 435) explains,

[c]onnexive logic may be seen as an attempt to formalize the species of implication recommended by Chrysippus:And those who introduce the notion of connection say that a conditional is sound when the contradictory of its consequent is incompatible with its antecedent. (Sextus Empiricus, translated in Kneale and Kneale 1962, p. 129.)

Using intuitionistically acceptable means only, the pair of theses AT
and AT′ is equivalent in deductive power with another pair of
schemata, which in established terminology are called (Strong)
*Boethius' Theses* and which may be viewed (in addition with
their converses) as capturing Chrysippus' idea:

BT: (A→B)→~(A →~B) and

BT′: (A→ ~B) → ~ (A→B).

The names ‘Aristotle's Theses’ and ‘Boethius'
Theses’ are, of course, not arbitrarily chosen. AT, for example,
is assumed at Aristotle's *Prior Analytics* 57^{b}3,
where it is explained that:

[I]t is impossible that the same thing should be necessitated by the being and by the not-being of the same thing. I mean, for example, that it is impossible thatBshould necessarily be great sinceAis white and thatBshould necessarily be great sinceAis not white.

Moreover, Boethius, for instance, holds that ‘if *A*
then ~*B*’ is the negation of ‘if *A*, then
*B*’ (Kneale and Kneale 1962, p. 191). Additional
historical remarks may be found in Kneale and Kneale 1962, Priest
1999, and Nasti De Vincentis 2006.

Let *L* be a language containing a unary connective ~
(negation) and a binary connective → (implication). A logical
system in a language extending *L* is called a *connexive
logic*, if AT, AT′, BT, and BT′ are theorems and,
moreover, (*A→**B*) →
(*B→**A*) fails to be a theorem (so that → can
hardly be understood as a bi-conditional). The connective → in a
system of connexive logic is said to be a *connexive
implication*.

Routley (1978) suggested a narrower conception of connexive logic. If
the requirement of a connection between antecedent and succedent of a
valid implication is understood as a content connection, and if a
content connection obtains if antecedent and succedent are relevant to
each other, then "the general classes of connexive and relevant logics
are one and the same" (Routley 1978, p. 393). Since every non-trivial
system of connexive logic has to omit some classical tautologies, and
since the standard paradoxes of non-relevant, material implication can
be avoided by rejecting Conjunctive Simplification, i.e.,
(*A*
∧ *B*) → *A* and
(*A*
∧ *B*) → *B*,
Routley requires for a connexive logic the rejection or qualification
of Conjunctive Simplification (or equivalent schemata). If the
contraposition rule and uniform substitution are assumed, the
combination of Conjunctive Simplification and Aristotle's Theses
results in inconsistency, see, for example, Thompson 1991. Mortensen
(1984) pointed out that there are inconsistent but non-trivial systems
satisfying both AT′ and Simplification. Examples of
non-trivial inconsistent systems of connexive logic satisfying Conjunctive
Simplification are presented in Sections 1.4 and 1.5.

Motivation for systems of connexive logic not only comes from
considerations about a content connection between antecedent and
succedent in valid implications, but also from more instrumental
considerations. In MacCall 1967, connexive implication is motivated by
reproducing in a first-order language all valid moods of Aristotle's
syllogistic. In particular, the classically invalid inference from
‘All *A* is *B*’ to ‘Some *A*
is *B*’ is obtained by translating ‘Some *A*
is *B*’ as
∃*x*(~(*A*(*x*) →
~*B*(*x*)), where → is a connexive implication. In
Wansing 2007 connexive implication
is motivated by introducing a negation connective into Categorial
Grammar in order to express negative information about membership in
syntactic categories.

- 1. Systems of connexive logic
- 2. Connexive logics and consequential logics
- 3. Summary
- Bibliography
- Other Internet Resources
- Related Entries

## 1. Systems of connexive logic

### 1.1 Algebraic connexive logic

Whereas the basic ideas of connexive logic are traced back to
antiquity, the search for formal systems with connexive implication
seems to have begun only in the 19th century in the work of H. MacColl
(1878). The more recent formal study of systems of connexive logic
started in the 1960s. In McCall 1966, S. McCall presented an
axiomatization of a system of propositional connexive logic introduced
by Angell (1962) in terms of certain four-valued matrices. The
language of McCall's logic **CC1** contains as primitive
(notation adjusted) a unary connective ~ (negation) and the binary
connectives
∧ (conjunction) and →
(implication). Disjunction
∨
and equivalence ↔ are defined in the usual way. The schematic
axioms and the rules of **CC1** are as follows:

A1 ( A→B) → ((B→C) → (A→C))A2 (( A→A) →B) →BA3 ( A→B) → ((A∧C) → (B∧C))A4 ( A∧A) → (B→B)A5 ( A∧ (B∧C)) → (B∧ (A∧C))A6 ( A∧A) → ((A→A) → (A∧A))A7 A→ (A∧ (A∧A))A8 (( A→ ~B) ∧B) → ~AA9 ( A∧ ~(A∧ ~B)) →BA10 ~( A∧ ~(A∧A))A11 (~ A∨ ((A→A) →A)) ∨ (((A→A) ∨ (A→A)) →A)A12 ( A→A) → ~(A→ ~A)R1 if ⊢ Aand ⊢ (A→B), then ⊢B(modus ponens)R2 if ⊢ Aand ⊢B, then ⊢ (A∧B) (adjunction)

Among these axiom schemata, only A12 is supraclassical. The system
**CC1** is characterized by the following four-valued
truth tables with designated values 1 and 2:

~ 1 4 2 3 3 2 4 1

∧ 1 2 3 4 1 1 2 3 4 2 2 1 4 3 3 3 4 3 4 4 4 3 4 3

→ 1 2 3 4 1 1 4 3 4 2 4 1 4 3 3 1 4 1 4 4 4 1 4 1

McCall emphasizes that the logic **CC1** is only one
among many possible systems satisfying the theses of Aristotle and
Boethius. Although **CC1** *is* a system of
connexive logic, its algebraic semantics appears to be only a formal
tool with little explanatory capacity. In **CC1**, the
constant truth functions **1**, **2**,
**3**, and **4** can be defined as follows
(McCall1966, p. 421): **1** := (*p*
→*p*), **2** := ~(*p* ↔
~*p*)}, **3** := (*p* ↔ ~*p*),
**4** := ~(*p*→*p*), for some sentence
letter *p*. As Routley and Montgomery (1968, p. 95) point out,
**CC1** "can be given a semantics by associating the
matrix value 1 with logical necessity, value 4 with logical
impossibility, value 2 with contingent truth, and value 3 with
contingent falsehood. However, many anomalies result; e.g. the
conjunction of two contingent truths yields a necessary truth".
Moreover, McCall points out that **CC1** has some
properties that are difficult to justify, if the name ‘connexive
logic’ is meant to reflect the fact that in a valid implication
*A*→ *B* there exists some form of connection
between the antecedent *A* and the succedent *B*. Axiom
A4, for example, is bad in this respect. On the other hand,
**CC1** might be said to undergenerate, since (*A*
∧
*A*) → *A* and *A* →
(*A*
∧
*A*) fail to be theorems of **CC1**. Routley and Montgomery
(1968) showed that the addition of the latter formulas to only a
certain subsystem of **CC1** leads to inconsistency.

These observations may well have distracted many non-classical
logicians from connexive logic. If the validity of Aristotle's and
Boethius' Theses is distinctive of connexive logics, it is, however,
not quite clear how damaging the above criticism is. In order to
construct a more satisfactory system of connexive logic, McCall (1975)
defined the notions of a connexive algebra and a connexive model and
presented an axiom system **CFL** that is characterized by
the class of all connexive models. In the language of
**CFL**, however, every implication is first-degree, i.e.,
no nesting of → is permitted. McCall refers to a result by R.
Meyer showing that the valid implications of **CFL** form
a subset of the set of valid material equivalences and briefly
discusses giving up the syntactic restriction to first-degree
implication. In summary, it seems fair to say that as the result of the
investigations into connexive logic in the 1960s and 1970s, connexive
logic, its ancient roots notwithstanding, appeared as a sort of exotic
branch of non-classical logic.

### 1.2 Connexive logic based on ternary frames for relevance logics

In the late 1970s and the 1980s, connexive logic was subjected to
semantical investigations based on ternary frames for relevance
logics. Routley (1978) obtained a semantic characterization of
Aristotle's Thesis AT′ and Boethius' Thesis BT using a
‘generation relation’ *G* between a formula
*A* and a possible world *s*. The semantics employs
model structures
F = <*T*, *K*,
*R*, *S*, *U*, *G*, *>, where *K*
is a non-empty set of possible worlds, *T* ∈ *K* is
a distinguished world (the ‘real world’), *R*,
*S*, and *U* are ternary relations on *K*,
*G* is a generation relation, and * is a function on *K*
mapping every world *s* to its ‘opposite’ or
‘reverse’ *s**. A valuation is a function
*v* that sends pairs of worlds and propositional variables into
{0,1}, satisfying the following heredity condition: if
*R*(*T*, *s*, *u*) and *v*(*p*,
*s*) = 1, then *v*(*p*, *u*) =
1. Intuitively, *G*(*A*, *t*) is supposed to mean that
everything that holds in world *t* is implied by *A*. A
model is a structure
M =
<F, *v*>. The relation
M, *t*
⊨ *A* (*A* is true
at *t* in
M) is inductively defined as follows:

M,t⊨piffv(p,t) = 1

M,t⊨ ~Aiff M,t* ⊭A

M,t⊨ (A∧B) iff there ares,uwithStsuM,s⊨Aand M,u⊨B

M,t⊨ (A∨B) iff there ares,uwithUtsuM,s⊨Aor M,u⊨B

M,t⊨ (A→B) iff for alls,uifRtsuand M,s⊨A, then M,u⊨B

[Note: whenever there is little chance for ambiguity, we replace
*R*(*x*, *y*, *z*) by
*R**x**y**z*.]

Moreover, it is required that for every formula *A* and world
*t*, *G*(*A*, *t*) implies
M, *t*
⊨ *A*. A formula
*A* is true in model
M iff
M, *T*
⊨ *A*, and *A* is
valid with respect to a class of models, if *A* is true in all
models from that class. AT′ is semantically characterized by the
following property of models: ∃*t*
(*R*(*T**, *t*, *t**) and
*G*(*A*, *t*)), and BT is characterized by
∀*w*∃*s*, *t*, *u*
(*R*(*w*, *s*, *t*),
*R*(*w**, *s*, *u*),
*G*(*A*, *s*), and
*R*(*T*, *t*, *u**)).

Mortensen (1984), who considers AT′, explains that Routley's
characterization of AT′ is "not particularly intuitively
enlightening" and points out that in certain logics with a ternary
relational models semantics another characterization of AT′ is
available, namely the condition that for every model
M
the set C_{A} := {*s* :
M, *s*
⊨ *A* and
M, *s*
⊭ ~*A*} is
non-empty. Like Routley's non-recursive requirement that
*G*(*A*, *t*) implies
M, *t*
⊨ *A*, Mortensen's
condition is not a purely structural condition, since it mentions the
truth relation
⊨. Mortensen (1984, p. 114)
maintains that the condition *C*_{A} ≠
∅ "is closest to the way we think of Aristotle", and emphasizes
that for a self-inconsistent proposition *A*, the set
*C*_{A} must be empty, whence AT′ is to
be denied. Mortensen also critically discusses the addition of
AT′ to the relevance logic **E**. In this context,
AT′ amounts to the condition that no implication is true at the
world *T**.

A more regular semantics for extensions of the basic relevance logic
**B** by either AT′ or BT has been presented in
(Brady 1989). In this semantics, conjunction is defined in the
standard way, and there is a subset of worlds *O* ⊆
*K*. The extended model structures contain a function
ℑ that maps sets of worlds, and in
particular, interpretations of formulas (alias propositions)
*I*(*A*) to sets of worlds in such a way that a formula
*A* is true at a world *t* iff *t* ∈
ℑ(*I*(*A*)). This
allows Brady to state model conditions capturing AT′ and BT as
follows:

AT′: Ift∈O, then (∃x,y∈ ℑ(f))Rt*xy* , for any propositionf;BT: (∃

x,y∈ ℑ(f)) (∃z∈K) (RtxzandRt*yz*), for any propositionfand anyt∈K.

Note that these clauses still are not purely structural conditions but conditions on the interpretation of formulas. Also the investigations into connexive logics based on ternary frames did not, as it seems, lead to establishing connexive logic as a fully recognized branch of non-classical logic.

### 1.3 Connexive logic based on subtraction negation

A close relation between connexive logic and the idea of negation as
cancellation has been observed by Routley (1978), Routley *et
al*. (1982), and Routley and Routley (1985). However, whereas
Routley suggested the semantics using a generation relation, connexive
logics based in a straightforward way on the cancellation view of
negation have been worked out by Priest (1999). Negation as
cancellation (alias subtraction negation) is a conception of negation
that can be traced back to Aristotle's *Prior Analytics* and is
often associated with Strawson, who held that a "contradiction cancels
itself and leaves nothing" (1952, p. 3). (The idea of *ex
contradictione nihil sequitur* is also discussed in Wagner 1991.)
The connection between the subtraction account of negation and the
principles distinctive of connexive logic is explained by Routley and
Routley (1985, p. 205) as follows:

Entailment is inclusion of logical content. So, ifAwere to entail ~A, it would include as part of its content, what neutralizes it, ~A, in which event it would entail nothing, having no content. So it is not the case thatAentails ~A, that is Aristotle's thesis ~(A→ ~A) holds.

Priest (1999) directly translates a definition of entailment that
enforces the null-content account of contradictions into evaluation
clauses. A model is a structure
M = <*W*, *g*,
*v*>, where *W* is a non-empty set of possible worlds,
*g* is a distinguished element from *W*, and *v*
is a valuation function from the set of propositional variables into
the set of classical truth values {1, 0}. Two clauses for evaluating
implications at possible worlds are considered (notation adjusted):

(a) M,s⊨A→Biff (i) there is a worlduwith M,u⊨Aand (ii) for every worldu, M,u⊨Athen M,u⊨B;

(b) M,s⊨A→Biff (i) there is a worlduwith M,u⊨A, (ii) there is a worlduwith M,u⊭B, and (iii) for every worldu, M,u⊨Athen M,u⊨B.

Condition (i) ensures that nothing is implied by an unsatisfiable
antecedent. The evaluation clauses for the other connectives are
classical. A formula *A* is true in a model
(M
⊨ *A*) iff
M, *g*
⊨ *A*; and *A* is
valid if *A* is true in every model. Condition (ii) ensures
that the law of contraposition is valid. A set Δ of formulas is
true in a model iff every element of Δ is true in the
model.

There are two notions of entailment (Δ
⊨ *A*), one coming with
clause (a) the other with clause (b):

(a) Δ⊨Aiff Δ is true in some model, and every model in which Δ is true is a model in whichAis true;

(b) Δ⊨Aiff Δ is true in some model, ~Ais true in some model, and every model in which Δ is true is a model in whichAis true.

These two connexive logics arise from the idea of negation as
cancellation in a straightforward way. They are neither monotonic nor
closed under uniform substitution. Proof systems and decision
procedures for them can be obtained from a straightforward faithful
translation τ into the modal logic **S5**. For
implications *A* → *B* the translation is defined
as follows, where ⊃ is material implication and ¬ is classical
negation:

(a) ◊τ(A) ∧ □(τ(A) ⊃ τ(B));

(b) ◊τ(A) ∧ ◊¬τ(B) ∧ □(τ(A) ⊃ τ(B)).

Although the semantics of Priest's connexive logics is simple and transparent, the underlying idea of subtraction negation is not unproblematic. Priest (1999, p. 146) mentions strong fallibilists who "endorse each of their views, but also endorse the claim that some of their views are false". Their contradictory opinions in fact hardly are contentless, so that the cancellation account of negation and, as a result, systems of connexive logic based on subtraction negation appear not to be very well-motivated.

### 1.4 Four-valued constructive connexive logic

A system of connexive logic with an intuitively plausible possible
worlds semantics using a binary relation has been introduced in
Wansing 2005. In this paper it is observed that a modification of
the falsification conditions for negated implications in possible
worlds models for David Nelson's constructive four-valued logic with
strong negation results in a connexive logic, called
**C**, which inherits from Nelson's logic an
interpretation in terms of information states pre-ordered by a
relation of possible expansion of these states. For Nelson's
constructive logics see, for example, (Almukdad and Nelson 1984,
Gurevich 1977, Nelson 1949, Odintsov 2003, Routley 1974, Thomason
1969, Wansing 2001).

The key observation for obtaining **C** is simple: in the
presence of the double negation introduction law, it suffices to
validate both BT′ and its converse ~(*A* →
*B*) → (*A* → ~*B*). In other
words, an interpretation of the falsification conditions of
implications is called for, which deviates from the standard
conditions. In Nelson's systems of constructive logic, the double
negation laws hold, and the relational semantics for these logics is
such that falsification and verification of formulas are dealt with
separately. However, the falsification conditions of implications are
the classical ones expressed by the schema ~(*A* →
*B*) ↔ (*A*
∧ ~*B*).
To obtain a connexive implication, it is therefore enough to assume
another interpretation of the falsification conditions of implications
expressed by ~(*A* → *B*) ↔ (*A*
→ ~*B*).

Consider the language *L* :=
{∧,
∨, →, ~}
based on the denumerable set
*A**t** _{L}* of propositional
variables. Equivalence ↔ is defined as usual. The schematic
axioms and rules of the logic

**C**are:

a1 the axioms of intuitionistic positive logic a2 ~ ~ A↔Aa3 ~( A∨B) ↔ (~A∧ ~B)a4 ~( A∧B) ↔ (~A∨ ~B)a5 ~( A→B) ↔ (A→ ~B)R1 modus ponens

Clearly, a5 is the only supraclassical axiom of
**C**. The consequence relation
⊢_{C}
(derivability in **C**) is defined as usual. A
**C**-frame is a pair
F = <*W*, ≤ >,
where ≤ is a reflexive and transitive binary relation on the
non-empty set *W*. Let <*W*,
≤ >^{+} be the set of all *X* ⊆
*W* such that if *u* ∈ *X* and *u*
≤ *w*, then *w* ∈ *X*. A
**C**-model is a structure
M = <*W*, ≤,
*v*^{+}, *v*^{−} >,
where <*W*, ≤ > is a **C**-frame
and *v*^{+} and *v*^{−} are
valuation functions from *At** _{L}* into
<

*W*, ≤ >

^{+}. Intuitively,

*W*is a set of information states. The function

*v*

^{+}sends an atom

*p*to the states in

*W*that support the truth of

*p*, whereas

*v*

^{−}sends

*p*to the states that support the falsity of

*p*. M = <

*W*, ≤,

*v*

^{+},

*v*

^{−}> is said to be the model based on the frame <

*W*, ≤ >. The relations M,

*t*⊨

^{+}

*A*(M supports the truth of

*A*at

*t*) and M,

*t*⊨

^{−}

*A*(M supports the falsity of

*A*at

*t*) are inductively defined as follows:

M,t⊨^{+}pifft∈v^{+}(p)

M,t⊨^{−}pifft∈v^{−}(p)

M,t⊨^{+}(A∧B) iff M,t⊨^{+}Aand M,t⊨^{+}B

M,t⊨^{−}(A∧B) iff M,t⊨^{−}Aor M,t⊨^{−}B

M,t⊨^{+}(A∨B) iff M,t⊨^{+}Aor M,t⊨^{+}B

M,t⊨^{−}(A∨B) iff M,t⊨^{−}Aand M,t⊨^{−}B

M,t⊨^{+}(A→B) iff for allu≥t(M,u⊨^{+}Aimplies M,u⊨^{+}B)

M,t⊨^{−}(A→B) iff for allu≥t(M,u⊨^{+}Aimplies M,u⊨^{−}B)

M,t⊨^{+}~Aiff M,t⊨^{−}A

M,t⊨^{−}~Aiff M,t⊨^{+}A

If
M = <*W*, ≤,
*v*^{+}, *v*^{−} > is a
**C**-model, then
M
⊨ *A* (*A* is valid
in
M
) iff for every
*t* ∈ *W*,
M, *t*
⊨^{+} *A*.
F
⊨ *A* (*A* is valid
on
F) iff
M
⊨ *A* for every model
M based on
F.
A formula is **C**-valid iff it is valid on every
frame. Support of truth and support of falsity for arbitrary formulas
are persistent with respect to the relation ≤ of possible expansion
of information states. That is, for any **C**-model
M = <*W*, ≤,
*v*^{+}, *v*^{−} > and formula
*A*, if *s* ≤ *t*, then
M, *s*
⊨^{+} *A* implies
M, *t*
⊨^{+} *A* and
M, *s*
⊨^{−} *A*
implies
M, *t*
⊨^{−} *A*.
It can easily be shown that a negation normal form theorem holds. The
logic **C** is characterized by the class of all
**C**-frames: for any *L*-formula *A*,
⊢_{C}
*A* iff *A* is **C**-valid. Moreover,
**C** satisfies the disjunction property and the
constructible falsity property. If
⊢_{C}
*A*
∨ *B*, then
⊢_{C}
*A* or
⊢_{C}
*B*. If
⊢_{C}
~(*A*
∧ *B*), then
⊢_{C}
~* A* or
⊢_{C}
~*B*.
Decidability of **C** follows from a faithful embedding
into positive intuitionistic propositional logic.

Like Nelson's four-valued constructive logic **N4**,
**C** is a paraconsistent logic. Note that
**C** contains contradictions, for example:
⊢_{C}
((*p*
∧ ~ *p*) →
(~ *p*
∨ *p*)) and
⊢_{C}
~((*p*
∧ ~*p*) →
(~ *p*
∨ *p*)). It is obvious from the
above presentation that **C** differs from
**N4** only with respect to the falsification (or support
of falsity) conditions of implications. As in **N4**,
provable strong equivalence is a congruence relation, i.e., the set
{*A* :
⊢_{C}
*A*} is closed under the rule *A* ↔ *B*,
~ *A* ↔ ~ *B* /
*C*(*A*) ↔ *C*(*B*). Wansing (2005)
also presents a first-order extension **QC** of
**C**.

Whereas the direction from right to left of Axiom a5 can be
justified by rejecting the view that if *A* implies *B*
and *A* is inconsistent, *A* implies any formula, in
particular *B*, the direction from left to right seems rather
strong. If the verification conditions of implications are dynamic (in
the sense of referring to other states in addition to the state of
evaluation), then a5 indicates that the falsification conditions of
implications are dynamic as well. The falsity of (*A* →
*B*) thus implies that if *A* is true, *B* is
*false*. Yet, one might wonder why it is not required that the
falsity of (*A*→ *B*) implies that if *A* is
true, *B* is *not true*. This cannot be expressed in a
language with just one negation ~ expressing falsity instead of
absence of truth (classically at the state of evaluation or
intuitionistically at all related states). If one adds to
**C** the further axiom ~*A* → (*A*
→ *B*) to obtain a connexive variant of Nelson's
three-valued logic **N3**, intuitionistic negation ¬
is definable by setting: ¬*A* := *A* →
~*A*. Then a5 might be replaced by

a5′: ~(A→B) ↔ (A→ ¬B).

The resulting system satisfies AT, AT′, BT, and BT′,
because *A* → ¬ ~*A* and ~*A*
→ ¬*A* are theorems. For BT, for example, we have:

1. A→Bassumption 2. B→ ¬ ~Btheorem 3. A→ ¬ ~B1, 2, transitivity of → 4. ( A→ ¬ ~B) → ~(A→ ~B)axiom a5′ 5. ~( A→ ~B)3, 4, R1 6. ( A→B) → ~(A→ ~B)1, 5, deduction theorem

This logic, however, is the trivial system (a fact not noticed in (Wansing 2005, Section 6)).

### 1.5 Material connexive logic

If implications *A* → *B* are understood as
material implications, then a separate treatment of falsity conditions
again allows introducing a system of connexive logic. The resulting
system **MC** may be called a system of material connexive logic.
The semantics is quite obvious: a model
M
is just a function from the set of all literals, i.e., atomic
formulas or negated atomic formulas, into the set of classical truth
values {1, 0}. Truth of a formula *A* in a model
M
(M
⊨ *A*)
is inductively defined as follows:

M ⊨piffv(p) = 1

M ⊨ (A∧B) iff M ⊨Aand M ⊨B

M ⊨ (A∨B) iff M ⊨Aor M ⊨B

M ⊨ (A→B) iff M ⊭Aor M ⊨B

M ⊨ ~piffv(~p) = 1

M ⊨ ~ ~Aiff M ⊨A

M ⊨ ~(A∧B) iff M ⊨ ~Aor M ⊨ ~B

M ⊨ ~(A∨B) iff M ⊨ ~Aand M ⊨ ~B

M ⊨ ~ (A→B) iff M ⊭Aor M ⊨ ~B

A formula is valid iff it is true in all models. The set of all valid formulas is axiomatized by the following set of axiom schemata and rules:

a1 _{c}the axioms of classical positive logical a2 ~ ~ A↔Aa3 ~( A∨B) ↔ (~A∧ ~B)a4 ~( A∧B) ↔ (~A∨ ~B)a5 ~( A→B) ↔ (A→ ~B)R1 modus ponens

**MC** can be faithfully embedded into positive classical logic,
whence **MC** is decidable. The classical tautology
~(*A* → *B*) → (*A*
∧ ~*B*)
is, of course, not a theorem of **MC**. Like
**C**, **MC** is a paraconsistent logic
containing contradictions.

## 2. Connexive logics and consequential logics

Aristotle's and Boethius' Theses express, as it seems, some
pre-theoretical intuitions about meaning relations between negation
and implication. But it is not clear that a language must contain only
one negation operation and only one implication. The three-valued
constructive connexive logic of Section 1.5 contains two negations,
and the language of systems of *consequential implication*
comprises two implication connectives together with one negation, see
(Pizzi 1977, 1991, 1993, 1996). In (Pizzi and Williamson 1997), the
notion of a normal system of analytic consequential implication is
defined. ‘Normal’ here means that such a system contains
certain formuals and is closed under certain ruels. The smallest
normal consequential logic that satisfies AT is called
**CI**. Alternatively, **CI** can be
characterized as the smallest normal system that satisfies Weak
Boethius' Thesis:

(A→B) ⊃ ¬(A→ ¬B),

where → is consequential implication, ⊃ is material
implication, and ¬ is classical negation. Pizzi and Williamson
show that **CI** can be faithfully embedded into the
normal modal logic **KD**, and vice versa. Analytic
consequential implication is interpreted according to the following
translation function φ:

φ(A→B) = □(φA⊃ φB) ∧ (□φB⊃ □φA) ∧ (◊φB⊃ ◊φA)

As Pizzi and Williamson (1997, 571) point out, their investigation is a "contribution to the modal treatment of logics intermediate between logics of consequential implication and connexive logics." They emphasize a difficulty of regarding consequential implication as a genuine implication connective by showing that in any normal system of consequential logic that admits modus ponens for consequential implication and contains BT, the following formulas are provable:

(a) (A→B) ≡ (B →A),(b) (

A→B) ≡ ¬(A→ ¬B),

where ≡ is classical equivalence. Since (*A* →
*B*) ↔ ~(*A* → ~*B*) is a
theorem of **C**, the more problematic fact, from the
point of view of this system, is the provability of (a). Pizzi and
Williamson also show that in any normal system of consequential logic
that contains BT, the formula (*A* → *B*) ≡
(*A* ≡ *B*) is provable, if (*A* →
*B*) ⊃ (*A* ⊃ *B*) is provable, in other
words, consequential implication collapses into classical equivalence
if (*A* → *B*) ⊃ (*A* ⊃ *B*)
is provable.

## 3. Summary

In summary, it may be said that connexive logic, although it is not very well-known and unusual in various respects, is not just a formal game. There are several kinds of systems of connexive logics with different kinds of semantics and proof systems. (A dialogical treatment of connexive logic may be found in (Rahman and Rückert, 2001).) The intuitions captured by systems of connexive logic can be traced back to ancient roots, and applications of connexive logics range from Aristotle's syllogistic to Categorial Grammar. A recent monograph developing a system of connexive logic in the context of solving a braod range of paradoxes is (Angell, 2002).

## Bibliography

- Almukdad A. and Nelson, D., 1984, "Constructible falsity and
inexact predicates",
*Journal of Symbolic Logic*, 49: 231-233. - Angell, R., 1962, "A Propositional Logic with Subjunctive
Conditionals",
*Journal of Symbolic Logic*, 27: 327-343. - Angell, R., 2002,
*A-Logic*, Lanham: University Press of America. - Brady, R., 1989, "A Routley-Meyer affixing style semantics for
logics containing Aristotle's Thesis",
*Studia Logica*, 48: 235-241. - Gurevich, Y., 1977, "Intuitionistic logic with strong negation",
*Studia Logica*, 36: 49-59. - Kneale, W. and Kneale, 1962, M.,
*The Development of Logic*, London: Duckworth. - MacColl, H., 1878, "The calculus of equivalent statements (II)",
*Proceedings of the London Mathematical Society 1877-78*, 9: 177-186. - McCall, S., 1966, "Connexive Implication",
*Journal of Symbolic Logic*, 31: 415-433. - McCall, S., 1967, "Connexive implication and the syllogism",
*Mind*, 76: 346-356. - McCall, S., 1975, "Connexive implication", § 29.8 in: A.R.
Anderson and N.D. Belnap,
*Entailment. The Logic of Relevance and Necessity. Volume 1*, Princeton: Princeton University Press, 434-446. - Mortensen, C., 1984, Aristotle's Thesis in Consistent and
Inconsistent Logics,
*Studia Logica*43: 107-116. - Nasti De Vincentis, M., 2006, "Conflict and Connectedness: Between
Modern Logic and History of Ancient Logic", in: E. Ballo and
M. Franchella (eds.),
*Logic and Philosophy in Italy*, Monza: Polimetrica, 229-251. - Nelson, D., 1949, "Constructible Falsity",
*Journal of Symbolic Logic*, 14:16-26. - Odintsov, S., 2003, "Algebraic Semantics for Paraconsistent
Nelson's Logic",
*Journal of Logic and Computation*, 13: 453-468. - Odintsov S. and Wansing, H., 2004, "Constructive Predicate Logic
and Constructive Modal Logic. Formal Duality versus Semantical
Duality", in: V. Hendricks et al. (eds.),
*First-Order Logic Revisited*, Berlin: Logos Verlag, 269-286. - Pizzi, C., 1977, "Boethius' Thesis and Conditional Logic",
*Journal of Philosophical Logic*, 6: 283-302. - Pizzi, C., 1991, "Decision Procedures for Logics of Consequential
Implication",
*Notre Dame Journal of Formal Logic*, 32: 618-636. - Pizzi, C., 1993, "Consequential Implication: A Correction",
*Notre Dame Journal of Formal Logic*, 34: 621-624. - Pizzi, C., 1996, "Weak vs. Strong Boethius' Thesis: A Problem in
the Analysis of Consequential Implication", in: A. Ursini and P.
Aglinanó (eds.),
*Logic and Algebra*, New York: Marcel Dekker, 647-654. - Pizzi, C. and Williamson, T., 1997, "Strong Boethius' Thesis and
Consequential Implication",
*Journal of Philosophical Logic*, 26: 569-588. - Priest, G., 1999, "Negation as Cancellation and Connexive Logic",
*Topoi*, 18: 141-148. - Rahman, S. and Rückert, H., 2001, "Dialogical Connexive Logic",
*Synthese*, 127: 105-139. - Routley, R., 1974, "Semantical Analyses of Propositional Systems of
Fitch and Nelson",
*Studia Logica*, 33: 283-298. - Routley, R., 1978, "Semantics for Connexive Logics. I",
*Studia Logica*37: 393-412. - Routley, R., Meyer, R., Plumwood, V. and Brady, R., 1982,
*Relevant Logics and Their Rivals*, Atascadero, CA: Ridgeview Publishing Company. - Routley, R. and Montgomery, H., 1968, "On Systems Containing
Aristotle's Thesis",
*Journal of Symbolic Logic*, 33: 82-96. - Routley, R. and Routley V., 1985, "Negation and Contradiction",
*Revista Columbiana de Mathemáticas*, 19: 201-231. - Strawson, P., 1952,
*Introduction to Logical Theory*, Oxford: Oxford University Press. - Thomason, R., 1969, "A Semantical Study of Constructive Falsity",
*Zeitschrift für mathematische Logik und Grundlagen der Mathematik*, 15: 247-257. - Thompson, B., 1991, "Why is Conjunctive Simplification Invalid?",
*Notre Dame Journal of Formal Logic*, 32: 248-254. - Wagner, G., 1991, Ex contradictione nihil sequitur, in:
*Proceedings IJCAI 1991*, , San Francisco: Morgan Kaufmann, 538-543. - Wansing, H., 2001, "Negation", in: L. Goble (ed.),
*The Blackwell Guide to Philosophical Logic*, Cambridge, MA: Basil Blackwell Publishers, 415-436. - Wansing, H., 2005, "Connexive Modal Logic", in: R. Schmidt et al.
(eds.),
*Advances in Modal Logic. Volume 5*, London: King's College Publications, 367-383. [Available online.] - Wansing, H., 2007, "A note on negation in categorial grammar",
*Logic Journal of the Interest Group in Pure and Applied Logics*15: 271-286.

## Other Internet Resources

[Please contact the author with suggestions.]

## Related Entries

logic: modal | logic: paraconsistent | logic: relevance | type theory: constructive