Erotetic reasoning with alternatives

The erotetic theory of reasoning of Koralus and Mascarenhas treats the premises of a deductive task asymmetrically: a disjunction-like first premise raises a set of alternatives, a question; the second premise is a hint toward an answer; the reasoner selects the alternative the hint bears on and reads conclusions off the selected alternative, a mental-models analog of conjunction elimination. A Problem is the alternative set with its hint; a conclusion is Illusory under a selection rule when some selected alternative yields it although it does not follow from the premises' classical content. The selection rule is a parameter: Matches is the exact content overlap of the mental-models and erotetic literature, the alternative carrying the hint's content, and Overlaps is bare consistency with the hint; probabilistic rules such as selection by confirmation are study-specific refinements. The schema indirect covers the classical illusory inference from disjunction as the special case where the hint is the first conjunct itself (disjunction_eq_indirect), and matching provably undergenerates the indirect case while certifying the classical one.

The generators formalized with the schema are the three the literature has established: disjunction, indefinites (one alternative per witness), and the epistemic modal might, whose attentive content is the alternative pair of the prejacent with the tautology.

Implementation notes

• Alternatives are bare Set W propositions; Matches p := p ⊆ hint renders exact content overlap semantically, with no syntactic conjunct structure.
• Under the weak Overlaps rule the symmetric conclusion of the classical schema is also certified (disjunction_illusory_overlaps_right): the rule records attention, not the asymmetry, which comes from the selection theory.

References

• [KM13e]
• [KM18]
• [WJL04]
• [MK17]
• [MP19]
• [SMM22]
• [BPCM22]

structure Erotetic.Problem (W : Type u_2) : Type u_2

A reasoning problem whose first premise raises alternatives and whose second premise is a hint.

• alts : Set (Set W)

  The Hamblin alternatives raised by the first premise.

• hint : Set W

  The second premise.

def Erotetic.Problem.premises {W : Type u_1} (P : Problem W) : Set W

The classical content of the two premises together.

Equations

• P.premises = ⋃₀ P.alts ∩ P.hint

def Erotetic.Problem.Entails {W : Type u_1} (P : Problem W) (q : Set W) : Prop

A conclusion follows classically from the premises.

Equations

• P.Entails q = (P.premises ⊆ q)

def Erotetic.Problem.selected {W : Type u_1} (P : Problem W) (p : Set W) : Set W

The erotetic selection of the alternative p as the answer: the alternative with the hint.

Equations

• P.selected p = p ∩ P.hint

def Erotetic.Problem.Overlaps {W : Type u_1} (P : Problem W) (p : Set W) : Prop

Bare overlap: the hint is consistent with the alternative.

Equations

• P.Overlaps p = (P.selected p).Nonempty

def Erotetic.Problem.Matches {W : Type u_1} (P : Problem W) (p : Set W) : Prop

Exact matching: the alternative carries the hint's content, the selection procedure of the mental-models account and the erotetic theory.

Equations

• P.Matches p = (p ⊆ P.hint)

def Erotetic.Problem.Illusory {W : Type u_1} (P : Problem W) (sel : Set W → Prop) (q : Set W) : Prop

A conclusion is illusory under the selection rule sel when some selected alternative the hint partially overlaps yields it by conjunction elimination, though it does not follow classically.

Equations

• P.Illusory sel q = ((∃ p ∈ P.alts, sel p ∧ (P.selected p).Nonempty ∧ P.selected p ⊆ q) ∧ ¬P.Entails q)

theorem Erotetic.Problem.Illusory.mono {W : Type u_1} (P : Problem W) {sel sel' : Set W → Prop} (h : ∀ (p : Set W), sel p → sel' p) {q : Set W} (hq : P.Illusory sel q) : P.Illusory sel' q

Weakening the selection rule preserves illusions.

def Erotetic.disjunction {W : Type u_1} (a b c : Set W) : Problem W

The classical schema: the premise (a ∧ b) ∨ c raising {a ∧ b, c}, with hint a.

Equations

• Erotetic.disjunction a b c = { alts := {a ∩ b, c}, hint := a }

def Erotetic.indirect {W : Type u_1} (a b c d : Set W) : Problem W

The indirect schema: the same disjunctive premise with an arbitrary hint d.

Equations

• Erotetic.indirect a b c d = { alts := {a ∩ b, c}, hint := d }

def Erotetic.might {W : Type u_1} (p : Set W) : Set (Set W)

might φ raises the alternatives {φ, ⊤}, its attentive content.

Equations

• Erotetic.might p = {p, Set.univ}

def Erotetic.mightProblem {W : Type u_1} (a b : Set W) : Problem W

The might schema: might (a ∧ b) with hint a.

Equations

• Erotetic.mightProblem a b = { alts := Erotetic.might (a ∩ b), hint := a }

def Erotetic.indefinite {W : Type u_1} {E : Type u_2} (P : E → Set W) (D : Set E) (hint : Set W) : Problem W

An indefinite raises one alternative per member of its domain.

Equations

• Erotetic.indefinite P D hint = { alts := P '' D, hint := hint }

theorem Erotetic.disjunction_eq_indirect {W : Type u_1} {a b c : Set W} : disjunction a b c = indirect a b c a

The classical schema is the indirect schema whose hint is the first conjunct itself.

@[simp]

theorem Erotetic.premises_indirect {W : Type u_1} {a b c d : Set W} : (indirect a b c d).premises = (a ∩ b ∪ c) ∩ d

@[simp]

theorem Erotetic.premises_disjunction {W : Type u_1} {a b c : Set W} : (disjunction a b c).premises = (a ∩ b ∪ c) ∩ a

theorem Erotetic.indirect_invalid {W : Type u_1} {a b c d : Set W} (h : ((c ∩ d) \ b).Nonempty) : ¬(indirect a b c d).Entails b

The schema is classically invalid: a world verifying the second disjunct and the hint but not the conclusion.

theorem Erotetic.indirect_illusory {W : Type u_1} {a b c d : Set W} {sel : Set W → Prop} (hsel : sel (a ∩ b)) (hab : (a ∩ b ∩ d).Nonempty) (h : ((c ∩ d) \ b).Nonempty) : (indirect a b c d).Illusory sel b

Whatever rule selects the first disjunct yields the illusion.

theorem Erotetic.matches_disjunction_iff {W : Type u_1} {a b c : Set W} (hc : (c \ a).Nonempty) {p : Set W} (hp : p ∈ {a ∩ b, c}) : (disjunction a b c).Matches p ↔ p = a ∩ b

In the classical schema, matching selects exactly the first disjunct.

theorem Erotetic.disjunction_illusory_matches {W : Type u_1} {a b c : Set W} (hab : (a ∩ b).Nonempty) (h : ((c ∩ a) \ b).Nonempty) : (disjunction a b c).Illusory (disjunction a b c).Matches b

The classical illusory inference from disjunction, under exact matching.

theorem Erotetic.disjunction_illusory_overlaps_right {W : Type u_1} {a b c : Set W} (hca : (c ∩ a).Nonempty) (h : ((a ∩ b) \ c).Nonempty) : (disjunction a b c).Illusory (disjunction a b c).Overlaps c

Under bare overlap the symmetric, unattractive conclusion is certified too: Overlaps records attention, not the selection asymmetry.

theorem Erotetic.not_matches_right {W : Type u_1} {a b c : Set W} (hc : (c \ a).Nonempty) : ¬(disjunction a b c).Matches c

Matching never selects the second disjunct of the classical schema.

theorem Erotetic.indirect_not_illusory_matches {W : Type u_1} {a b c d : Set W} (h₁ : ((a ∩ b) \ d).Nonempty) (h₂ : (c \ d).Nonempty) (q : Set W) : ¬(indirect a b c d).Illusory (indirect a b c d).Matches q

Exact matching undergenerates the indirect schema: when neither alternative carries the hint, no conclusion at all is illusory under matching.

theorem Erotetic.mightProblem_eq_disjunction {W : Type u_1} {a b : Set W} : mightProblem a b = disjunction a b Set.univ

The might schema is the classical schema with the tautologous second disjunct.

@[simp]

theorem Erotetic.sUnion_might {W : Type u_1} (p : Set W) : ⋃₀ might p = Set.univ

The might premise is informationally idle.

theorem Erotetic.might_ne_of_ne_univ {W : Type u_1} {p : Set W} (hp : p ≠ Set.univ) : might p ≠ might Set.univ

It is nevertheless not the alternative set of the tautology.

theorem Erotetic.might_illusory {W : Type u_1} {a b : Set W} (hab : (a ∩ b).Nonempty) (h : (a \ b).Nonempty) : (mightProblem a b).Illusory (mightProblem a b).Matches b

The might conclusion is illusory under matching.

theorem Erotetic.indefinite_illusory {W : Type u_1} {E : Type u_2} {P : E → Set W} {D : Set E} {hint : Set W} {john : E} (hj : john ∈ D) (hw : (P john ∩ hint).Nonempty) (hcm : ∃ x ∈ D, ((P x ∩ hint) \ P john).Nonempty) : (indefinite P D hint).Illusory (indefinite P D hint).Overlaps (P john)

The indefinite conclusion about a witness is illusory under overlap whenever another witness could verify the indefinite: its match is on the individual, which bare propositions cannot see.

Posteriors over the schema

Conditioning a measure on the schema's premises cannot separate the attractive conclusion from the symmetric one: the premises distribute, and the two posteriors agree exactly when the priors of the two conjunctions do.

theorem Erotetic.premises_eq_distrib {W : Type u_1} (A B C : Set W) : (A ∩ B ∪ C) ∩ A = A ∩ B ∪ A ∩ C

The premises ((a ∧ b) ∨ c) ∧ a are classically (a ∧ b) ∨ (a ∧ c).

theorem Erotetic.premises_inter_left {W : Type u_1} (A B C : Set W) : (A ∩ B ∪ C) ∩ A ∩ B = A ∩ B

theorem Erotetic.premises_inter_right {W : Type u_1} (A B C : Set W) : (A ∩ B ∪ C) ∩ A ∩ C = A ∩ C

theorem Erotetic.posterior_eq_iff {W : Type u_1} {A B C : Set W} [MeasurableSpace W] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (hE : MeasurableSet ((A ∩ B ∪ C) ∩ A)) (h0 : μ ((A ∩ B ∪ C) ∩ A) ≠ 0) : μ[B | (A ∩ B ∪ C) ∩ A] = μ[C | (A ∩ B ∪ C) ∩ A] ↔ μ (A ∩ B) = μ (A ∩ C)

Conditioning any finite measure on the premises, the posteriors of b and of c agree iff the priors of a ∧ b and a ∧ c do: a posterior-based account distinguishes the conclusions only through the priors.