Scoring the accounts on Chemla & Schlenker (2012)

Chemla and Schlenker's inferential experiments rate, for if-, or- and unless-sentences with too, whether the conditional or the unconditional presupposition follows. Each cell is scored in four steps. The fact is the inference endorsed more in the cell (observed). Its parse is the target sentence, a formula of the propositional fragment that every theory reads (target). The theory says which contexts accept that formula (Theory.accepts). The linking hypothesis, that subjects infer the presupposition a sentence is predicted to carry (the paper's §2.3.1), turns the acceptance conditions into a predicted inference: the unconditional one if the theory predicts it, otherwise the conditional one if the theory predicts that, and nothing if it predicts neither (predicted). Each experiment scores a theory cell by cell (experiment1, experiment4), for a registered account or for a theory under development alike.

Every account accepts a target sentence iff the context entails if p, q, except that the incremental accounts, which coincide on the fragment (Eval.Projection.edges), require the unconditional q in the inverse order (accepts_target_iff). The conditional inference is endorsed more in every tested cell of both experiments (observed_experiment1, observed_experiment4). So every incremental account is wrong on each inverse-order sentence and right on each canonical one, and every other account, the symmetric ones and Limited Symmetry, is right on all (verdict_experiment1, verdict_experiment4).

References

• [CS12]
• [Sch09a]
• [Kal23]

def Eval.Projection.ChemlaSchlenker2012.incremental : List Account

The incremental accounts.

Equations

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

Acceptance of the target sentences

theorem Eval.Projection.ChemlaSchlenker2012.triggers_target (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : (List.map Prod.snd (ChemlaSchlenker2012.target 0 1 2 k o).triggers).Nodup

The target sentences carry one trigger.

theorem Eval.Projection.ChemlaSchlenker2012.accepts_target_iff {W : Type} (I : Fin 3 → Set W) {C : Set W} (a : Account) (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : a.Accepts I C (ChemlaSchlenker2012.target 0 1 2 k o) ↔ C ⊆ if a ∈ incremental ∧ o = ChemlaSchlenker2012.Order.inverse then I 1 else {w : W | w ∈ I 0 → w ∈ I 1}

Every account accepts a target sentence iff the context entails the conditional presupposition if p, q, except that an incremental account requires the unconditional q in the inverse order.

Predictions, observations and verdicts

noncomputable def Eval.Projection.ChemlaSchlenker2012.predicted (T : Theory) (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : Option ChemlaSchlenker2012.Inference

The linking hypothesis of the experiments as a rule. A theory predicts that subjects endorse the unconditional inference q from the target sentence of a cell if it predicts that inference, and otherwise the conditional inference if p, q if it predicts that one. A theory that predicts neither predicts nothing about the cell.

Equations

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

theorem Eval.Projection.ChemlaSchlenker2012.predicted_eq (a : Account) (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : predicted a.theory k o = some (if a ∈ incremental ∧ o = ChemlaSchlenker2012.Order.inverse then ChemlaSchlenker2012.Inference.unconditional else ChemlaSchlenker2012.Inference.conditional)

def Eval.Projection.ChemlaSchlenker2012.observedIn {R : Type} (rows : List R) (cell : R → ChemlaSchlenker2012.Construction × ChemlaSchlenker2012.Order) (inference : R → ChemlaSchlenker2012.Inference) (mean : R → ℚ) (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : Option ChemlaSchlenker2012.Inference

The inference endorsed more in a cell, among rows recording the mean rating of an inference in a cell, if the cell was tested and the two means differ.

Equations

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

def Eval.Projection.ChemlaSchlenker2012.observed1 : ChemlaSchlenker2012.Construction → ChemlaSchlenker2012.Order → Option ChemlaSchlenker2012.Inference

The inference endorsed more in a cell of Experiment 1 (Table 4).

Equations

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

def Eval.Projection.ChemlaSchlenker2012.observed4 : ChemlaSchlenker2012.Construction → ChemlaSchlenker2012.Order → Option ChemlaSchlenker2012.Inference

The inference endorsed more in a cell of Experiment 4 (Table 7).

Equations

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

noncomputable def Eval.Projection.ChemlaSchlenker2012.experiment1 : Experiment Theory (ChemlaSchlenker2012.Construction × ChemlaSchlenker2012.Order) ChemlaSchlenker2012.Inference

Experiment 1 of [CS12], whose inferences are rated in Table 4.

Equations

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

noncomputable def Eval.Projection.ChemlaSchlenker2012.experiment4 : Experiment Theory (ChemlaSchlenker2012.Construction × ChemlaSchlenker2012.Order) ChemlaSchlenker2012.Inference

Experiment 4 of [CS12], whose inferences are rated in Table 7.

Equations

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

theorem Eval.Projection.ChemlaSchlenker2012.observed_experiment1 (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : experiment1.observed (k, o) = if k = ChemlaSchlenker2012.Construction.unlessSentence ∧ o = ChemlaSchlenker2012.Order.canonical then none else some ChemlaSchlenker2012.Inference.conditional

By Table 4, the conditional inference is endorsed more in every tested cell, and the unless-sentence in the canonical order was not tested.

theorem Eval.Projection.ChemlaSchlenker2012.observed_experiment4 (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : experiment4.observed (k, o) = if k = ChemlaSchlenker2012.Construction.unlessSentence ∧ o = ChemlaSchlenker2012.Order.canonical then none else some ChemlaSchlenker2012.Inference.conditional

By Table 7, the conditional inference is endorsed more in every tested cell, and the unless-sentence in the canonical order was not tested.

theorem Eval.Projection.ChemlaSchlenker2012.verdict_experiment1 (a : Account) (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : experiment1.verdict a.theory (k, o) = if k = ChemlaSchlenker2012.Construction.unlessSentence ∧ o = ChemlaSchlenker2012.Order.canonical then Verdict.silent else if a ∈ incremental ∧ o = ChemlaSchlenker2012.Order.inverse then Verdict.wrong else Verdict.correct

On Experiment 1, every incremental account is wrong on each inverse-order sentence and right on each canonical one, and every other account is right on all.

theorem Eval.Projection.ChemlaSchlenker2012.verdict_experiment4 (a : Account) (k : ChemlaSchlenker2012.Construction) (o : ChemlaSchlenker2012.Order) : experiment4.verdict a.theory (k, o) = if k = ChemlaSchlenker2012.Construction.unlessSentence ∧ o = ChemlaSchlenker2012.Order.canonical then Verdict.silent else if a ∈ incremental ∧ o = ChemlaSchlenker2012.Order.inverse then Verdict.wrong else Verdict.correct

On Experiment 4, as on Experiment 1, every incremental account is wrong on each inverse-order sentence and right on each canonical one, and every other account is right on all.