Information Technology Reference
In-Depth Information
logic that use strict (necessary) implication as a primitive and do not bother to
have a connective
for necessity. But at least for the standard normal modal
logics, strict implication can be defined as
(
A
Ↄ
B
). This kind of move is not
open for relevance logics.
3 Hilbert-Style Formulations for Relevance Logics
Anderson and Belnap have a basic formal language that contains the unary
connective
∼
of De Morgan negation, and the binary connectives of conjunction
∧
.
The following sets of axioms (cf. Anderson and Belnap (1975) or Dunn (1986))
can be seen as forming various fragments of the relevance logic R: 1-4 the impli-
cational fragment R
ₒ
, 1-4 with 10-12 the implication-negation fragment R
ₒ
,
and 1-9 the positive fragment R+.
, disjunction
∨
, and (relevant) implication
→
Implication:
A
→
A
Self-Implication
(1)
(
A
→
B
)
→
[(
C
→
A
)
→
(
C
→
B
)]
Prefixing
(2)
[
A
→
(
A
→
B
)]
→
(
A
→
B
)
Contraction
(3)
[
A
→
(
B
→
C
)]
→
[
B
→
(
A
→
C
)]
Permutation
(4)
Conjunction-Disjunction:
A
∧
B
→
A,
A
∧
B
→
B
Conjunction Elimination
(5)
[(
A
→
B
)
∧
(
A
→
C
)]
→
(
A
→
B
∧
C
) Conjunction Introduction
(6)
A
→
A
∨
B,
B
→
A
∨
B
Disjunction Introduction
(7)
[(
A
→
C
)
∧
(
B
→
C
)]
→
(
A
∨
B
→
C
)
Disjunction Elimination
(8)
A
∧
(
B
∨
C
)
→
(
A
∧
B
)
∨
C
Distribution
(9)
Negation:
(
A
→∼
A
)
→∼
A
Reductio
(10)
(
A
→∼
B
)
→
(
B
→∼
A
)
Contraposition
(11)
∼∼
A
→∼
A
Double Negation
(12)
A Hilbert-style axiom system is often taken to have only one rule of inference:
A, A
B
(modus ponens), and this is the only rule for R
ₒ
and R
ₒ
.
However for R+ and R itself Anderson and Belnap have an additional rule of
inference:
A, B
→
B
∴
B
(adjunction).
The system E of Entailment can be obtained by replacing axiom 4 (Permuta-
tion) with Restricted Permutation: where
B
abbreviates
B
1
→
∴
A
∧
B
2
,
(
B
[
B
[
A
→
→
C
)]
→
→
(
A
→
C
)] Restricted-Permutation.
