Reasonable Inference @cite{stalnaker-1975}

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 Core.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 Dialogue.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

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

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

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

Equations

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

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

Sequential update along a list of asserted sentences.

Equations

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

def Dialogue.ReasonableInference.appropriateSeq {W : Type u_1} (A : Appropriateness W) (σ : List (Set W)) (k : Core.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

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

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

Reasonable inference (@cite{stalnaker-1975} 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 Dialogue.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 Dialogue.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 Dialogue.ReasonableInference.respectsCompatibility {W : Type u_1} (A : Appropriateness W) : Prop

Stalnaker's first universal constraint (@cite{stalnaker-1975} Appendix, postulate 1): one cannot appropriately assert a proposition in a context incompatible with it. Any concrete A should satisfy this.

Equations

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

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

Stalnaker's second universal constraint (@cite{stalnaker-1975} Appendix, postulate 2): the change function commutes with the interpretation — g(P, k) = k ∩ ⟦P⟧_k. This holds by construction of changeFn.