从严格蕴涵能否定义实质蕴涵？模态逻辑相关技术求证

Great question—this cuts to some fascinating intersections between modal and classical propositional logic. The short answer is yes, such a modal logic exists, and we can construct it to meet all your requirements:

1. Setup: Primitive Symbols and Base System #

We’ll build our modal logic using only two primitive symbols:

• Negation: ¬
• Strict implication: ⥽ (standardly interpreted as "necessarily, if A then B", or □(A→B) in modal notation, but we’re working in reverse here—no primitive □ or material implication →).

We’ll use a base of weak strict implication axioms (similar to Lewis’s S1, plus a key axiom to link strict implication to our future material implication definition):

• Axiom 1 (Self-Implication): ⊢ A ⥽ A
• Axiom 2 (Transitivity): ⊢ (A ⥽ B) ⥽ ((B ⥽ C) ⥽ (A ⥽ C))
• Axiom 3 (Distribution): ⊢ (A ⥽ (B ⥽ C)) ⥽ ((A ⥽ B) ⥽ (A ⥽ C))
• Axiom 4 (Contrapositive Link): ⊢ (A ⥽ B) ⥽ ¬(A ⥽ ¬B)

Our inference rules are:

• Strict Modus Ponens: If ⊢ A and ⊢ A ⥽ B, then ⊢ B
• Uniform Substitution: We can substitute any formula for a propositional variable in a theorem.

2. Defining Material Implication #

We define classical material implication A → B as follows:

A → B =df ¬(A ⥽ ¬B)

Intuitively, this says "it is not necessary that A implies not B"—which, in classical terms, aligns with "if A is true, then B is true" (since the only way A ⥽ ¬B fails is if there’s a scenario where A holds and B doesn’t not hold, i.e., B holds too).

3. Deriving Classical Axioms and Rules #

Now we can show that all standard classical axioms for → and ¬ are theorems of our system, and classical rules are derivable:

Classical Axioms #

1. Axiom K (Weakening): ⊢ A → (B → A)
   Substitute our definition: ⊢ ¬(A ⥽ ¬¬(B ⥽ ¬A)) which simplifies to ⊢ ¬(A ⥽ (B ⥽ ¬A)). Using Axiom 1 (B ⥽ B) and Axiom 3, we can prove this is a theorem—roughly, because A can’t strictly imply that B strictly implies ¬A (since A and B can both hold without contradiction).

2. Axiom S (Distribution): ⊢ (A → (B → C)) → ((A → B) → (A → C))
   Translating to our defined →, this becomes a complex strict implication/negation formula. Using Axioms 2, 3, and 4, we can derive this by leveraging the transitivity and distribution properties of strict implication to mirror the classical distribution rule.

3. Double Negation: ⊢ ¬¬A → A
   Translates to ⊢ ¬(¬¬A ⥽ ¬A). By Axiom 4 and the contrapositive of Axiom 1 (¬A ⥽ ¬A), this simplifies to a theorem—since ¬¬A can’t strictly imply ¬A without contradicting self-implication.

Classical Inference Rules #

• Modus Ponens: If ⊢ A and ⊢ A → B, then ⊢ B
  If ⊢ A and ⊢ ¬(A ⥽ ¬B), then by Axiom 4, the negation of A ⥽ ¬B entails that A ⥽ B must hold (since A ⥽ ¬B and A ⥽ B can’t both be true if A is a theorem). Then applying Strict Modus Ponens to ⊢ A and ⊢ A ⥽ B gives us ⊢ B.

Why This Works #

The core trick is using negation to "undo" the modal force of strict implication, creating a connective that behaves exactly like classical material implication. Our axiom 4 ensures that strict implication entails our defined material implication, and the base strict implication axioms give us enough structure to derive all classical rules and axioms without needing primitive material implication.

内容的提问来源于stack exchange，提问作者Justin