|
|
Rupert wrote:
> 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?
Maybe it's a typo. If *all* of the axioms that involve strict
implication are themselves strict implications and there are no axioms
for removing diamonds with implications, and the only rule of deduction
involves ordinary implication, then it seems impossible to meaningfuly
relate strict and ordinary implication (these are probably roughly your
thoughts).
Thus, 8) should(?) read:
8) (A strictly implies B) implies (A implies B). Maybe you could search
through the paper and pay attention to where 8) is actually used.
It is only the presence of axiom schema 9) (and the towering figure of
the great Tarski) that causes me to hedge.
-semiopen
|
|