|
|
In their paper "Some theorems about the sentential calculi of Lewis and
Heyting", McKinsey and Tarski present a system of modal logic in which
&, ~, and [diamond] are the undefined logical symbols, the sole rule of
inference is modus ponens, "a implies b" means
~(a & ~b),
"a strictly implies b" means
~[diamond](a & ~b),
and the following are axioms, for any formulas A, B, C, and D:
1) (A & B) strictly implies (B & A)
2) (A & B) strictly implies A
3) A strictly implies (A & A)
4) ((A & B) & C) strictly implies (A & (B & C))
5) ((A strictly implies B) & (B strictly implies C)) strictly implies
(A strictly implies C)
6) (A & (A strictly implies B)) strictly implies B
7) [diamond][diamond]A strictly implies [diamond]A
8) (A strictly implies B) strictly implies (A implies B)
9) A implies (B implies (A and B))
10) ((A strictly implies C) and (B strictly implies D)) strictly
implies ((A and B) strictly implies (C and D))
11) (A strictly implies B) strictly implies ([diamond]A strictly
implies [diamond]B)
and they say that by (8) the rule of detachment for strict implication
is a derived rule of the system. I assume this means that if A and (A
strictly implies B) are theorems of the system, then so is B. I am
having trouble seeing how this is the case since (8) is a strict
implication. Can anyone help me?
|
|