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

1 Answer 1


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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.