Stalnaker (1975): Indicative Conditionals

This file formalizes [Sta75]'s account of the direct argument, either the butler or the gardener did it, so if the butler didn't, the gardener did. The indicative conditional has the selection-function truth condition of [Sta68], and entails the material conditional without being entailed by it (Conditional.selectionConditional_subset_materialImp, not_entails_direct). What makes the argument compelling is pragmatic: in a context, an indicative conditional's selection function keeps to the context set whenever the antecedent is compatible with it (pragmaticConstraint), and a disjunction is appropriately asserted only where each disjunct can hold without the other. Under Stalnaker's earlier condition (4) on selection functions, the constraint says that restricting the selection function to the context set changes nothing at context worlds (pragmaticConstraint_iff_restrict). Under the constraint, a proposition accepted in the context is accepted under any compatible antecedent (selectionConditional_of_accepted), the indicative and the material conditional are accepted in the same contexts (accepted_iff_material), and so the direct argument, contraposition and the hypothetical syllogism are reasonable for indicatives though invalid (direct_argument, contraposition, hypothetical_syllogism).

The appendix's calculus makes reasonable inference a logical notion: a pragmatic interpretation assigns each sentence a proposition in a context, an appropriateness relation and a change function obeying two postulates, and an inference is reasonable when every context in which its premisses are appropriately asserted in sequence comes to entail its conclusion (PragmaticInterpretation.Reasonable). An entailment whose conclusion expresses the same proposition in every context is reasonable (Reasonable.of_entails). On the language of the direct argument, whose contexts carry a selection function obeying the constraint, the direct argument is reasonable in the language (direct_argument_reasonable) though not an entailment in it. The fatalist's argument (fatalism) draws each of its conditional conclusions reasonably within the context that supposes a disjunct, and fails only by detaching them: constructive dilemma, valid for entailment (Entails.or), does not hold for reasonable inference.

Implementation notes

A context of the conditional language is a context set together with a selection function obeying the pragmatic constraint for it, and assertion restricts the selection function to the updated set, so that indicatives conform to the constraint after every assertion. The appropriateness relation encodes the paper's two generalizations, that a disjunction requires each disjunct to be open without the other and that an indicative conditional requires a compatible antecedent, together with the first postulate. Subjunctive conditionals, which suspend the constraint, are outside the language.

References

• [Sta75]
• [Sta68]
• [Gri75]
• [And51]

The pragmatic constraint

def Stalnaker1975.pragmaticConstraint {W : Type u_1} (s : Conditional.SelectionFunction W) (C : Set W) : Prop

The pragmatic constraint on a selection function relative to a context set C. At a world of C, an antecedent true somewhere in C selects a world of C, which Stalnaker glosses as the worlds of the context set being closer to each other than to any world outside it.

Equations

• Stalnaker1975.pragmaticConstraint s C = ∀ (w : W) (A : Set W), w ∈ C → (A ∩ C).Nonempty → s.sel w A ∈ C

theorem Stalnaker1975.pragmaticConstraint_restrict {W : Type u_1} (s : Conditional.SelectionFunction W) (C : Set W) : pragmaticConstraint (s.restrict C) C

The restriction of a selection function to a context obeys the pragmatic constraint for that context.

theorem Stalnaker1975.pragmaticConstraint_iff_restrict {W : Type u_1} {C : Set W} {s : Conditional.SelectionFunction W} (hs : s.IsCSO) : pragmaticConstraint s C ↔ ∀ w ∈ C, ∀ (A : Set W), (s.restrict C).sel w A = s.sel w A

Under Stalnaker's condition (4), the pragmatic constraint says that restricting the selection function to the context set changes nothing at context worlds.

theorem Stalnaker1975.mem_selectionConditional_of_forall_mem {W : Type u_1} (s : Conditional.SelectionFunction W) {C p q : Set W} {w : W} (hw : w ∈ C) (hopen : (p ∩ C).Nonempty) (hC : pragmaticConstraint s C) (himp : ∀ w' ∈ C, w' ∈ p → w' ∈ q) : w ∈ Conditional.selectionConditional s p q

At a context world, for an antecedent compatible with the context and a selection function meeting the pragmatic constraint, the selection conditional holds whenever the material conditional holds throughout the context.

The indicative conditional in a context

theorem Stalnaker1975.selectionConditional_of_accepted {W : Type u_1} (s : Conditional.SelectionFunction W) {C p q : Set W} (hC : pragmaticConstraint s C) (hp : ∃ w ∈ C, w ∈ p) (hq : ∀ w ∈ C, w ∈ q) (w : W) : w ∈ C → w ∈ Conditional.selectionConditional s p q

A proposition accepted in a context is accepted under any antecedent compatible with the context, once the selection function obeys the pragmatic constraint.

theorem Stalnaker1975.direct_argument {W : Type u_1} (s : Conditional.SelectionFunction W) {C p q : Set W} (hC : pragmaticConstraint s C) (hopen : ∃ w ∈ C, w ∉ p) (hdisj : ∀ w ∈ C, w ∈ p ∨ w ∈ q) (w : W) : w ∈ C → w ∈ Conditional.selectionConditional s pᶜ q

The direct argument is reasonable, since in a context accepting the disjunction where the negated first disjunct is open, the indicative conditional is accepted.

theorem Stalnaker1975.accepted_iff_material {W : Type u_1} (s : Conditional.SelectionFunction W) {C p q : Set W} (hC : pragmaticConstraint s C) (hp : ∃ w ∈ C, w ∈ p) : (∀ w ∈ C, w ∈ Conditional.selectionConditional s p q) ↔ ∀ w ∈ C, w ∈ p → w ∈ q

In a context compatible with the antecedent, the indicative and the material conditional are accepted together.

theorem Stalnaker1975.contraposition {W : Type u_1} (s : Conditional.SelectionFunction W) {C p q : Set W} (hC : pragmaticConstraint s C) (hq : ∃ w ∈ C, w ∉ q) (h : ∀ w ∈ C, w ∈ Conditional.selectionConditional s p q) (w : W) : w ∈ C → w ∈ Conditional.selectionConditional s qᶜ pᶜ

Contraposition is reasonable for indicatives, since when the conditional is accepted and the negated consequent is open, the contrapositive is accepted.

theorem Stalnaker1975.hypothetical_syllogism {W : Type u_1} (s : Conditional.SelectionFunction W) {C p q r : Set W} (hC : pragmaticConstraint s C) (hp : ∃ w ∈ C, w ∈ p) (h₁ : ∀ w ∈ C, w ∈ Conditional.selectionConditional s p q) (h₂ : ∀ w ∈ C, w ∈ Conditional.selectionConditional s q r) (w : W) : w ∈ C → w ∈ Conditional.selectionConditional s p r

The hypothetical syllogism is reasonable for indicatives, since when both conditionals are accepted and the first antecedent is open, the chained conditional is accepted.

Reasonable inference

structure Stalnaker1975.PragmaticInterpretation (L : Type u_1) (W : Type u_2) (K : Type u_3) : Type (max (max u_1 u_2) u_3)

A pragmatic interpretation of a language, the paper's appendix, gives the proposition each sentence expresses in a context, an appropriateness relation, and a change function, obeying the two postulates that an appropriate assertion is compatible with the context and that an assertion adds its proposition to the context set.

• contextSet : K → Set W

  The context set of a context.

• prop : L → K → Set W

  The proposition a sentence expresses in a context.

• appropriate : L → K → Prop

  Appropriateness of asserting a sentence in a context.

• change : L → K → K

  The context resulting from asserting a sentence.

• appropriate_compatible (P : L) (k : K) : self.appropriate P k → (self.contextSet k ∩ self.prop P k).Nonempty

  The first postulate: an appropriate assertion is compatible with the context.

• contextSet_change (P : L) (k : K) : self.contextSet (self.change P k) = self.contextSet k ∩ self.prop P k

  The second postulate: an assertion narrows the context set to its proposition.

def Stalnaker1975.PragmaticInterpretation.changeSeq {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) (σ : List L) (k : K) : K

The context after asserting a sequence of sentences.

Equations

• I.changeSeq σ k = List.foldl (fun (k : K) (P : L) => I.change P k) k σ

def Stalnaker1975.PragmaticInterpretation.AppropriateSeq {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) : List L → K → Prop

A sequence of sentences is appropriate when each is appropriate in the context the preceding ones produce.

Equations

• I.AppropriateSeq [] x✝ = True
• I.AppropriateSeq (P :: σ) x✝ = (I.appropriate P x✝ ∧ I.AppropriateSeq σ (I.change P x✝))

def Stalnaker1975.PragmaticInterpretation.Reasonable {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) (σ : List L) (P : L) : Prop

An inference is reasonable when every context in which the premisses are appropriately asserted in sequence comes to entail the conclusion.

Equations

• I.Reasonable σ P = ∀ (k : K), I.AppropriateSeq σ k → I.contextSet (I.changeSeq σ k) ⊆ I.prop P (I.changeSeq σ k)

def Stalnaker1975.PragmaticInterpretation.Entails {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) (P Q : L) : Prop

A sentence entails another in the language when the premiss's proposition is included in the conclusion's in every context.

Equations

• I.Entails P Q = ∀ (k : K), I.prop P k ⊆ I.prop Q k

def Stalnaker1975.PragmaticInterpretation.Rigid {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) (P : L) : Prop

A sentence is rigid when it expresses the same proposition in every context.

Equations

• I.Rigid P = ∀ (k k' : K), I.prop P k = I.prop P k'

theorem Stalnaker1975.PragmaticInterpretation.changeSeq_singleton {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) (P : L) (k : K) : I.changeSeq [P] k = I.change P k

theorem Stalnaker1975.PragmaticInterpretation.Reasonable.of_entails {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) {P Q : L} (hQ : I.Rigid Q) (h : I.Entails P Q) : I.Reasonable [P] Q

An entailment of a rigid conclusion is a reasonable inference.

theorem Stalnaker1975.PragmaticInterpretation.Entails.or {L : Type u_1} {W : Type u_2} {K : Type u_3} (I : PragmaticInterpretation L W K) {P₁ P₂ Q₁ Q₂ P Q : L} (hP : ∀ (k : K), I.prop P k = I.prop P₁ k ∪ I.prop P₂ k) (hQ : ∀ (k : K), I.prop Q k = I.prop Q₁ k ∪ I.prop Q₂ k) (h₁ : I.Entails P₁ Q₁) (h₂ : I.Entails P₂ Q₂) : I.Entails P Q

Constructive dilemma holds for entailment, since with disjunction interpreted as union, entailments from the disjuncts yield an entailment from the disjunction.

The language of the direct argument

inductive Stalnaker1975.Sentence (Atom : Type u_1) : Type u_1

The sentences are built from atoms by negation, disjunction, and the indicative conditional.

• atom {Atom : Type u_1} (a : Atom) : Sentence Atom
• not {Atom : Type u_1} (P : Sentence Atom) : Sentence Atom
• or {Atom : Type u_1} (P Q : Sentence Atom) : Sentence Atom
• ifThen {Atom : Type u_1} (P Q : Sentence Atom) : Sentence Atom

structure Stalnaker1975.Context (W : Type u_1) : Type u_1

A context is a context set with a selection function obeying the pragmatic constraint for it.

• set : Set W

  The context set.

• sel : Conditional.SelectionFunction W

  The selection function of the context.

• constraint : pragmaticConstraint self.sel self.set

  Indicative conditionals conform to the constraint.

def Stalnaker1975.Sentence.prop {Atom : Type u_1} {W : Type u_2} (V : Atom → Set W) : Sentence Atom → Context W → Set W

The proposition a sentence expresses in a context under a valuation of the atoms.

Equations

• Stalnaker1975.Sentence.prop V (Stalnaker1975.Sentence.atom a) x✝ = V a
• Stalnaker1975.Sentence.prop V P.not x✝ = (Stalnaker1975.Sentence.prop V P x✝)ᶜ
• Stalnaker1975.Sentence.prop V (P.or Q) x✝ = Stalnaker1975.Sentence.prop V P x✝ ∪ Stalnaker1975.Sentence.prop V Q x✝
• Stalnaker1975.Sentence.prop V (P.ifThen Q) x✝ = Conditional.selectionConditional x✝.sel (Stalnaker1975.Sentence.prop V P x✝) (Stalnaker1975.Sentence.prop V Q x✝)

def Stalnaker1975.Sentence.Appropriate {Atom : Type u_1} {W : Type u_2} (V : Atom → Set W) : Sentence Atom → Context W → Prop

An assertion is appropriate when it is compatible with the context, a disjunction moreover requires each disjunct to be open without the other, and an indicative conditional requires a compatible antecedent.

Equations

• One or more equations did not get rendered due to their size.
• Stalnaker1975.Sentence.Appropriate V (P.ifThen Q) x✝ = ((x✝.set ∩ Stalnaker1975.Sentence.prop V P x✝).Nonempty ∧ (x✝.set ∩ Stalnaker1975.Sentence.prop V (P.ifThen Q) x✝).Nonempty)
• Stalnaker1975.Sentence.Appropriate V x✝¹ x✝ = (x✝.set ∩ Stalnaker1975.Sentence.prop V x✝¹ x✝).Nonempty

noncomputable def Stalnaker1975.Context.update {W : Type u_2} (k : Context W) (P : Set W) : Context W

The context after accepting a proposition has the narrowed context set with the selection function restricted to it.

Equations

• k.update P = { set := k.set ∩ P, sel := k.sel.restrict (k.set ∩ P), constraint := ⋯ }

noncomputable def Stalnaker1975.interp {Atom : Type u_1} {W : Type u_2} (V : Atom → Set W) : PragmaticInterpretation (Sentence Atom) W (Context W)

The pragmatic interpretation of the language under a valuation.

Equations

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

def Stalnaker1975.ReasonableInL {Atom : Type u_1} (W : Type u_3) (σ : List (Sentence Atom)) (P : Sentence Atom) : Prop

An inference is reasonable in the language when it is reasonable under every valuation.

Equations

• Stalnaker1975.ReasonableInL W σ P = ∀ (V : Atom → Set W), (Stalnaker1975.interp V).Reasonable σ P

def Stalnaker1975.EntailsInL {Atom : Type u_1} (W : Type u_3) (P Q : Sentence Atom) : Prop

A sentence entails another in the language when it does so under every valuation.

Equations

• Stalnaker1975.EntailsInL W P Q = ∀ (V : Atom → Set W), (Stalnaker1975.interp V).Entails P Q

theorem Stalnaker1975.ifThen_entails_material {Atom : Type u_1} {W : Type u_2} (P Q : Sentence Atom) : EntailsInL W (P.ifThen Q) (P.not.or Q)

The indicative conditional entails the material conditional in the language.

theorem Stalnaker1975.direct_argument_reasonable {Atom : Type u_1} {W : Type u_2} (a b : Atom) : ReasonableInL W [(Sentence.atom a).or (Sentence.atom b)] ((Sentence.atom a).not.ifThen (Sentence.atom b))

The direct argument is reasonable in the language, since wherever a disjunction of atoms is appropriately asserted, the context comes to accept the conditional from the negated first disjunct to the second.

The direct argument is not an entailment

inductive Stalnaker1975.Suspect : Type

The suspects.

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

@[instance_reducible]

instance Stalnaker1975.instDecidableEqSuspect : DecidableEq Suspect

Equations

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

@[instance_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.

inductive Stalnaker1975.Culprit : Type

The atoms of the butler-or-gardener argument.

• butler : Culprit
• gardener : Culprit

@[instance_reducible]

instance Stalnaker1975.instDecidableEqCulprit : DecidableEq Culprit

Equations

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

@[instance_reducible]

instance Stalnaker1975.instReprCulprit : Repr Culprit

Equations

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

def Stalnaker1975.instReprCulprit.repr : Culprit → ℕ → Std.Format

Equations

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

def Stalnaker1975.culpritOf : Culprit → Set Suspect

The valuation on which each atom names its suspect.

Equations

• Stalnaker1975.culpritOf Stalnaker1975.Culprit.butler = {Stalnaker1975.Suspect.butler}
• Stalnaker1975.culpritOf Stalnaker1975.Culprit.gardener = {Stalnaker1975.Suspect.gardener}

noncomputable def Stalnaker1975.someoneElseFirst : Conditional.SelectionFunction Suspect

A selection function that, off the antecedent, reaches for someone else first.

Equations

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

theorem Stalnaker1975.not_entails_direct : ¬EntailsInL Suspect ((Sentence.atom Culprit.butler).or (Sentence.atom Culprit.gardener)) ((Sentence.atom Culprit.butler).not.ifThen (Sentence.atom Culprit.gardener))

At a world where the butler did it, the butler or the gardener did it holds while if the butler didn't, the gardener did fails: the direct argument is no entailment.

Fatalism

inductive Stalnaker1975.Fate : Type

The atoms of the fatalist's argument are being killed and taking precautions.

• killed : Fate
• precautions : Fate

@[instance_reducible]

instance Stalnaker1975.instDecidableEqFate : DecidableEq Fate

Equations

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

def Stalnaker1975.instReprFate.repr : Fate → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Stalnaker1975.instReprFate.repr Stalnaker1975.Fate.killed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Stalnaker1975.Fate.killed")).group prec✝

@[instance_reducible]

instance Stalnaker1975.instReprFate : Repr Fate

Equations

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

@[reducible, inline]

abbrev Stalnaker1975.Outcome : Type

A world records whether one is killed and whether one takes precautions.

Equations

• Stalnaker1975.Outcome = (Bool × Bool)

def Stalnaker1975.fateOf : Fate → Set Outcome

The valuation of the fatalist's atoms.

Equations

• Stalnaker1975.fateOf Stalnaker1975.Fate.killed = {w : Stalnaker1975.Outcome | w.1 = true}
• Stalnaker1975.fateOf Stalnaker1975.Fate.precautions = {w : Stalnaker1975.Outcome | w.2 = true}

noncomputable def Stalnaker1975.survivalFirst : Conditional.SelectionFunction Outcome

A selection function that, off the antecedent, reaches first for survival.

Equations

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

noncomputable def Stalnaker1975.fateCtx : Context Outcome

The null context of the fatalist, with a selection function reaching first for survival.

Equations

• Stalnaker1975.fateCtx = { set := Set.univ, sel := Stalnaker1975.survivalFirst, constraint := ⋯ }

def Stalnaker1975.killed : Sentence Fate

I will be killed.

Equations

• Stalnaker1975.killed = Stalnaker1975.Sentence.atom Stalnaker1975.Fate.killed

def Stalnaker1975.precautions : Sentence Fate

I take precautions.

Equations

• Stalnaker1975.precautions = Stalnaker1975.Sentence.atom Stalnaker1975.Fate.precautions

theorem Stalnaker1975.fatalism : Sentence.Appropriate fateOf (killed.or killed.not) fateCtx ∧ (fateCtx.update (Sentence.prop fateOf killed fateCtx)).set ⊆ Sentence.prop fateOf (precautions.ifThen killed) (fateCtx.update (Sentence.prop fateOf killed fateCtx)) ∧ (fateCtx.update (Sentence.prop fateOf killed.not fateCtx)).set ⊆ Sentence.prop fateOf (precautions.not.ifThen killed.not) (fateCtx.update (Sentence.prop fateOf killed.not fateCtx)) ∧ ¬(fateCtx.update (Sentence.prop fateOf (killed.or killed.not) fateCtx)).set ⊆ Sentence.prop fateOf ((precautions.ifThen killed).or (precautions.not.ifThen killed.not)) (fateCtx.update (Sentence.prop fateOf (killed.or killed.not) fateCtx))

The fatalist argues I will be killed or not; if I will, then even with precautions I will be killed; if I will not, then even without precautions I will not be; so precautions are ineffective or unnecessary. In the null context the disjunction is appropriate, and each conditional is accepted in the context supposing its disjunct; but the disjunction of the conditionals is not accepted in the context of the disjunctive premiss, since at a world where one is killed without precautions neither conditional holds. Constructive dilemma fails for reasonable inference.