Docs / Studies / Studies.Stalnaker1968

A Theory of Conditionals

Stalnaker, R. C. (1968). In Studies in Logical Theory (pp. 98–112). Blackwell

Stalnaker evaluates if A, B at the world a selection function picks for A: a world where A holds, the base world when A holds there, and an absurd world, where every sentence holds, when no possible world verifies A. This file takes as primitive the conditional of the closest accessible antecedent-worlds (Conditional.orderingImp) and reads the absurd world as an empty domain. Under Stalnaker's assumption, that each world's similarity ordering is linear and well-founded, the closest accessible antecedent-world satisfies the paper's four conditions on a selection function (IsSelectionFunction), and conditions (3) and (4) in turn make the priority a selection establishes a total ordering of the selected worlds. The logic C2 adds the corner > to classical propositional logic and defines necessity as ¬A > A.

Errata

Footnote 7 makes the modal logic of C2 S4 when relative possibility is transitive and S5 when it is also symmetric. As Mandelkern observes, condition (2) lets a selection function reach worlds not possible relative to the base world, and defined necessity is necessity over the worlds selected (IsSelectionFunction.mem_ofDomain_compl_iff). With relative possibility the identity, □A ⊃ □□A fails (exists_not_box_imp_box_box). Under Stalnaker's assumption the selected worlds are the possible ones and footnote 7 holds (box_imp_box_box_minimals).

TODO

The completeness of C2, proved by Stalnaker and Thomason.

References

Stalnaker 1968, A Theory of Conditionals
Stalnaker & Thomason 1970, A Semantic Analysis of Conditional Logic
Mandelkern 2018, The Case of the Missing ‘If’: Accessibility Relations in Stalnaker’s Theory of Conditionals

Selection functions

L52–69

Under Stalnaker's assumption, a centered similarity ordering that is linear and well-founded, the closest accessible antecedent-world is a selection function.

theorem isSelectionFunction_minimals L71–85

{W : Type u_1} {R : W → Set W} {ord : W → Preorder W} (hR : ∀ (w : W), w ∈ R w) (hc : Conditional.IsCentered ord) (htot : ∀ (w : W), Std.Total LE.le) (hanti : ∀ (w : W), Std.Antisymm LE.le) (hwf : ∀ (w : W), WellFounded LT.lt) :

IsSelectionFunction R fun (w : W) (A : Set W) => (ord w).minimals (R w ∩ A)

Built from

L87–95

Priority

A selection establishes an ordering of the worlds it selects (fn. 8): selecting v for an antecedent makes v prior to every world of the antecedent. When each domain is a set of antecedent-worlds with at most one member, condition (4) says that priority is antisymmetric, and priority is then a total ordering of the selected worlds.

Conditions (3) and (4) make priority a total ordering of the selected worlds (§II).

theorem IsSelectionFunction.isLinearOrder_prior L157–162

{W : Type u_1} {R : W → Set W} {D : W → Set W → Set W} (hM : IsSelectionFunction R D) (w : W) :

IsLinearOrder { v : W // Prior D w v v } fun (x1 x2 : { v : W // Prior D w v v }) => Prior D w ↑x1 ↑x2

Built from ,

Priority is the order that choices from pairs reveal: v is prior to u exactly when v is the world selected from {v, u}, the ordering of SelectionFunction.IsCSO.linearOrder.

theorem IsSelectionFunction.prior_iff_mem_pair L164–170

{W : Type u_1} {R : W → Set W} {D : W → Set W → Set W} {w v : W} (hM : IsSelectionFunction R D) {u : W} :

Prior D w v u ↔ v ∈ D w {v, u}

Built from ,

L173–174

L176–180

L182–186

The formal system C2

Every theorem of C2 is valid.

theorem Provable.sound L281–308

{α : Type u_2} {A : Formula α} (h : Provable A) :

Valid A

Built from , ,

L310–312

When the antecedent is possible, a denied conditional is equivalent to the conditional with the opposite consequent (§III, (2)).

theorem provable_neg_corner L314–320

{α : Type u_2} (A B : Formula α) :

Provable (A.dia.imp ((A.corner B).neg.iff (A.corner B.neg)))

Built from , , ,

Invalid inferences

The countermodels order three worlds cyclically, 0 closest to itself, then 1, then 2.

The corner is not transitive: if Hoover were a communist he would be a traitor, and if he had been born a Russian he would be a communist, but not: if he had been born a Russian he would be a traitor.

theorem not_valid_trans L347–357

¬Valid ((((Formula.atom 0).corner (Formula.atom 1)).and ((Formula.atom 1).corner (Formula.atom 2))).imp ((Formula.atom 0).corner (Formula.atom 2)))

Built from ,

Strengthening the antecedent fails: if the match were struck it would light, but not if it had been soaked overnight and were struck.

theorem not_valid_strengthening L359–368

¬Valid (((Formula.atom 0).corner (Formula.atom 2)).imp (((Formula.atom 0).and (Formula.atom 1)).corner (Formula.atom 2)))

Built from ,

Contraposition fails: if the bombing were halted North Vietnam would not negotiate, but not: if North Vietnam negotiated the bombing would not have been halted.

theorem not_valid_contraposition L370–378

¬Valid (((Formula.atom 0).corner (Formula.atom 1)).imp ((Formula.atom 1).neg.corner (Formula.atom 0).neg))

Built from

Valid inferences

Footnote 10 notes that C follows from A > B, B > C and A, and that the biconditional is transitive; footnote 11 that modus tollens is valid.

L385–391

L393–399

L401–405

Defined necessity