~A → A and
A
→ ~ A,
| This is a file in the archives of the Stanford Encyclopedia of Philosophy. |
version history
|
Stanford Encyclopedia of PhilosophyA | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
|
last substantive content change
|
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,
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 57b3, 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 that B should necessarily be great since A is white and that B should necessarily be great since A is 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 (Priest 1999) and (Kneale and Kneale 1962).
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,
consistent systems of connexive logic satisfying Conjunctive
Simplification are presented in Sections 1.3-1.6.
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 2005b; see the Other Internet Resources section) connexive implication is motivated by introducing a negation connective into Categorial Grammar in order to express negative information about membership in syntactic categories.
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 (McCall1966) 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) → B A3 (A→B) → ((A A4 (A A5 (A A6 (A A7 A → (A A8 ((A → ~B) A9 (A A10 ~(A A11 (~A A12 (A →A) → ~(A → ~ A) R1 if A and
R2 if
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
1
2
4
3
3
3
3
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.
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
= <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
=
<, v>. The relation
, t
A (A is true
at t in
) is inductively defined as follows:
A
[Note: whenever there is little chance for ambiguity, we replace R(x, y, z) by Rxyz.]
Moreover, it is required that for every formula A and world
t, G(A, t) implies
, t
A. A formula
A is true in model
iff
, 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
the set CA := {s :
, s
A and
, s
~A} is
non-empty. Like Routley's non-recursive requirement that
G(A, t) implies
, 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 CA ≠
Ø "is closest to the way we think of Aristotle", and emphasizes
that for a self-inconsistent proposition A, the set
CA 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′: If t ∈ O, then (∃x, y ∈
BT: (∃x,y ∈
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.
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, if A were 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 that A entails ~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
= <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)
(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
(
A) iff
, 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) Δ
(b) Δ
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)
(b) ◊τ(A)
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.
A system of connexive logic with an intuitively plausible possible worlds semantics using a binary relation has been introduced in (Wansing 2005a). 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
AtL 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 ↔ A a3 ~(A a4 ~(A 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
= <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
= <W, ≤,
v+, v−>, where
<W, ≤ > is a C-frame and
v+ and v− are valuation
functions from AtL 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.
= <W, ≤,
v+, v−> is said to be
the model based on the frame <W, ≤ >. The relations
, t
+ A
( supports the truth of A
at t) and
, t
− A
(
supports the falsity of A at t) are
inductively defined as follows:
If
= <W, ≤,
v+, v−> is a
C-model, then
A (A is valid
in
) iff for every
t ∈ W,
, t
+ A.
A (A is valid
on
) iff
A for every model
based on
.
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
= <W, ≤,
v+, v−> and formula
A, if s ≤ t, then
, s
+ A implies
, t
+ A and
, s
− A
implies
, 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.
It is obvious from the above presentation that C
differs from Nelson's four-valued constructive logic N4 only with
respect to the falsification (or support of falsity) conditions of
implications. This modification is significant, as it not only turns
→ into a connexive implication but also leads to a constructive
logic with intuitionistic implication in which the DeMorgan laws hold
and provable equivalence is a congruence relation, i.e., the
set {A :
C
A} is closed under the rule A ↔ B /
C(A) ↔ C(B). Wansing (2005a)
also presents a first-order extension QC of
C.
Axiom a5 calls for some explanation. Whereas the direction from right to left 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 may be replaced by
a5′: ~(A → B) ↔ (A → ¬ B).
The resulting system is another system of connexive logic with a transparent semantics and an intuitive interpretation in terms of information states. It satisfies AT, AT′, BT, and BT′, because A → ¬ ~A and ~A → ¬A are theorems. For BT, for example, we have:
1. A→ B assumption 2. B → ¬ ~B theorem 3. A → ¬ ~B 1, 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
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
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
(
A)
is inductively defined as follows:
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:
a1c the axioms of classical positive logical a2 ~ ~A ↔ A a3 ~(A a4 ~(A 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.
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)
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.
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. 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.
| Heinrich Wansing Heinrich.Wansing@tu-dresden.de |
A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z