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


(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)


(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




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.
    – Schiphol
    Commented 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.
    – Greg S
    Commented 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. Commented 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. Commented 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/… Commented Jun 24, 2018 at 22:30

1 Answer 1


Based on Joseph Jay Zeman's book Modal Logic: The Lewis-Modal Systems (see the Lemon-style bases in the Appendix), 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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .