Stalnaker 1975 [Sta75]

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 CommonGround.HasAssertion (§ 4 below): the Stalnaker-1975 change-function calculus is shown to be the Stalnaker-instance projection of the framework-generic HasAssertion.assert. The direct-argument theorem then lifts to: for ANY HasAssertion 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 the substrate section above.

Integration

• pragmaticConstraint, selectionConditional, moodedConditional, Mood.admissibleSelection, selectionConditional_eq_material_within_context, moodedConditional_indicative_eq_material_within_context — in 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 the substrate section above.
• This file: a butler/gardener witness for (4); abstract version of (4) parameterised over any constraint-respecting selection function.

See also

• 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.

Reasonable Inference [Sta75]

Stalnaker 1975's Appendix introduces a pragmatic notion of inference, distinct from semantic entailment. The idea: an inference from a sequence of premise assertions (P₁, …, Pₙ) to a conclusion Q is reasonable when, in every context in which the premises can appropriately be asserted in sequence, the resulting context entails Q.

The formal apparatus is a triple (⟦·⟧, A, g):

• ⟦P⟧_k: the proposition expressed by P in context k (the semantic interpretation, here just a Set W);
• A(P, k): the appropriateness relation — whether asserting P in context k is appropriate;
• g(P, k) = k ∩ ⟦P⟧_k: the change function — the new context after asserting P. This is exactly CommonGround.ContextSet.update.

This module defines Appropriateness, sequential appropriateness A*, sequential update g*, and the reasonableInference predicate.

Stalnaker's proposal is that entailment ⊊ reasonable inference — inferences like the "direct argument" (A or B; ∴ if not-A, B) are reasonable without being entailments. The Stalnaker1975 study file exhibits the gap.

@[reducible, inline]

abbrev Discourse.ReasonableInference.Appropriateness (W : Type u_1) : Type u_1

Appropriateness of a sentence in a context. Stalnaker leaves this maximally schematic; concrete theories of conditionals, disjunction, presupposition fill it in. Two universal constraints from the Appendix are captured below as compatible_of_appropriate and the change-function identity.

Equations

• Discourse.ReasonableInference.Appropriateness W = (Set W → CommonGround.ContextSet W → Prop)

def Discourse.ReasonableInference.changeFn {W : Type u_1} (P : Set W) (k : CommonGround.ContextSet W) : CommonGround.ContextSet W

The change function g(P, k) = k ∩ ⟦P⟧_k. Already exists as ContextSet.update; this is the Stalnakerian alias.

Equations

• Discourse.ReasonableInference.changeFn P k = k.update P

def Discourse.ReasonableInference.changeFnSeq {W : Type u_1} (σ : List (Set W)) (k : CommonGround.ContextSet W) : CommonGround.ContextSet W

Sequential update along a list of asserted sentences.

Equations

• Discourse.ReasonableInference.changeFnSeq σ k = List.foldl (fun (acc : CommonGround.ContextSet W) (P : Set W) => Discourse.ReasonableInference.changeFn P acc) k σ

def Discourse.ReasonableInference.appropriateSeq {W : Type u_1} (A : Appropriateness W) (σ : List (Set W)) (k : CommonGround.ContextSet W) : Prop

Sequential appropriateness: each Pᵢ is appropriate in the context obtained by updating with P₁, …, Pᵢ₋₁. Stalnaker's A(σ, k) = ⋀ᵢ A(Pᵢ, kᵢ).

Equations

• Discourse.ReasonableInference.appropriateSeq A [] k = True
• Discourse.ReasonableInference.appropriateSeq A (P :: rest) k = (A P k ∧ Discourse.ReasonableInference.appropriateSeq A rest (Discourse.ReasonableInference.changeFn P k))

def Discourse.ReasonableInference.reasonableInference {W : Type u_1} (A : Appropriateness W) (σ : List (Set W)) (Q : Set W) : Prop

Reasonable inference ([Sta75] Appendix).

σ ⊨ᵣ Q (reasonable-in-A) iff in every context k in which the premise sequence is appropriate, the post-update context entails the conclusion.

This is distinct from ContextSet.entails (changeFnSeq σ k) ⟦Q⟧ for arbitrary k: reasonable inference quantifies only over contexts in which the premises can be asserted in sequence. The premise filter is exactly what lets pragmatic information (e.g., the disjunction- appropriateness condition) feed into the inference.

Equations

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

theorem Discourse.ReasonableInference.entailment_implies_reasonable {W : Type u_1} (A : Appropriateness W) (P Q : Set W) (h_ent : ∀ (w : W), P w → Q w) : reasonableInference A [P] Q

Entailment ⇒ reasonable inference for any appropriateness relation: if a single premise semantically entails the conclusion, the inference is also reasonable. The converse is the substantive Stalnakerian claim and fails — see the direct-argument theorem in Stalnaker1975.

theorem Discourse.ReasonableInference.reasonable_nil {W : Type u_1} (A : Appropriateness W) (Q : Set W) : reasonableInference A [] Q ↔ ∀ (w : W), Q w

Empty premise sequence: a reasonable inference from no premises is just universal validity of the conclusion.

def Discourse.ReasonableInference.respectsCompatibility {W : Type u_1} (A : Appropriateness W) : Prop

Stalnaker's first universal constraint ([Sta75] Appendix, postulate 1): one cannot appropriately assert a proposition in a context incompatible with it. Any concrete A should satisfy this.

Equations

• Discourse.ReasonableInference.respectsCompatibility A = ∀ (P : Set W) (k : CommonGround.ContextSet W), A P k → k.compatible P

theorem Discourse.ReasonableInference.changeFn_eq {W : Type u_1} (P : Set W) (k : CommonGround.ContextSet W) (w : W) : changeFn P k w ↔ k w ∧ P w

Stalnaker's second universal constraint ([Sta75] Appendix, postulate 2): the change function commutes with the interpretation — g(P, k) = k ∩ ⟦P⟧_k. This holds by construction of changeFn.

theorem Stalnaker1975.direct_argument_reasonable {W : Type u_1} (s : Semantics.Conditionals.SelectionFunction W) (C : 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 Semantics.Mood.GramMood.indicative s notA B w

Stalnaker's direct argument is reasonable ([Sta75] §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) (𝒜 : Discourse.ReasonableInference.Appropriateness W) (h_𝒜 : ∀ (k : CommonGround.ContextSet W), 𝒜 AorB k → Semantics.Conditionals.pragmaticConstraint s (Discourse.ReasonableInference.changeFn AorB k) ∧ ∃ w' ∈ {w' : W | notA w'}, Discourse.ReasonableInference.changeFn AorB k w') : Discourse.ReasonableInference.reasonableInference 𝒜 [AorB] (Semantics.Conditionals.moodedConditional Semantics.Mood.GramMood.indicative s notA B)

The direct argument is reasonable as a reasonableInference ([Sta75] 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 ⋯

@[implicit_reducible]

instance Stalnaker1975.instReprSuspect : Repr Suspect

Equations

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

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

Equations

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

@[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 Semantics.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 Semantics.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 [Sta75] emphasises.

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

1. The changeFn operator IS the projection of HasAssertion.assert in EVERY HasAssertion framework — the typeclass's toContextSet_assert law restated through changeFn = ContextSet.update.
2. The direct-argument theorem lifts to be polymorphic over [HasAssertion 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 CommonGround.HasAssertion typeclass's existence: a substantive philosophical claim (reasonable inference is framework-generic) given a substrate-level proof (the typeclass's update law is sufficient).

theorem Stalnaker1975.assert_eq_changeFn {S : Type u_1} {W : Type u_2} [CommonGround.HasAssertion S W] (s : S) (p : Set W) : CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s p) = Discourse.ReasonableInference.changeFn p (CommonGround.HasContextSet.toContextSet s)

Bridge theorem: Stalnaker's changeFn operator equals the HasContextSet-projection of HasAssertion.assert — in any HasAssertion framework, since changeFn p k is definitionally ContextSet.update k p (Stalnaker 1975 Appendix postulate 2) and the typeclass's update law demands exactly that projection.

theorem Stalnaker1975.direct_argument_reasonable_polymorphic {S : Type u_1} {W : Type u_2} [CommonGround.HasAssertion 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 (CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB))) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB) w') (w : W) : CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB) w → Semantics.Conditionals.moodedConditional Semantics.Mood.GramMood.indicative sel notA B w

Polymorphic direct argument: for ANY HasAssertion 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 HasAssertion typeclass provides one of the hypotheses for free: every world surviving the assertion satisfies AorB (the typeclass law assert_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 : CommonGround 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 (CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB))) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB) w') (w : W) : CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB) w → Semantics.Conditionals.moodedConditional Semantics.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 : Discourse.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 (CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB))) (h_open_notA : ∃ w' ∈ {w' : W | notA w'}, CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB) w') (w : W) : CommonGround.HasContextSet.toContextSet (CommonGround.HasAssertion.assert s AorB) w → Semantics.Conditionals.moodedConditional Semantics.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 HasAssertion typeclass abstracts over the representational difference.

Contraposition / hypothetical syllogism

[Sta75] 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.