Axioms for modal logics based upon counterfactuals

Suppose we have a logic for counterfactuals as with David Lewis. I here use ⇛ for the counterfactual conditional. So suppose we have:

Rules:

(1) If A and A→B are theorems, then B is a theorem.

(2) If (B1∧...)→C is a theorem, then so is ((A⇛B1)∧...)→(A⇛C)

Axioms:

(1) All truth functional tautologies

(2) A⇛A

(3) ((A⇛B)∧(B⇛A))→((A⇛C)↔(B⇛C))

(4) (((A∨B)⇛A)∨((A∨B)⇛B))∨(((A∨B)⇛C)↔((A⇛C)∧(B⇛C))

(5) (A⇛B)→(A→B)

(6) (A∧B)→(A⇛B)

Given Lewis's semantics so that α⇛β holds iff β holds in all closest possible worlds where α holds, we may define the modal operator for necessity

Definition

□α:=¬α⇛α.

Question

How do I most elegantly get modal logics in the hierarchy up to S5 on the basis of axiomatic principles for ⇛ while presupposing the Definition.

Initial example:

Given the Definition and the instance of axiom (5) that (¬α⇛α)→(¬α→α), we immediately get the T-axiom: □α→α.

• Unfortunately, Philosophy SE doesn't render LaTeX. If you could translate that to unicode symbols it'd make for an easier read. Jun 21, 2018 at 11:40
• Why should it be possible to prove K syntactically? It seems like proving it would depend on S5 semantics. Jun 22, 2018 at 7:12
• @Schiphol Yes, unfortunately Philosophy SE does not offer the option to write in LaTex. Maybe I will translate this tomorrow. Nevertheless, those that know Latex may just copy my posting into a latex editor and so access a quite readable version. Jun 22, 2018 at 18:04
• @Greg S To prove a statement - as K - syntactically does not rely upon any particular semantics, but upon the axioms and rules of the system presupposed. Jun 22, 2018 at 18:06
• Those who want to scrutinise some of these matters may access a compiled text here: mathoverflow.net/questions/302877/… Jun 24, 2018 at 22:30

1 Answer

Based on Zeman, you can prove S5 from L3, RL, L2 and L6. Since you've proven L3 (T), and your Rule 2 implies RL (N), that leaves L2 (K), and L6 (5). Ordinarily, K and 5 are axioms, so it's not obvious that they are provable from the syntax of counterfactuals. I might use a semantic justification for an axiom for 5 or S5 semantics from which K should follow.

If the axiomatization is complete with respect to S5 necessity semantics, you can prove L6.

L6) ¬(A⇛¬A)→((A⇛¬A)⇛¬(A⇛¬A))

For additional information, see mathoverflow answer