Information Technology Reference
In-Depth Information
q
is not provable in E or R. So the Variable Sharing
Property, even together with validity, do not suce for a “relevant implication.”
The Tracking Criterion relies on some way of keeping track. Anderson and
Belnap present a variation of Fitch's natural deduction system for classical logic,
but introduced subscripts to keep track of how assumptions are used. The idea is
that these subscripts are passed down from step to step and combined into a set
of subscripts when a two-premise rule is applied. Thus if one infers
B
from
A
and
A
∼
p
∧
(
p
∨
q
)]
→
implication [
→
B
where
A
has a set of subscripts
ʱ
and
A
→
B
has a set of subscripts
ʲ
,then
B
is inferred with subscripts
ʱ
ʲ
. The idea then is that if one assumes
A
with subscript
i
, and one derives
B
with subscripts
ʲ
, then in order to derive
A
∪
→
B
we must have
i
∈
ʲ
, and then we can derive
A
→
B
with subscripts
ʲ
.
This works beautifully with the pure implicational fragment of R (and
with a slight modification of E), and even stays nice when rules for negation are
added.
But things get complicated when we add conjunction, and really weird when
disjunction is added as well. The problem is that if we assume
p
with subscript
1 and then assume
q
with subscript 2, then one might think it would be natural
to infer
p
−{
i
}
∧
q
with subscripts
{
1
,
2
}
. But then one could derive
q
→
(
p
∧
q
) with
subscript
{
1
}
, and then prove
p
→
(
q
→
(
p
∧
q
)) as a theorem. From this one
can prove
p
p
) (exercise). This is the notorious Positive Paradox of
Implication, and if one plugs any theorem
B
in for
p
and any sentence
A
for
q
, then by modus ponens one can prove
A
→
(
q
→
→
B
,where
A
and
B
may well not
share a sentential variable.
Anderson and Belnap avoid this problem by not allowing the inference
A
1
B
2
A
∧
B
1
,
2
but instead only allow
∧
-introduction when the premises have the same (set of)
subscripts.
This fixes the problem with conjunction (though the uninitiated might find
it ad hoc), but it creates another problem when we try to add disjunction. The
way that disjunction makes things even worse is that Anderson and Belnap want
to have as a theorem:
[
A ∧
(
B ∨ C
)]
→
[(
A ∧ B
)
∨
(
A ∧ C
)]
Distribution
.
We will not bother to state the introduction and elimination rules for disjunc-
tion, but simply state that although they seem very natural, they give Anderson
and Belnap no better way to prove Distribution that to simply postulate it. For
more details please consult Dunn (1986), where you will also find a way to solve
the problem.
One thing Meyer has on his side is that the Anderson-Belnap “relevance log-
ics” do not have some relevance operation
ˁ
in their vocabulary, so that one
might define “
A
relevantly implies
B
” as say “Relevantly,
A
materially implies
B
”:
ˁ
(
A
Ↄ
B
). Of course, the same kind of thing is true of formulations of modal
