Stalnaker 1975 @cite{stalnaker-1975}

Indicative Conditionals. Philosophia 5(3): 269–286.

Core contributions formalized here

1. The pragmatic constraint on selection (§III): if i ∈ C, then f(A,i) ∈ C whenever some A-world is in C.

2. Indicative ≠ subjunctive at the pragmatic level (§III/IV): both have the same truth-conditional clause; subjunctive mood signals that the pragmatic constraint may be suspended.

3. Disjunction-appropriateness (§III): A or B is appropriately asserted only in contexts where both ¬A∧B and A∧¬B are open.

4. The direct argument is a reasonable inference but not an entailment (§IV): from A or B, infer if ¬A, B.

   • direct_argument_reasonable: in any context where the disjunction can be appropriately asserted, the post-update context makes the indicative conditional true at every surviving world.
   • direct_argument_not_entailment: a single concrete world model exhibits a selection function for which A∨B holds at a world but if ¬A, B fails — so the inference is not semantic entailment.

5. Fatalism failure (§V): sketched in fatalism_remark as a docstring; the formal point is that constructive dilemma is valid only for entailments, not for reasonable inferences.

6. Polymorphic lift via Dialogue.Assertable (§ 4 below): the Stalnaker-1975 change-function calculus is shown to be the Stalnaker-instance projection of the framework-generic Assertable.speakerAssert. The direct-argument theorem then lifts to: for ANY Assertable framework, the direct argument from A∨B to if ¬A, B is a reasonable inference. Stalnaker's pragmatic claim is framework-generic, not Stalnaker-representation-specific.

The two universal pragmatic postulates from the Appendix (respectsCompatibility, changeFn_eq) are stated in Theories/Pragmatics/Assertion/ReasonableInference.lean.

Integration

• pragmaticConstraint, selectionConditional, moodedConditional, Mood.admissibleSelection, selectionConditional_eq_material_within_context, moodedConditional_indicative_eq_material_within_context — in Theories/Semantics/Conditionals/Basic.lean. The mood distinction lives in Mood.admissibleSelection, not in two parallel conditional defs: .indicative requires pragmaticConstraint, .subjunctive imposes none.
• Appropriateness, changeFn, reasonableInference — in Theories/Pragmatics/Assertion/ReasonableInference.lean.
• This file: a butler/gardener witness for (4); abstract version of (4) parameterised over any constraint-respecting selection function.

See also

• Phenomena/Modality/Studies/CarianiSantorio2018.lean — extends the Stalnaker selection-function mechanism from conditionals to bare will. C&S's Semantics.Conditionals.SelectionFunction infrastructure is exactly the one used here for selectionConditional; the would-conditional / Stalnaker-counterfactual identification in C&S §5.3.2 reuses this paper's selection-function semantics under universe parameter.

theorem Stalnaker1975.direct_argument_reasonable {W : Type u_1} (s : Semantics.Conditionals.SelectionFunction W) (C : Core.CommonGround.ContextSet W) (notA B AorB : W → Prop) (h_constraint : Semantics.Conditionals.pragmaticConstraint s C) (h_C_AorB : ∀ (w : W), C w → AorB w) (h_AorB_decomp : ∀ (w : W), AorB w → notA w → B w) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, C w') (w : W) : C w → Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative s notA B w

Stalnaker's direct argument is reasonable (@cite{stalnaker-1975} §IV).

Quantified over any selection function s and context C such that:

• s obeys the pragmatic constraint relative to C;
• the antecedent ¬A is open in C (some context-set world is ¬A);
• in C, every world satisfies A ∨ B (i.e., the disjunction is established as common ground after assertion);

the indicative conditional if ¬A, B is true at every world in C.

This is the substance of §IV: no individual semantic entailment is invoked; the pragmatic constraint plus the post-update common ground are enough.

Stalnaker's appropriateness condition for disjunction (§III, end) — that asserting A or B requires both ¬A∧B and A∧¬B to be open in the prior context — is what guarantees h_open_notA after the update.

theorem Stalnaker1975.direct_argument_reasonableInference {W : Type u_1} (s : Semantics.Conditionals.SelectionFunction W) (notA B AorB : W → Prop) (h_AorB_decomp : ∀ (w : W), AorB w → notA w → B w) (𝒜 : Dialogue.ReasonableInference.Appropriateness W) (h_𝒜 : ∀ (k : Core.CommonGround.ContextSet W), 𝒜 AorB k → Semantics.Conditionals.pragmaticConstraint s (Dialogue.ReasonableInference.changeFn AorB k) ∧ ∃ w' ∈ {w' : W | notA w'}, Dialogue.ReasonableInference.changeFn AorB k w') : Dialogue.ReasonableInference.reasonableInference 𝒜 [AorB] (Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative s notA B)

The direct argument is reasonable as a reasonableInference (@cite{stalnaker-1975} Appendix), in the sense of the change-function calculus: in every prior context k such that asserting A∨B lands one in a Stalnakerian indicative-friendly state, the post-update context entails the indicative conditional.

The Appropriateness relation here bundles the two contextual facts the disjunction-appropriateness condition guarantees: the pragmatic constraint holds, and ¬A remains open after the update.

inductive Stalnaker1975.Suspect : Type

Three worlds for the butler/gardener model. The third world makes B false at a possible selection target, exhibiting the gap.

• butler : Suspect
• gardener : Suspect
• someoneElse : Suspect

@[implicit_reducible]

instance Stalnaker1975.instDecidableEqSuspect : DecidableEq Suspect

Equations

• Stalnaker1975.instDecidableEqSuspect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Stalnaker1975.instReprSuspect.repr : Suspect → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Stalnaker1975.instReprSuspect : Repr Suspect

Equations

• Stalnaker1975.instReprSuspect = { reprPrec := Stalnaker1975.instReprSuspect.repr }

@[reducible, inline]

abbrev Stalnaker1975.W3 : Type

Equations

• Stalnaker1975.W3 = Stalnaker1975.Suspect

def Stalnaker1975.A3 : W3 → Prop

Equations

• Stalnaker1975.A3 s = (s = Stalnaker1975.Suspect.butler)

def Stalnaker1975.B3 : W3 → Prop

Equations

• Stalnaker1975.B3 s = (s = Stalnaker1975.Suspect.gardener)

def Stalnaker1975.AorB3 : W3 → Prop

Equations

• Stalnaker1975.AorB3 s = (Stalnaker1975.A3 s ∨ Stalnaker1975.B3 s)

def Stalnaker1975.notA3 : W3 → Prop

Equations

• Stalnaker1975.notA3 s = ¬Stalnaker1975.A3 s

@[implicit_reducible]

instance Stalnaker1975.instDecidablePredW3A3 : DecidablePred A3

Equations

• Stalnaker1975.instDecidablePredW3A3 s = decEq s Stalnaker1975.Suspect.butler

@[implicit_reducible]

instance Stalnaker1975.instDecidablePredW3B3 : DecidablePred B3

Equations

• Stalnaker1975.instDecidablePredW3B3 s = decEq s Stalnaker1975.Suspect.gardener

@[implicit_reducible]

instance Stalnaker1975.instDecidablePredW3AorB3 : DecidablePred AorB3

Equations

• Stalnaker1975.instDecidablePredW3AorB3 s = instDecidableOr

@[implicit_reducible]

instance Stalnaker1975.instDecidablePredW3NotA3 : DecidablePred notA3

Equations

• Stalnaker1975.instDecidablePredW3NotA3 s = instDecidableNot

noncomputable def Stalnaker1975.s_subj3 : Semantics.Conditionals.SelectionFunction W3

A "subjunctive" selection function on W3 that, for any nonempty antecedent set, picks someoneElse first if available — modelling selection that reaches outside the natural context set.

Equations

• One or more equations did not get rendered due to their size.

theorem Stalnaker1975.direct_argument_not_entailment : AorB3 Suspect.butler ∧ ¬Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative s_subj3 notA3 B3 Suspect.butler

Counterexample to the direct argument as a semantic entailment.

At w = butler, A∨B = true, but s_subj3.sel butler {¬A worlds} = someoneElse, where B fails. So if ¬A, B is false at butler under this selection function.

theorem Stalnaker1975.direct_argument_holds_under_indicative_selection (s : Semantics.Conditionals.SelectionFunction W3) : (Semantics.Conditionals.pragmaticConstraint s fun (w : W3) => w ≠ Suspect.someoneElse ∧ AorB3 w) → Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative s notA3 B3 Suspect.butler

Sanity check: with any indicative selection function (one that obeys the pragmatic constraint relative to C), the conditional does hold at every C-world satisfying the disjunction. The contrast with direct_argument_not_entailment is the pragmatic-vs-semantic gap @cite{stalnaker-1975} emphasises.

Stalnaker 1975's change-function calculus uses changeFn p k (set intersection) as the post-assertion update operator. The Theories/Dialogue/Assertable.lean typeclass abstracts over any dialogue-state representation that admits Stalnakerian narrowing. This section shows that:

1. The changeFn operator IS the Stalnaker-instance projection of Assertable.speakerAssert (a 1-line bridge by Set.inter_comm).
2. The direct-argument theorem lifts to be polymorphic over [Assertable S W] — Stalnaker's "reasonable inference" claim doesn't depend on Stalnaker's particular state representation.
3. The lifted theorem applies cleanly to both the Stalnaker instance (the original framework) and the Krifka instance (a commitment-space representation with a radically different internal structure but the same projected context-set behavior).

This is the consumer that earns the Dialogue.Assertable typeclass's existence: a substantive philosophical claim (reasonable inference is framework-generic) given a substrate-level proof (the typeclass's narrowing law is sufficient).

theorem Stalnaker1975.stalnaker_speakerAssert_eq_changeFn {W : Type u_1} (s : Dialogue.Stalnaker.StalnakerState W) (p : Set W) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s p) = Dialogue.ReasonableInference.changeFn p (Core.CommonGround.HasContextSet.toContextSet s)

Bridge theorem: Stalnaker's changeFn operator equals the HasContextSet-projection of Assertable.speakerAssert at the Stalnaker instance.

changeFn p k = k ∩ p (Stalnaker 1975 Appendix postulate 2); HasContextSet.toContextSet (Stalnaker.assert s p) = p ∩ s.contextSet. They're equal up to Set.inter_comm.

theorem Stalnaker1975.direct_argument_reasonable_polymorphic {S : Type u_1} {W : Type u_2} [Dialogue.Assertable S W] (s : S) (sel : Semantics.Conditionals.SelectionFunction W) (notA B AorB : W → Prop) (h_AorB_decomp : ∀ (w : W), AorB w → notA w → B w) (h_constraint : Semantics.Conditionals.pragmaticConstraint sel (Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB))) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB) w') (w : W) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB) w → Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative sel notA B w

Polymorphic direct argument: for ANY Assertable framework, asserting A∨B yields a context set in which the indicative conditional if ¬A, B holds at every world.

The proof is shorter than its single-framework predecessor (direct_argument_reasonable) because the Assertable typeclass provides one of the hypotheses for free: every world surviving the assertion satisfies AorB (the typeclass law speakerAssert_narrows). Compare with the Stalnaker-specific version, which had to take this as a hypothesis (h_C_AorB).

theorem Stalnaker1975.direct_argument_reasonable_stalnaker {W : Type u_1} (s : Dialogue.Stalnaker.StalnakerState W) (sel : Semantics.Conditionals.SelectionFunction W) (notA B AorB : W → Prop) (h_AorB_decomp : ∀ (w : W), AorB w → notA w → B w) (h_constraint : Semantics.Conditionals.pragmaticConstraint sel (Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB))) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB) w') (w : W) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB) w → Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative sel notA B w

Stalnaker instance application: the polymorphic lift fires on the Stalnaker framework. Recovers the framework-specific direct_argument_reasonable for the post-assertion context.

theorem Stalnaker1975.direct_argument_reasonable_krifka {W : Type u_1} (s : Dialogue.Krifka.KrifkaState W) (sel : Semantics.Conditionals.SelectionFunction W) (notA B AorB : W → Prop) (h_AorB_decomp : ∀ (w : W), AorB w → notA w → B w) (h_constraint : Semantics.Conditionals.pragmaticConstraint sel (Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB))) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB) w') (w : W) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert s AorB) w → Semantics.Conditionals.moodedConditional Core.Mood.GramMood.indicative sel notA B w

Krifka instance application: the polymorphic lift fires on the commitment-space framework too. Krifka's KrifkaState represents the same dialogue state as a tree of indexed commitments rather than a flat list of propositions, but the direct-argument inference is equally valid — the Assertable typeclass abstracts over the representational difference.

Contraposition / hypothetical syllogism

@cite{stalnaker-1975} observes that contraposition and hypothetical syllogism fail in general for selection-based conditionals; the counterexamples all involve subjunctives whose antecedents are presupposed false. For indicatives — which obey pragmaticConstraint — both inference forms come out reasonable in the Appendix's sense.

The semantic-failure side already exists as Semantics.Conditionals.perfection_not_entailed_variablyStrict and can be adapted directly to selection-based conditionals. The pragmatic-success side is a clean extension of direct_argument_reasonable and is left for follow-up.

Fatalism (§V) fatalism_remark

Dummett's wartime-Britain fatalism argument has the form:

1. K ∨ ¬K (premise: I will be killed or not).
2. From K, derive If P, K (precautions ineffective).
3. From ¬K, derive If ¬P, ¬K (precautions unnecessary).
4. ∴ Q ∨ R.

Steps 2 and 3 are reasonable inferences (they exploit the post-update context where K or ¬K is taken as established). Step 4 applies constructive dilemma — valid for entailments, but not for reasonable inferences. The argument equivocates the two notions.

Formalising this requires the n-ary appropriateSeq machinery already present, plus a counterexample showing constructive dilemma fails for reasonable inference. Left for follow-up.