From modal to classical logic

Question

Can material implication be defined from strict implication? More precisely, is there a modal logic with primitive symbols for negation and strict implication only, such that material implication can be defined and axioms for material implication and negation are then derivable as theorems? The rules of inference of classical logic should also be derivable.

Answer 1

Let's try at least to sharpen things up and to get a clearly framed question.

Strict implication of course comes in various grades (corresponding to the strength of various modal systems). Let's consider the strict implication conditional of S5. Now it is known that the pure strict implication fragment of S5 is axiomatised by taking as axioms instances of the schemas

$(A \Rightarrow A)\\ (A \Rightarrow (B \Rightarrow C)) \Rightarrow ((A \Rightarrow B) \Rightarrow (A \Rightarrow C))\\ (S \Rightarrow (A \Rightarrow S))\\ (((S \Rightarrow A) \Rightarrow S) \Rightarrow S) $

where $S$ is a strict conditional $C \Rightarrow D$, and the rule of inference is strict modus ponens.

We can add to this the following negation rules

$(A \Rightarrow B) \Rightarrow ((A \Rightarrow {\sim}B) \Rightarrow (A \Rightarrow C)))\\ (A \Rightarrow {\sim\sim}A)\\ (({\sim}B \Rightarrow {\sim}A) \Rightarrow (A \Rightarrow B))$

and (if I recall correctly) you then get the strict implication/negation fragment of S5.

So now we have something on the table to play with, and a clear question to ask. Is there a wff $A \to C$ definable in terms of $A, C, \sim, \Rightarrow$ for which the standard classical laws of the material conditional and negation together are then provable in the implication/negation fragment of S5? (If not provable in this strong system, they won't be provable in a weaker system corresponding to a weaker notion of strict implication for S3, S4 etc.)

E.g. can we define an arrow for which Peirce's Law is provable in this system.

That's a clear question, at least. My conjecture is: no!