From a7439147592e4ad9db28f6874fb7b2642d37603e Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 3 Nov 2026 14:28:46 -0800 Subject: [PATCH 1/5] feat(Studies/Geurts2010): formalize the book's recipe and free choice --- Linglib/Data/Examples/Geurts2010.json | 531 +++++++++ Linglib/Data/Examples/Geurts2010.lean | 370 ++++++ Linglib/Data/Examples/contributions.csv | 1 + Linglib/Semantics/Exhaustification/Basic.lean | 7 + .../Exhaustification/InnocentExclusion.lean | 9 +- Studies/Fox2007.lean | 11 +- Studies/Geurts2010.lean | 1061 ++++++++++++++++- Studies/GeurtsPouscoulous2009.lean | 61 +- 8 files changed, 1984 insertions(+), 67 deletions(-) create mode 100644 Linglib/Data/Examples/Geurts2010.json create mode 100644 Linglib/Data/Examples/Geurts2010.lean diff --git a/Linglib/Data/Examples/Geurts2010.json b/Linglib/Data/Examples/Geurts2010.json new file mode 100644 index 0000000000..265be5191e --- /dev/null +++ b/Linglib/Data/Examples/Geurts2010.json @@ -0,0 +1,531 @@ +[ + { + "id": "geurts2010_table2_i", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 i, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma read some of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "false"], + ["quantifier", "some"], + ["alternative", "many"], + ["alternative", "most"], + ["alternative", "all"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_ii", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 ii, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma read many of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "false"], + ["quantifier", "many"], + ["alternative", "most"], + ["alternative", "all"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_iii", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 iii, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma read most of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "false"], + ["quantifier", "most"], + ["alternative", "all"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_iv", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 iv, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma read all of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "false"], + ["quantifier", "all"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_v", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 v, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma didn't read any of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "true"], + ["quantifier", "some"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_vi", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 vi, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma didn't read many of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "true"], + ["quantifier", "many"], + ["alternative", "some"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_vii", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 vii, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma didn't read most of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "true"], + ["quantifier", "most"], + ["alternative", "some"], + ["alternative", "many"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_table2_viii", + "source": {"bibkey": "geurts-2010", "paperLabel": "Table 2 viii, p. 58"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Wilma didn't read all of the papers", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["negated", "true"], + ["quantifier", "all"], + ["alternative", "some"], + ["alternative", "many"], + ["alternative", "most"] + ], + "comment": "The prediction of the definition (24) by Horn sets; *any* is the form of *some* under negation (p. 54).", + "verified": "page-image" + }, + { + "id": "geurts2010_11", + "source": {"bibkey": "geurts-2010", "paperLabel": "(11), p. 110"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "George is British or Canadian.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "disjunct"], + ["inference", "He may be British."], + ["conveys", "true"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_12", + "source": {"bibkey": "geurts-2010", "paperLabel": "(12), p. 110"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "George may be British or Canadian.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "freeChoice"], + ["inference", "He may be British."], + ["conveys", "true"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_19", + "source": {"bibkey": "geurts-2010", "paperLabel": "(19), p. 118"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "You can have fruit or chocolate cake.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "My son asks what is for dessert; the modal is deontic and performative.", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "freeChoice"], + ["inference", "You can have chocolate cake."], + ["conveys", "true"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_13", + "source": {"bibkey": "geurts-2010", "paperLabel": "(13), p. 112"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Many of the nurses were drunk.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "sameLength"], + ["inference", "George doesn't believe that all the nurses were drunk."], + ["conveys", "true"] + ], + "comment": "The weak implicature of pp. 113-114, which the strong one extends given Competence.", + "verified": "page-image" + }, + { + "id": "geurts2010_23", + "source": {"bibkey": "geurts-2010", "paperLabel": "(23), p. 122"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "It must have been a great party. I hear that well before midnight all the doctors, many though not all of the interns, and many of the nurses were drunk.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "afterUse"], + ["inference", "George doesn't know whether all the nurses were drunk."], + ["conveys", "true"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_26a", + "source": {"bibkey": "geurts-2010", "paperLabel": "(26a), p. 124"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "I hurt my finger.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "sameLength"], + ["inference", "I didn't hurt my thumb."], + ["conveys", "true"] + ], + "comment": "The weak form, that the speaker does not believe it; the form printed needs Competence (p. 114).", + "verified": "page-image" + }, + { + "id": "geurts2010_26b", + "source": {"bibkey": "geurts-2010", "paperLabel": "(26b), p. 124"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "I hurt my toe.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "longer"], + ["inference", "I didn't hurt my big toe."], + ["conveys", "false"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_6_figs", + "source": {"bibkey": "geurts-2010", "paperLabel": "(6), p. 166"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Cleo either had a mango or some of the figs.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "figs"], + ["inference", "Cleo didn't eat all the figs."], + ["conveys", "true"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_3", + "source": {"bibkey": "geurts-2010", "paperLabel": "(3), p. 165"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Cleo either had a mango or some of the figs.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "mango"], + ["inference", "Cleo didn't have a mango."], + ["conveys", "false"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_31_x", + "source": {"bibkey": "geurts-2010", "paperLabel": "(31), pp. 179-180"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Last year, a Dutch sailor showed some symptoms of delirium.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "referent"], + ["inference", "The sailor in question didn't show all the symptoms of delirium."], + ["conveys", "true"] + ], + "comment": "The model (35), given Competence about the discourse referent.", + "verified": "page-image" + }, + { + "id": "geurts2010_29", + "source": {"bibkey": "geurts-2010", "paperLabel": "(29), p. 144"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Last year, a Dutch sailor showed some of the symptoms of delirium.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["item", "everySailor"], + ["inference", "Last year, no Dutch sailor showed all the symptoms of delirium."], + ["conveys", "false"] + ], + "comment": "", + "verified": "page-image" + }, + { + "id": "geurts2010_61a", + "source": {"bibkey": "geurts-2010", "paperLabel": "(61a), p. 158"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "All the farmers in this region own goats or sheep.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["quantifier", "all"], + ["inference", "None of them own both."], + ["conveys", "false"] + ], + "comment": "Conventionalist theories unanimously predict the inference by default (p. 158).", + "verified": "page-image" + }, + { + "id": "geurts2010_61b", + "source": {"bibkey": "geurts-2010", "paperLabel": "(61b), p. 158"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "At least 300 of the farmers in this region own goats or sheep.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["quantifier", "moreThanOne"], + ["inference", "At least 300 of them don't own both."], + ["conveys", "false"] + ], + "comment": "Conventionalist theories unanimously predict the inference by default (p. 158).", + "verified": "page-image" + }, + { + "id": "geurts2010_61c", + "source": {"bibkey": "geurts-2010", "paperLabel": "(61c), p. 158"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "Only six farmers in this region own goats or sheep.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["quantifier", "exactlyTwo"], + ["inference", "Only six farmers in this region own goats or sheep but not both."], + ["conveys", "false"] + ], + "comment": "At least some conventionalist theories predict the inference by default (p. 158).", + "verified": "page-image" + }, + { + "id": "geurts2010_56a", + "source": {"bibkey": "geurts-2010", "paperLabel": "(56a), p. 156"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "I hope that some of my relatives will remember my birthday.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["attitude", "hope"], + ["inference", "I hope that not all of them will remember it."], + ["conveys", "false"] + ], + "comment": "Conventionalist theories predict the inference; p. 156 queries the arrow and p. 157 calls the prediction plain false.", + "verified": "page-image" + }, + { + "id": "geurts2010_56b", + "source": {"bibkey": "geurts-2010", "paperLabel": "(56b), p. 156"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "You have to read some of these papers.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["attitude", "have to"], + ["inference", "You're not allowed to read all of them."], + ["conveys", "false"] + ], + "comment": "Conventionalist theories predict the inference; p. 156 queries the arrow and p. 157 calls the prediction plain false.", + "verified": "page-image" + }, + { + "id": "geurts2010_56c", + "source": {"bibkey": "geurts-2010", "paperLabel": "(56c), p. 156"}, + "reportedIn": null, + "language": "stan1293", + "primaryText": "I want you to give me some of your biscuits.", + "discourseSegments": [], + "glossedTokens": [], + "translation": "", + "context": "", + "judgment": "acceptable", + "alternatives": [], + "readings": [], + "paperFeatures": [ + ["attitude", "want"], + ["inference", "I want you not to give me all of your biscuits."], + ["conveys", "false"] + ], + "comment": "Conventionalist theories predict the inference; p. 156 queries the arrow and p. 157 calls the prediction plain false.", + "verified": "page-image" + } +] diff --git a/Linglib/Data/Examples/Geurts2010.lean b/Linglib/Data/Examples/Geurts2010.lean new file mode 100644 index 0000000000..026812a93d --- /dev/null +++ b/Linglib/Data/Examples/Geurts2010.lean @@ -0,0 +1,370 @@ +module + +public import Linglib.Data.Examples.Schema + +/-! +# `Geurts2010` — typed example data + +Auto-generated from `Linglib/Data/Examples/Geurts2010.json` by +`scripts/gen_examples.py`. Do not edit by hand; edit the JSON and re-run +the generator. Consumers (the paper's study file, test-suite hubs) import +this module; declarations live in `namespace Geurts2010.Examples`. +-/ + +@[expose] public section + +namespace Geurts2010.Examples + +def table2_i : Datum := + { id := "geurts2010_table2_i" + source := ⟨"geurts-2010", "Table 2 i, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma read some of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "false"), ("quantifier", "some"), ("alternative", "many"), ("alternative", "most"), ("alternative", "all")] } + +def table2_ii : Datum := + { id := "geurts2010_table2_ii" + source := ⟨"geurts-2010", "Table 2 ii, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma read many of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "false"), ("quantifier", "many"), ("alternative", "most"), ("alternative", "all")] } + +def table2_iii : Datum := + { id := "geurts2010_table2_iii" + source := ⟨"geurts-2010", "Table 2 iii, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma read most of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "false"), ("quantifier", "most"), ("alternative", "all")] } + +def table2_iv : Datum := + { id := "geurts2010_table2_iv" + source := ⟨"geurts-2010", "Table 2 iv, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma read all of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "false"), ("quantifier", "all")] } + +def table2_v : Datum := + { id := "geurts2010_table2_v" + source := ⟨"geurts-2010", "Table 2 v, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma didn't read any of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "true"), ("quantifier", "some")] } + +def table2_vi : Datum := + { id := "geurts2010_table2_vi" + source := ⟨"geurts-2010", "Table 2 vi, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma didn't read many of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "true"), ("quantifier", "many"), ("alternative", "some")] } + +def table2_vii : Datum := + { id := "geurts2010_table2_vii" + source := ⟨"geurts-2010", "Table 2 vii, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma didn't read most of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "true"), ("quantifier", "most"), ("alternative", "some"), ("alternative", "many")] } + +def table2_viii : Datum := + { id := "geurts2010_table2_viii" + source := ⟨"geurts-2010", "Table 2 viii, p. 58"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Wilma didn't read all of the papers" + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("negated", "true"), ("quantifier", "all"), ("alternative", "some"), ("alternative", "many"), ("alternative", "most")] } + +def ex_11 : Datum := + { id := "geurts2010_11" + source := ⟨"geurts-2010", "(11), p. 110"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "George is British or Canadian." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "disjunct"), ("inference", "He may be British."), ("conveys", "true")] } + +def ex_12 : Datum := + { id := "geurts2010_12" + source := ⟨"geurts-2010", "(12), p. 110"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "George may be British or Canadian." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "freeChoice"), ("inference", "He may be British."), ("conveys", "true")] } + +def ex_19 : Datum := + { id := "geurts2010_19" + source := ⟨"geurts-2010", "(19), p. 118"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "You can have fruit or chocolate cake." + glossedTokens := [] + context := "My son asks what is for dessert; the modal is deontic and performative." + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "freeChoice"), ("inference", "You can have chocolate cake."), ("conveys", "true")] } + +def ex_13 : Datum := + { id := "geurts2010_13" + source := ⟨"geurts-2010", "(13), p. 112"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Many of the nurses were drunk." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "sameLength"), ("inference", "George doesn't believe that all the nurses were drunk."), ("conveys", "true")] } + +def ex_23 : Datum := + { id := "geurts2010_23" + source := ⟨"geurts-2010", "(23), p. 122"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "It must have been a great party. I hear that well before midnight all the doctors, many though not all of the interns, and many of the nurses were drunk." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "afterUse"), ("inference", "George doesn't know whether all the nurses were drunk."), ("conveys", "true")] } + +def ex_26a : Datum := + { id := "geurts2010_26a" + source := ⟨"geurts-2010", "(26a), p. 124"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "I hurt my finger." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "sameLength"), ("inference", "I didn't hurt my thumb."), ("conveys", "true")] } + +def ex_26b : Datum := + { id := "geurts2010_26b" + source := ⟨"geurts-2010", "(26b), p. 124"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "I hurt my toe." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "longer"), ("inference", "I didn't hurt my big toe."), ("conveys", "false")] } + +def ex_6_figs : Datum := + { id := "geurts2010_6_figs" + source := ⟨"geurts-2010", "(6), p. 166"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Cleo either had a mango or some of the figs." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "figs"), ("inference", "Cleo didn't eat all the figs."), ("conveys", "true")] } + +def ex_3 : Datum := + { id := "geurts2010_3" + source := ⟨"geurts-2010", "(3), p. 165"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Cleo either had a mango or some of the figs." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "mango"), ("inference", "Cleo didn't have a mango."), ("conveys", "false")] } + +def ex_31_x : Datum := + { id := "geurts2010_31_x" + source := ⟨"geurts-2010", "(31), pp. 179-180"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Last year, a Dutch sailor showed some symptoms of delirium." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "referent"), ("inference", "The sailor in question didn't show all the symptoms of delirium."), ("conveys", "true")] } + +def ex_29 : Datum := + { id := "geurts2010_29" + source := ⟨"geurts-2010", "(29), p. 144"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Last year, a Dutch sailor showed some of the symptoms of delirium." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("item", "everySailor"), ("inference", "Last year, no Dutch sailor showed all the symptoms of delirium."), ("conveys", "false")] } + +def ex_61a : Datum := + { id := "geurts2010_61a" + source := ⟨"geurts-2010", "(61a), p. 158"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "All the farmers in this region own goats or sheep." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("quantifier", "all"), ("inference", "None of them own both."), ("conveys", "false")] } + +def ex_61b : Datum := + { id := "geurts2010_61b" + source := ⟨"geurts-2010", "(61b), p. 158"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "At least 300 of the farmers in this region own goats or sheep." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("quantifier", "moreThanOne"), ("inference", "At least 300 of them don't own both."), ("conveys", "false")] } + +def ex_61c : Datum := + { id := "geurts2010_61c" + source := ⟨"geurts-2010", "(61c), p. 158"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "Only six farmers in this region own goats or sheep." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("quantifier", "exactlyTwo"), ("inference", "Only six farmers in this region own goats or sheep but not both."), ("conveys", "false")] } + +def ex_56a : Datum := + { id := "geurts2010_56a" + source := ⟨"geurts-2010", "(56a), p. 156"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "I hope that some of my relatives will remember my birthday." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("attitude", "hope"), ("inference", "I hope that not all of them will remember it."), ("conveys", "false")] } + +def ex_56b : Datum := + { id := "geurts2010_56b" + source := ⟨"geurts-2010", "(56b), p. 156"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "You have to read some of these papers." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("attitude", "have to"), ("inference", "You're not allowed to read all of them."), ("conveys", "false")] } + +def ex_56c : Datum := + { id := "geurts2010_56c" + source := ⟨"geurts-2010", "(56c), p. 156"⟩ + reportedIn := none + method := some .introspection + language := "stan1293" + primaryText := "I want you to give me some of your biscuits." + glossedTokens := [] + context := "" + judgment := .acceptable + alternatives := [] + readings := [] + paperFeatures := [("attitude", "want"), ("inference", "I want you not to give me all of your biscuits."), ("conveys", "false")] } + +def all : List Datum := [table2_i, table2_ii, table2_iii, table2_iv, table2_v, table2_vi, table2_vii, table2_viii, ex_11, ex_12, ex_19, ex_13, ex_23, ex_26a, ex_26b, ex_6_figs, ex_3, ex_31_x, ex_29, ex_61a, ex_61b, ex_61c, ex_56a, ex_56b, ex_56c] + +end Geurts2010.Examples diff --git a/Linglib/Data/Examples/contributions.csv b/Linglib/Data/Examples/contributions.csv index 442845dc84..3dc7045c93 100644 --- a/Linglib/Data/Examples/contributions.csv +++ b/Linglib/Data/Examples/contributions.csv @@ -244,6 +244,7 @@ GartnerGyuris2017,unclassified Gasparri2025,unclassified George2011,unclassified Geurts2005,unclassified +Geurts2010,introspection GeurtsPouscoulous2009,unclassified Giannakidou2002,unclassified GilesEtAl2026,unclassified diff --git a/Linglib/Semantics/Exhaustification/Basic.lean b/Linglib/Semantics/Exhaustification/Basic.lean index 213986517f..93b294e31b 100644 --- a/Linglib/Semantics/Exhaustification/Basic.lean +++ b/Linglib/Semantics/Exhaustification/Basic.lean @@ -105,6 +105,13 @@ theorem excludes_eq_compl_sUnion (C : Set (Set W)) (p : Set W) : theorem exh_eq_sdiff (C : Set (Set W)) (p : Set W) : exh C p = p \ ⋃₀ {q ∈ C | ¬ p ⊆ q} := by rw [exh, excludes_eq_compl_sUnion, Set.sdiff_eq] +/-- When every alternative is entailed by the prejacent or entails the non-entailed `q`, +exhaustifying removes just `q`. -/ +theorem exh_eq_sdiff_of_forall (hq : q ∈ C) (hpq : ¬ p ⊆ q) (h : ∀ r ∈ C, p ⊆ r ∨ r ⊆ q) : + exh C p = p \ q := + Set.ext fun _ ↦ and_congr_right fun _ ↦ ⟨fun hw hwq ↦ hpq (hw q hq hwq), + fun hw r hr hwr ↦ (h r hr).resolve_right fun hrq ↦ hw (hrq hwr)⟩ + theorem exh_eq_self_iff : exh C p = p ↔ ∀ q ∈ C, (p ∩ q).Nonempty → p ⊆ q := ⟨fun h q hq ⟨w, hw, hwq⟩ ↦ by rw [← h] at hw; exact hw.2 q hq hwq, fun h ↦ (exh_subset C p).antisymm fun w hw ↦ ⟨hw, fun q hq hwq ↦ h q hq ⟨w, hw, hwq⟩⟩⟩ diff --git a/Linglib/Semantics/Exhaustification/InnocentExclusion.lean b/Linglib/Semantics/Exhaustification/InnocentExclusion.lean index e99d796f89..502cd33a3e 100644 --- a/Linglib/Semantics/Exhaustification/InnocentExclusion.lean +++ b/Linglib/Semantics/Exhaustification/InnocentExclusion.lean @@ -298,12 +298,9 @@ theorem exhIE_singleton_self : exhIE {φ} φ = φ := exhIE_eq_self_of_forall _ _ fun _ ha _ ↦ (mem_singleton_iff.1 ha).ge theorem exhIE_pair_sdiff {d : Set World} (hne : (φ \ d).Nonempty) : exhIE {φ, d} φ = φ \ d := by - have hexh : exh {φ, d} φ = φ \ d := by - obtain ⟨w, hw, hwd⟩ := hne - ext u - simp only [mem_exh, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq, mem_sdiff] - exact and_congr_right fun _ ↦ ⟨fun h hud ↦ hwd (h.2 hud hw), fun hud ↦ - ⟨fun _ ↦ subset_rfl, fun h ↦ (hud h).elim⟩⟩ + have hexh : exh {φ, d} φ = φ \ d := exh_eq_sdiff_of_forall (by simp) + (fun h ↦ let ⟨_, hw, hwd⟩ := hne; hwd (h hw)) + (by rintro r (rfl | rfl); exacts [.inl subset_rfl, .inr subset_rfl]) rw [exhIE_eq_exh_of_nonempty _ _ (hexh ▸ hne), hexh] theorem not_isInnocentlyExcludable_of_subset_union (hfin : ALT.Finite) {p q : Set World} diff --git a/Studies/Fox2007.lean b/Studies/Fox2007.lean index 2e89f4d272..2cbbcd2bd0 100644 --- a/Studies/Fox2007.lean +++ b/Studies/Fox2007.lean @@ -231,13 +231,10 @@ theorem exhIE_w : exhIE {w, s, n, e} w = w \ e := by theorem exhIE_s : exhIE {w, s, n, e} s = s \ n := by obtain ⟨rfl, -, hn, ⟨a, has, han⟩, -⟩ := h - have hexh : exh {s ∪ n, s, n, e} s = s \ n := by - ext u - simp only [mem_exh, mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq, - mem_sdiff] - refine and_congr_right fun _ ↦ ⟨fun h' hun ↦ han (h'.2.2.1 hun has), fun hun ↦ - ⟨fun _ ↦ subset_union_left, fun _ ↦ subset_rfl, fun h' ↦ (hun h').elim, - fun h' ↦ (hun (hn h')).elim⟩⟩ + have hexh : exh {s ∪ n, s, n, e} s = s \ n := exh_eq_sdiff_of_forall (by simp) + (fun h ↦ han (h has)) (by + rintro r (rfl | rfl | rfl | rfl) + exacts [.inl subset_union_left, .inl subset_rfl, .inr subset_rfl, .inr hn]) rw [exhIE_eq_exh_of_nonempty _ _ (hexh ▸ ⟨a, has, han⟩), hexh] theorem exhIE_n : exhIE {w, s, n, e} n = n \ s := by diff --git a/Studies/Geurts2010.lean b/Studies/Geurts2010.lean index 2a14aa4f11..5abe2a9c51 100644 --- a/Studies/Geurts2010.lean +++ b/Studies/Geurts2010.lean @@ -1,60 +1,1045 @@ module public import Studies.GeurtsPouscoulous2009 +public import Linglib.Pragmatics.NeoGricean.Basic +public import Linglib.Semantics.Exhaustification.Basic +public import Linglib.Data.Examples.Geurts2010 +public import Mathlib.Algebra.Notation.Indicator +public import Mathlib.Order.Atoms +public import Mathlib.Order.Minimal +public import Mathlib.Order.UpperLower.Basic /-! # Geurts (2010): Quantity Implicatures -This file formalizes the textbook's case against conventionalism in section 7.3 of [geurts-2010], -which rests on [geurts-pouscoulous-2009]'s verification experiment. Conventionalist theories of -scalar inference agree that *some* is read as *some but not all* under an upward-entailing -quantifier such as *all* or *more than one*, and the stronger versions predict the same under a -non-monotone quantifier such as *exactly two*, while none predicts it under a downward-entailing -one; the experiment found no such readings. The three quantifiers of (62) are the earlier study's -`Quant`, and the weak and strong predictions are its `PredictsLocalSIWeak` and `PredictsLocalSI` -(`conventionalist_predictions`). Chapter 3's observation that a downward-entailing environment -reverses a scale, so that *not all* blocks the local inference, is the negated case -(`downward_entailing_blocks`). +A quantity implicature is an inference about a speaker's beliefs, drawn from the speaker's not +having said something stronger. If alternatives are closed under conjunction and disjunction, as +the book declines to do, and Competence is assumed wherever it is consistent, the Standard Recipe +[gives exactly the exclusive reading of a long +disjunction](##Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom), but under *may* it [leaves +the speaker no consistent state](##Sentence.standardRecipe_may_or_eq_empty). Starting from a +partition of the speaker's states gives [free choice](##Sentence.mem_survivors_may_or_iff) and +[form-sensitive scalar inferences](##Sentence.mem_survivors_scalar_iff). Comparing readings for +strength [picks out the upward-entailing scopes](##boundedReading_ssubset_iff) in which the +verification experiment finds no upper bound. + +## Implementation notes + +* A state is the set of worlds compatible with what the speaker believes. For the performative (19), + p. 118, it is read as what the speaker permits, the text giving the case the same logical + structure. +* `may` quantifies over the speaker's own state, so that the assumption of p. 111, footnote 5, that + a speaker who does not believe that something may be so believes that it is not, holds by + construction. +* `NeoGricean.IsSecondaryImplicature` is not the book's rule: the Standard Recipe is a heuristic and + the hearer may adopt or reject Competence (pp. 37, 39–40). It is used as the necessary condition + on Competence of p. 41, checked per alternative rather than jointly, and strengthening wherever it + holds is an assumption made here. +* `Sentence.survivors` applies the heuristic (i) categorically to single states with one alternative + per cell, where p. 116 has "probably", p. 121 weighs states against each other and pp. 113 and 115 + allow several sentences. `Sentence.Entails` preserves belief, not truth. +* `Sentence.size` stands in for economy and is one instance of the preorder `cost`, where lower + means more available (p. 123). Previous use in (23), p. 122, is modelled by lowering the sentence + to zero, although the text has the *construction* used, of the interns. +* (26b), p. 124, comes out under the heuristic (i) alone, by length, where the text credits + monolexicality and salience. +* The upper sets of the worlds of (29), p. 61, are the closure of the disjuncts under conjunction + and disjunction ([each is a union of conjunctions](##eq_iUnion_iInter_of_isUpperSet)), up to the + empty set and the whole space, neither of which bears on a strong implicature. +* The alternatives of (20) are a reconstruction, since p. 120 prints none; the extension to any + number of disjuncts in `inter_nonempty_of_forall_not_subset` is not the text's. A state of (32), + p. 179, as a relation between worlds and values of the referent, renders a model the text calls + "extremely sketchy" (p. 178). +* The operator O of (39), p. 148, is `Exhaustification.exh`. +* (61b) and (61c) are read through the quantifiers of (62), which the text calls parallel (p. 159). + +## Errata + +* pp. 63–64 say that (35) enables the inferences that the speaker does not know whether or not `x`. + With three disjuncts they enable only that the speaker does not believe `x`: [believing a disjunct + false stays consistent](##isSecondaryImplicature_Ici) with Quality and the weak implicatures of + (34) and (35), though [not of all disjuncts together](##eq_empty_of_forall_subset_compl_Ici). So + the looseness p. 40 calls immaterial matters here, and "why not infer one of the two?" (p. 41) is + answered only for two. +* p. 64 rejects closing the alternatives under disjunction as repeating the trouble of (32). Under + that closure the weak implicature of *A or B* blocks the strong implicature of (32b), since + Quality would then give belief in *A or B*: [only alternatives false wherever just one disjunct + holds pass](##isSecondaryImplicature_upperSets_iff), and the closure [gives ignorance about every + disjunct](##notMem_polar_Ici_of_mem_primaryImplicatures). (7d), p. 167, is such a disjunctive + alternative, and p. 168 itself blocks its strengthening. +* p. 115 concludes that George "may be American", for British. +* p. 143 paraphrases the negated upper-bounded *like* in (25) as "either we don't like coffee or we + don't love it". [It is *or we love it*](##compl_sdiff_like): the printed form excludes the + continuation *we LOVE it*, and p. 187 has "like but not love". +* p. 149 says that (42b) expresses the "many but not all" reading of (41). The computation on the + same page, p. 150, and [`exh`](##exh_compl_many) give *some but not many*. +* p. 168 cites (9a), but (9) has no parts. +* (11), p. 169, prints the disjunction outside the speaker's belief, where the prose has it inside, + as Competence of the subject, and (16), p. 170, follows it. [Given (10) or (15) the two + coincide](##subset_or_subset_iff), so the derivation stands. +* (46), p. 188, prints *drinking and drinking non-alcoholic beverages*. By (39) the prejacent is + conjoined with the *denial* of the alternative. +* p. 189 overstates in putting the shift of a lower bound "simply out of reach" of O: [O reaches it + given the alternative RICH₁](##exh_rich), the stipulation pp. 188–189 grant elsewhere as "wildly + ad hoc". + +## TODO + +* The presupposition-based implicatures of §8.3, the open alternatives of §6.6 with conditional + perfection, and Spector's route for belief reports (pp. 169–170, [spector-2006]) are not + formalized. +* Separate the consistency check from the innocent exclusion of [fox-2007] at (34) and (35), which + should locate what disjunctive closure adds. +* The experiments of Chapters 4 and 5 belong in `Data/Statistics`. ## References * [geurts-2010] * [geurts-pouscoulous-2009] +* [fox-2007] +* [russell-2006] +* [sauerland-2004] +* [soames-1982] +* [spector-2006] +* [vanrooij-schulz-2004] -/ -public section +@[expose] public section namespace Geurts2010 -open Quantifier Quantifier.Det GeurtsPouscoulous2009 +open Set NeoGricean Question + +variable {W : Type*} {s φ ψ : Set W} + +/-! ### The Standard Recipe -/ + +/-- Soames's Competence⁺ (12), p. 37: the speaker's beliefs agree with the facts at `w`. -/ +def CompetentPlus (w : W) (s ψ : Set W) : Prop := (w ∈ ψ → s ⊆ ψ) ∧ (w ∉ ψ → s ⊆ ψᶜ) + +-- p. 38 +theorem CompetentPlus.mem_polar {w : W} (h : CompetentPlus w s ψ) : s ∈ polar ψ := + Question.mem_polar.2 ((em (w ∈ ψ)).imp h.1 h.2) + +-- p. 38, Travis, who has an opinion on everything regardless of the facts +theorem not_competentPlus_of_subset {w : W} (hs : s.Nonempty) (hw : w ∉ ψ) (h : s ⊆ ψ) : + ¬ CompetentPlus w s ψ := fun hc ↦ + let ⟨_, hv⟩ := hs + hc.2 hw hv (h hv) + +-- the diagram of p. 39: non-belief is disbelief or no opinion, no opinion being non-competence +theorem compl_Iic_eq_union (ψ : Set W) : + (Iic ψ)ᶜ = (Iic ψᶜ \ {∅}) ∪ (polar ψ : Set (Set W))ᶜ := by + rw [← compl_Iic_inter_polar] + ext s + simp only [mem_union, mem_inter_iff, mem_compl_iff, mem_Iic, SetLike.mem_coe, mem_polar] + tauto + +-- p. 40: (16) and (17) exclude each other, so (16) cannot come from strengthening (17) +theorem disjoint_Iic_compl_polar (ψ : Set W) : + Disjoint (Iic ψᶜ) (polar ψ : Set (Set W))ᶜ := + disjoint_left.2 fun _ h hc ↦ hc (mem_polar.2 (.inr h)) + +-- p. 110, footnote 4; p. 167 +theorem inter_nonempty_of_subset_union (hq : s ⊆ φ ∪ ψ) (hψ : ¬ s ⊆ ψ) : (s ∩ φ).Nonempty := + let ⟨_, hw, hwψ⟩ := not_subset.1 hψ + ⟨_, hw, (hq hw).resolve_right hwψ⟩ + +-- p. 41: given Quality, the weak implicatures make Competence fail for a disjunct, when the rest +-- of the disjunction is itself an alternative +theorem notMem_polar_of_subset_union (hq : s ⊆ φ ∪ ψ) (hφ : ¬ s ⊆ φ) (hψ : ¬ s ⊆ ψ) : + s ∉ polar φ := fun h ↦ + (mem_polar.1 h).elim hφ fun hc ↦ + let ⟨_, hw, hwφ⟩ := inter_nonempty_of_subset_union hq hψ + hc hw hwφ + +-- p. 120: what is possible and on which the speaker has an opinion, the speaker believes +theorem subset_of_inter_nonempty_of_mem_polar (hp : (s ∩ ψ).Nonempty) (hc : s ∈ polar ψ) : + s ⊆ ψ := + (mem_polar.1 hc).resolve_right fun h ↦ let ⟨_, hw, hwψ⟩ := hp; h hw hwψ + +-- p. 54: the Horn scale (4) makes (10) an alternative to (9), but (9) entails (10), so that the +-- weak implicature contradicts Quality +theorem Iic_inter_compl_Iic_eq_empty {ι : Type*} [Preorder ι] {E : Set W → Set W} {a : ι → Set W} + {i j : ι} (hE : Antitone E) (ha : Antitone a) (h : i ≤ j) : + Iic (E (a i)) ∩ (Iic (E (a j)))ᶜ = ∅ := + eq_empty_of_forall_notMem fun _ hs ↦ hs.2 (subset_trans hs.1 (hE (ha h))) + +/-! ### Long disjunctions + +The worlds of (29) are ordered by what they make true. A world with `⊥` below it is one in which no +disjunct holds, so the long disjunction (31) is `Ioi ⊥`; the conjunction of the disjuncts below `x` +is `Ici x`, and a world in which just one disjunct holds is an atom. -/ + +section LongDisjunction + +variable {α : Type*} [PartialOrder α] [OrderBot α] {a b c x : α} {t : Set α} + +private theorem notMem_Ici_of_isAtom (hb : IsAtom b) (hx : x ≠ ⊥) (h : x ≠ b) : b ∉ Ici x := + fun hle ↦ h ((hb.le_iff_eq hx).1 hle) + +private theorem Ici_ssubset_Ioi_bot (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) : + Ici a ⊂ Ioi (⊥ : α) := + ⟨fun _ hy ↦ ha.bot_lt.trans_le hy, fun h ↦ notMem_Ici_of_isAtom hb ha.1 hab (h hb.bot_lt)⟩ + +private theorem compl_Iic_ssubset_Ioi_bot (hx : IsAtom x) : (Iic x)ᶜ ⊂ Ioi (⊥ : α) := + ⟨fun _ hy ↦ bot_lt_iff_ne_bot.2 fun he ↦ hy (he ▸ bot_le), fun h ↦ h hx.bot_lt le_rfl⟩ + +-- pp. 63–64: with the alternatives (34) and (35), closed under conjunction only, `K¬A` passes the +-- consistency check once there are three disjuncts, because (35) leaves out the rest of the +-- disjunction +theorem isSecondaryImplicature_Ici (ha : IsAtom a) (hb : IsAtom b) (hc : IsAtom c) (hab : a ≠ b) + (hac : a ≠ c) (hbc : b ≠ c) : + IsSecondaryImplicature (Ioi ⊥) (Ici '' {x | x ≠ ⊥}) (Ici a) := by + refine isSecondaryImplicature_iff.2 ⟨⟨a, ha.1, rfl⟩, Ici_ssubset_Ioi_bot ha hb hab, ?_⟩ + rintro _ ⟨x, hx, rfl⟩ - hsub + have hxb : x = b := (hb.le_iff_eq hx).1 (hsub ⟨hb.bot_lt, notMem_Ici_of_isAtom hb ha.1 hab⟩) + have hxc : x = c := (hc.le_iff_eq hx).1 (hsub ⟨hc.bot_lt, notMem_Ici_of_isAtom hc ha.1 hac⟩) + exact hbc (hxb.symm.trans hxc) + +-- (32), p. 62: over the alternatives of the parse (A ∨ B) ∨ C, the strong implicature of (32b) +-- goes through, which rules out the world in which only C holds +theorem isSecondaryImplicature_parse (ha : IsAtom a) (hb : IsAtom b) (hc : IsAtom c) (hab : a ≠ b) + (hac : a ≠ c) : + IsSecondaryImplicature (Ioi ⊥) + {(Ici a ∪ Ici b) ∩ Ici c, (Ici a ∩ Ici b) ∪ Ici c, Ici a ∩ Ici b ∩ Ici c} + ((Ici a ∩ Ici b) ∪ Ici c) := by + have hb' : a ∉ Ici b := notMem_Ici_of_isAtom ha hb.1 hab.symm + have hc' : a ∉ Ici c := notMem_Ici_of_isAtom ha hc.1 hac.symm + have hψ : a ∉ (Ici a ∩ Ici b) ∪ Ici c := by rintro (h | h); exacts [hb' h.2, hc' h] + refine isSecondaryImplicature_iff.2 ⟨by simp, ⟨?_, fun h ↦ hψ (h ha.bot_lt)⟩, ?_⟩ + · rintro y (h | h) + exacts [ha.bot_lt.trans_le h.1, hc.bot_lt.trans_le h] + · have hsdiff : a ∈ Ioi ⊥ \ ((Ici a ∩ Ici b) ∪ Ici c) := ⟨ha.bot_lt, hψ⟩ + rintro χ (rfl | rfl | rfl) - h + exacts [hc' (h hsdiff).2, hψ (h hsdiff), hc' (h hsdiff).2] + +-- pp. 62–63: the two binary parses each eliminate one column too many +theorem union_sdiff_parse_left (A B C : Set W) : + ((A ∪ B) ∪ C) \ (((A ∪ B) ∩ C) ∪ ((A ∩ B) ∪ C) ∪ (A ∩ B ∩ C)) = + ((A ∪ B) \ (A ∩ B)) \ C := by + ext w + simp only [mem_sdiff, mem_union, mem_inter_iff] + tauto + +theorem union_sdiff_parse_right (A B C : Set W) : + (A ∪ (B ∪ C)) \ ((A ∪ (B ∩ C)) ∪ (A ∩ (B ∪ C)) ∪ (A ∩ (B ∩ C))) = + ((B ∪ C) \ (B ∩ C)) \ A := by + ext w + simp only [mem_sdiff, mem_union, mem_inter_iff] + tauto + +-- contra p. 64: over the closure the text rejects, the weak implicatures give ignorance about every +-- disjunct +theorem notMem_polar_Ici_of_mem_primaryImplicatures (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) + {s : Set α} (hq : s ⊆ Ioi ⊥) (hp : s ∈ primaryImplicatures (Ioi ⊥) {χ | IsUpperSet χ}) : + s ∉ polar (Ici a) := by + have hweak := mem_primaryImplicatures.1 hp + refine fun h ↦ (Question.mem_polar.1 h).elim + (hweak _ (isUpperSet_Ici a) (Ici_ssubset_Ioi_bot ha hb hab)) fun hna ↦ ?_ + exact hweak _ (isLowerSet_Iic a).compl (compl_Iic_ssubset_Ioi_bot ha) fun y hy hya ↦ + hna hy ((ha.le_iff_eq (mem_Ioi.1 (hq hy)).ne').1 hya).ge + +-- an upper set of the worlds of (29) is a union of conjunctions of disjuncts, so that the upper +-- sets are the closure p. 64 considers +theorem eq_iUnion_iInter_of_isUpperSet {κ : Type*} {u : Set (Set κ)} (hu : IsUpperSet u) : + u = ⋃ x ∈ u, ⋂ i ∈ x, Ici ({i} : Set κ) := by + ext w + simp only [mem_iUnion, mem_iInter, mem_Ici, singleton_subset_iff, exists_prop] + exact ⟨fun hw ↦ ⟨w, hw, fun _ h ↦ h⟩, fun ⟨x, hx, h⟩ ↦ hu (fun i hi ↦ h i hi) hx⟩ + +-- p. 61: the only alternative (30) of the substitution method leaves worlds with two disjuncts +example : ({0, 1} : Set (Fin 3)) ∈ Ioi ⊥ \ Ici ⊤ ∧ ¬ IsAtom ({0, 1} : Set (Fin 3)) := by + refine ⟨⟨bot_lt_iff_ne_bot.2 (insert_nonempty _ _).ne_empty, fun h ↦ ?_⟩, fun h ↦ ?_⟩ + · simpa using h (mem_univ (2 : Fin 3)) + · obtain ⟨i, hi⟩ := Set.isAtom_iff.1 h + have h0 : (0 : Fin 3) ∈ ({i} : Set (Fin 3)) := hi ▸ (by simp) + have h1 : (1 : Fin 3) ∈ ({i} : Set (Fin 3)) := hi ▸ (by simp) + exact absurd (subsingleton_singleton h0 h1) (by decide) + +variable [IsAtomic α] + +-- contra p. 64: over alternatives closed under conjunction and disjunction, an alternative passes +-- the consistency check just when it holds in no world in which only one disjunct does +theorem isSecondaryImplicature_upperSets_iff : + IsSecondaryImplicature (Ioi ⊥) {χ | IsUpperSet χ} t ↔ + IsUpperSet t ∧ t ⊂ Ioi ⊥ ∧ ∀ x, IsAtom x → x ∉ t := by + rw [isSecondaryImplicature_iff] + refine and_congr_right fun _ ↦ and_congr_right fun _ ↦ + ⟨fun h x hx hxt ↦ ?_, fun h χ hχ hχφ hsub ↦ ?_⟩ + · exact h _ (isLowerSet_Iic x).compl (compl_Iic_ssubset_Ioi_bot hx) + fun y hy hle ↦ hy.2 ((hx.le_iff_eq (mem_Ioi.1 hy.1).ne').1 hle ▸ hxt) + · obtain ⟨y, hy, hyχ⟩ := not_subset.1 hχφ.2 + obtain ⟨b, hb, hby⟩ := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 hy).ne' + exact hyχ (hχ hby (hsub ⟨hb.bot_lt, h b hb⟩)) + +/-- Closing the alternatives of a long disjunction under conjunction and under disjunction, and +strengthening wherever Competence is consistent, yields exactly the exclusive reading. -/ +theorem Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom : + Ioi ⊥ \ ⋃₀ {t | IsSecondaryImplicature (Ioi ⊥) {χ | IsUpperSet χ} t} = {x : α | IsAtom x} := by + ext x + simp only [mem_sdiff, mem_Ioi, mem_sUnion, mem_ofPred_eq, isSecondaryImplicature_upperSets_iff] + refine ⟨fun ⟨hx, hn⟩ ↦ ?_, fun hx ↦ ⟨hx.bot_lt, fun ⟨t, ⟨_, _, h⟩, hxt⟩ ↦ h x hx hxt⟩⟩ + by_contra hna + obtain ⟨b, hb, hbx⟩ := (eq_bot_or_exists_atom_le x).resolve_left hx.ne' + refine hn ⟨Ici x, ⟨isUpperSet_Ici x, ⟨fun _ hy ↦ hx.trans_le hy, fun h ↦ ?_⟩, fun y hy hxy ↦ ?_⟩, + le_rfl⟩ + · exact hna (le_antisymm hbx (h hb.bot_lt) ▸ hb) + · exact hna ((hy.le_iff_eq hx.ne').1 hxy ▸ hy) + +-- the exclusive state itself meets the weak implicatures of that closure, so the reading is not +-- vacuous +theorem setOf_isAtom_mem_primaryImplicatures : + {x : α | IsAtom x} ∈ primaryImplicatures (Ioi ⊥) {χ | IsUpperSet χ} := + mem_primaryImplicatures.2 fun _ hχ hχφ hsub ↦ + let ⟨y, hy, hyχ⟩ := not_subset.1 hχφ.2 + let ⟨_, hb, hby⟩ := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 hy).ne' + hyχ (hχ hby (hsub hb)) + +-- p. 41: that the speaker cannot believe all the disjuncts false holds at any length +theorem eq_empty_of_forall_subset_compl_Ici {s : Set α} (hq : s ⊆ Ioi ⊥) + (h : ∀ a, IsAtom a → s ⊆ (Ici a)ᶜ) : s = ∅ := + eq_empty_of_forall_notMem fun y hy ↦ + let ⟨_, hb, hby⟩ := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 (hq hy)).ne' + h _ hb hy hby + +example : Ioi ⊥ \ ⋃₀ {t | IsSecondaryImplicature (Ioi ⊥) {χ | IsUpperSet χ} t} = + {w : Set (Fin 3) | ∃ i, w = {i}} := by + rw [Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom] + exact Set.ext fun _ ↦ Set.isAtom_iff + +end LongDisjunction + +/-! ### Intentions first + +Alternatives are sentences (pp. 29, 112), so complexity can be read off them. A speaker's state is +the set of worlds compatible with what the speaker believes, and `may` quantifies over it. -/ + +/-- The sentences of the examples of Chapter 6, over atomic clauses `P`. -/ +inductive Sentence (P : Type*) where + | atom : P → Sentence P + | neg : Sentence P → Sentence P + | or : Sentence P → Sentence P → Sentence P + | and : Sentence P → Sentence P → Sentence P + | may : Sentence P → Sentence P + +namespace Sentence + +variable {P : Type*} {V : P → Set W} {x y a b c u : Sentence P} {p q : P} + +/-- The number of nodes of a sentence, a first approximation to its complexity. -/ +def size : Sentence P → ℕ + | atom _ => 1 + | neg x => x.size + 1 + | or x y | and x y => x.size + y.size + 1 + | may x => x.size + 1 + +/-- The worlds at which a sentence is true, given the valuation of its atomic clauses and the +state `s` that `may` quantifies over. -/ +def eval (V : P → Set W) (s : Set W) : Sentence P → Set W + | atom p => V p + | neg x => (eval V s x)ᶜ + | or x y => eval V s x ∪ eval V s y + | and x y => eval V s x ∩ eval V s y + | may x => {_w | (s ∩ eval V s x).Nonempty} + +/-- $\mathrm{Bel}_S$: a speaker in state `s` believes the sentence. -/ +def Believes (V : P → Set W) (s : Set W) (x : Sentence P) : Prop := s ⊆ x.eval V s + +/-- $\mathrm{Poss}_S$: a speaker in state `s` considers what the sentence says possible. -/ +def Poss (V : P → Set W) (s : Set W) (x : Sentence P) : Prop := (s ∩ x.eval V s).Nonempty + +/-- The sentence `x` entails the sentence `y`. -/ +def Entails (V : P → Set W) (x y : Sentence P) : Prop := ∀ s, x.Believes V s → y.Believes V s + +theorem believes_may (hs : s.Nonempty) : (may x).Believes V s ↔ x.Poss V s := + ⟨fun h ↦ let ⟨_, hw⟩ := hs; h hw, fun h _ _ ↦ h⟩ + +theorem believes_and : (and x y).Believes V s ↔ x.Believes V s ∧ y.Believes V s := + subset_inter_iff + +theorem believes_neg : (neg x).Believes V s ↔ ¬ x.Poss V s := + ⟨fun h ⟨_, hw, hwx⟩ ↦ h hw hwx, fun h w hw hwx ↦ h ⟨w, hw, hwx⟩⟩ + +theorem poss_neg : (neg x).Poss V s ↔ ¬ x.Believes V s := by + simp [Poss, Believes, eval, inter_compl_nonempty_iff] + +theorem not_poss_neg : ¬ (neg x).Poss V s ↔ x.Believes V s := by rw [poss_neg, not_not] + +theorem poss_or : (or x y).Poss V s ↔ x.Poss V s ∨ y.Poss V s := by + simp only [Poss, eval, inter_union_distrib_left, union_nonempty] + +/-- The Standard Recipe's weak implicatures with Quality: the consistent states that believe the +sentence uttered and none of the alternatives `alts`. -/ +def standardRecipe (V : P → Set W) (x : Sentence P) (alts : Set (Sentence P)) : Set (Set W) := + {s | s.Nonempty ∧ x.Believes V s ∧ ∀ a ∈ alts, ¬ a.Believes V s} + +-- on a plain disjunction this is the recipe of `NeoGricean.primaryImplicatures` +theorem mem_standardRecipe_or_iff (hp : V p ⊂ V p ∪ V q) (hq : V q ⊂ V p ∪ V q) : + s ∈ standardRecipe V (or (atom p) (atom q)) {atom p, atom q} ↔ + s.Nonempty ∧ s ∈ Iic (V p ∪ V q) ∩ primaryImplicatures (V p ∪ V q) {V p, V q} := by + simp only [standardRecipe, mem_ofPred_eq, mem_inter_iff, mem_primaryImplicatures] + refine and_congr_right fun _ ↦ and_congr_right fun _ ↦ ?_ + simp only [mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] + exact ⟨fun ⟨h1, h2⟩ ↦ ⟨fun _ ↦ h1, fun _ ↦ h2⟩, fun ⟨h1, h2⟩ ↦ ⟨h1 hp, h2 hq⟩⟩ + +-- (11), steps i–iv of p. 110: for a plain disjunction the Standard Recipe delivers ignorance +theorem poss_of_mem_standardRecipe_or + (hs : s ∈ standardRecipe V (or (atom p) (atom q)) {atom p, atom q}) : + (atom p).Poss V s ∧ (atom q).Poss V s := + ⟨inter_nonempty_of_subset_union hs.2.1 (hs.2.2 (atom q) (by simp)), + inter_nonempty_of_subset_union (fun _ hw ↦ (hs.2.1 hw).symm) (hs.2.2 (atom p) (by simp))⟩ + +/-- Under *may*, the same reasoning leaves the speaker no consistent state at all: the Standard +Recipe's weak implicatures contradict what was said. -/ +theorem standardRecipe_may_or_eq_empty (p q : P) : + standardRecipe V (may (or (atom p) (atom q))) {may (atom p), may (atom q)} = ∅ := by + refine eq_empty_of_forall_notMem fun s ⟨hs, hq, ha⟩ ↦ ?_ + rcases poss_or.1 ((believes_may hs).1 hq) with h | h + · exact ha _ (by simp) ((believes_may hs).2 h) + · exact ha _ (by simp) ((believes_may hs).2 h) + +open Classical in +/-- The sentence a speaker in state `s` could have used to express what the speaker considers +possible, among `x` and `y`: `c` in cell $i_1$, where both are, `a` in $i_2$, where only `x` is, and +`b` in $i_3$, where only `y` is. Cell $i_4$, where neither is, falls with $i_3$; the examples +discard it by Quality or consistency. -/ +noncomputable def say (V : P → Set W) (x y a b c : Sentence P) (s : Set W) : Sentence P := + if x.Poss V s then (if y.Poss V s then c else a) else b + +theorem say_of_poss (hx : x.Poss V s) (hy : y.Poss V s) : say V x y a b c s = c := by + simp [say, hx, hy] + +theorem say_rec {C : Sentence P → Prop} (hc : x.Poss V s → y.Poss V s → C c) + (ha : x.Poss V s → ¬ y.Poss V s → C a) (hb : ¬ x.Poss V s → C b) : + C (say V x y a b c s) := by + unfold say + split_ifs with h h' + exacts [hc h h', ha h h', hb h] + +/-- The alternatives of pp. 115–116: what a consistent speaker of `u` would say is something the +speaker believes and which entails `u`. -/ +def AreAlternatives (V : P → Set W) (u : Sentence P) (say : Set W → Sentence P) : Prop := + ∀ s, s.Nonempty → u.Believes V s → (say s).Believes V s ∧ (say s).Entails V u + +variable {κ : Type*} [Preorder κ] {cost : Sentence P → κ} + +/-- The alternative heuristic (i): the consistent states that believe the sentence uttered and +could not have expressed which cell they are in by a sentence at most as complex. The partition is +the fibres of `say`, and `cost` ranks sentences, lower meaning more available. -/ +def survivors (V : P → Set W) (cost : Sentence P → κ) (u : Sentence P) + (say : Set W → Sentence P) : Set (Set W) := + {s | s.Nonempty ∧ u.Believes V s ∧ ¬ cost (say s) ≤ cost u} + +theorem mem_survivors_say_iff (ha : cost a ≤ cost u) (hb : cost b ≤ cost u) + (hc : ¬ cost c ≤ cost u) : + s ∈ survivors V cost u (say V x y a b c) ↔ + s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ y.Poss V s := by + simp only [survivors, mem_ofPred_eq, say] + split_ifs <;> simp_all + +-- the alternative heuristic (ii), p. 116: where the alternative of cell `i₁` is the hardest to +-- express, the most likely states are those of `i₁` +theorem maximalFor_say_iff {Q : Set W → Prop} (ha : cost a < cost c) (hb : cost b < cost c) + {s₀ : Set W} (h₀ : Q s₀) (hx₀ : x.Poss V s₀) (hy₀ : y.Poss V s₀) : + MaximalFor Q (fun s ↦ cost (say V x y a b c s)) s ↔ Q s ∧ x.Poss V s ∧ y.Poss V s := by + have hle : ∀ t, cost (say V x y a b c t) ≤ cost c := fun _ ↦ + say_rec (C := fun r ↦ cost r ≤ cost c) (fun _ _ ↦ le_rfl) (fun _ _ ↦ ha.le) fun _ ↦ hb.le + refine ⟨fun h ↦ ⟨h.1, ?_⟩, fun ⟨hs, hx, hy⟩ ↦ ⟨hs, fun t _ _ ↦ ?_⟩⟩ + · have hge : cost c ≤ cost (say V x y a b c s) := by + simpa only [say_of_poss hx₀ hy₀] using + h.2 h₀ (by simpa only [say_of_poss hx₀ hy₀] using hle s) + by_contra hn + have hlt : cost (say V x y a b c s) < cost c := + say_rec (C := fun r ↦ cost r < cost c) (fun h1 h2 ↦ absurd ⟨h1, h2⟩ hn) (fun _ _ ↦ ha) + fun _ ↦ hb + exact hlt.not_ge hge + · simpa only [say_of_poss hx hy] using hle t + +/-- The partition of (15) and (20): `c` says that `x` and `y` are possible, on top of `u`. -/ +noncomputable abbrev sayEither (V : P → Set W) (x y a b u : Sentence P) : Set W → Sentence P := + say V x y a b (and (may x) (and (may y) u)) + +theorem mem_survivors_sayEither_iff (ha : a.size ≤ u.size) (hb : b.size ≤ u.size) : + s ∈ survivors V size u (sayEither V x y a b u) ↔ + s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ y.Poss V s := + mem_survivors_say_iff ha hb (by simp only [size]; omega) + +private theorem believes_entails_top (hs : s.Nonempty) (hu : u.Believes V s) (hx : x.Poss V s) + (hy : y.Poss V s) : + (and (may x) (and (may y) u)).Believes V s ∧ (and (may x) (and (may y) u)).Entails V u := + ⟨believes_and.2 ⟨(believes_may hs).2 hx, believes_and.2 ⟨(believes_may hs).2 hy, hu⟩⟩, + fun _ h ↦ (believes_and.1 (believes_and.1 h).2).2⟩ + +/-- (15), p. 115: *George is British or Canadian*, with the alternatives (16). -/ +noncomputable abbrev sayOr (V : P → Set W) (p q : P) : Set W → Sentence P := + sayEither V (atom p) (atom q) (atom p) (atom q) (or (atom p) (atom q)) + +/-- (17), p. 117: *George may be British or Canadian*, with the alternatives (18). -/ +noncomputable abbrev sayMayOr (V : P → Set W) (p q : P) : Set W → Sentence P := + say V (atom p) (atom q) (may (atom p)) (may (atom q)) (and (may (atom p)) (may (atom q))) + +-- p. 115: the speaker of (15) considers both disjuncts possible +theorem mem_survivors_or_iff : + s ∈ survivors V size (or (atom p) (atom q)) (sayOr V p q) ↔ + s.Nonempty ∧ s ⊆ V p ∪ V q ∧ (atom p).Poss V s ∧ (atom q).Poss V s := + mem_survivors_sayEither_iff (by simp [size]) (by simp [size]) + +-- p. 115: (16) are alternatives in the sense of the method +theorem areAlternatives_sayOr : AreAlternatives V (or (atom p) (atom q)) (sayOr V p q) := + fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V (or (atom p) (atom q))) + (believes_entails_top hs h) + (fun _ hq ↦ ⟨fun w hw ↦ (h hw).resolve_right fun hwq ↦ hq ⟨w, hw, hwq⟩, + fun _ h' _ hw ↦ .inl (h' hw)⟩) + fun hp ↦ ⟨fun w hw ↦ (h hw).resolve_left fun hwp ↦ hp ⟨w, hw, hwp⟩, + fun _ h' _ hw ↦ .inr (h' hw)⟩ + +/-- Free choice: of the speakers of *George may be British or Canadian*, those that survive the +alternative heuristic are just the consistent ones that consider each disjunct possible. -/ +theorem mem_survivors_may_or_iff : + s ∈ survivors V size (may (or (atom p) (atom q))) (sayMayOr V p q) ↔ + s.Nonempty ∧ (atom p).Poss V s ∧ (atom q).Poss V s := by + rw [mem_survivors_say_iff (by simp [size]) (by simp [size]) (by simp [size])] + refine ⟨fun ⟨hs, _, h⟩ ↦ ⟨hs, h⟩, fun ⟨hs, hp, hq⟩ ↦ ⟨hs, ?_, hp, hq⟩⟩ + exact (believes_may hs).2 (poss_or.2 (.inl hp)) -theorem exactlyTwo_not_scopeUp : ¬ ScopeMonotone (Quant.exactlyTwo.sem : Det (Fin 3)) := by - intro h - have key : Quant.exactlyTwo.sem (Set.univ : Set (Fin 3)) {s | s = 0 ∨ s = 1} → - Quant.exactlyTwo.sem (Set.univ : Set (Fin 3)) Set.univ := - h Set.univ (Set.subset_univ _) - simp only [Quant.sem] at key - revert key +-- p. 117: (18) are alternatives in the sense of the method +theorem areAlternatives_sayMayOr : + AreAlternatives V (may (or (atom p) (atom q))) (sayMayOr V p q) := fun s hs h ↦ by + have key {r : P} (hr : V r ⊆ V p ∪ V q) : (may (atom r)).Entails V (may (or (atom p) (atom q))) := + fun _ h' _ hw ↦ (h' hw).mono (inter_subset_inter_right _ hr) + refine say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V (may (or (atom p) (atom q)))) + (fun hp hq ↦ ⟨believes_and.2 ⟨(believes_may hs).2 hp, (believes_may hs).2 hq⟩, + fun t h' ↦ key subset_union_left t (believes_and.1 h').1⟩) + (fun hp _ ↦ ⟨(believes_may hs).2 hp, key subset_union_left⟩) fun hp ↦ ?_ + rcases poss_or.1 ((believes_may hs).1 h) with h' | h' + · exact absurd h' hp + · exact ⟨(believes_may hs).2 h', key subset_union_right⟩ + +-- p. 118: the survivors believe the very alternative the Standard Recipe has them not believe +theorem believes_of_mem_survivors_may_or + (h : s ∈ survivors V size (may (or (atom p) (atom q))) (sayMayOr V p q)) : + (may (atom p)).Believes V s ∧ (may (atom q)).Believes V s := + have ⟨hs, hp, hq⟩ := mem_survivors_may_or_iff.1 h + ⟨(believes_may hs).2 hp, (believes_may hs).2 hq⟩ + +-- p. 117 applies the heuristic (ii) to (17), and p. 119 reasons by (i) for (19): both single out +-- `i₁` +theorem maximalFor_sayMayOr_iff (hp : (V p).Nonempty) (hq : (V q).Nonempty) : + MaximalFor (fun s : Set W ↦ s.Nonempty ∧ (may (or (atom p) (atom q))).Believes V s) + (fun s ↦ (sayMayOr V p q s).size) s ↔ + (s.Nonempty ∧ (may (or (atom p) (atom q))).Believes V s) ∧ + (atom p).Poss V s ∧ (atom q).Poss V s := by + obtain ⟨w, hw⟩ := hp + obtain ⟨v, hv⟩ := hq + exact maximalFor_say_iff (by simp [size]) (by simp [size]) (s₀ := V p ∪ V q) + ⟨⟨w, .inl hw⟩, fun _ _ ↦ ⟨w, .inl hw, .inl hw⟩⟩ ⟨w, .inl hw, hw⟩ ⟨v, .inr hv, hv⟩ + +-- pp. 119–120: free choice reports, where `V` gives the restaurant's permissions: with Competence +-- for each proposition at issue the weak inferences become beliefs +theorem subset_of_mem_survivors_or + (h : s ∈ survivors V size (or (atom p) (atom q)) (sayOr V p q)) (hp : s ∈ polar (V p)) + (hq : s ∈ polar (V q)) : s ⊆ V p ∧ s ⊆ V q := + have ⟨_, _, hpp, hpq⟩ := mem_survivors_or_iff.1 h + ⟨subset_of_inter_nonempty_of_mem_polar hpp hp, subset_of_inter_nonempty_of_mem_polar hpq hq⟩ + +/-- (13), p. 112: *many of the nurses were drunk*, with the alternatives (14), p. 113: `x` in the +cell of believing `x`, `u` and not `x` in that of believing its negation, and `u` and maybe `x` in +that of no opinion. The three-way partition of p. 113 is the partition by what is possible, among +`x` and its negation, since only the inconsistent state considers neither possible. The last two +alternatives have the same size, as p. 122 says of (22). -/ +noncomputable abbrev sayScalar (V : P → Set W) (u x : Sentence P) : Set W → Sentence P := + say V x (neg x) x (and u (neg x)) (and u (may x)) + +/-- The alternative heuristic is sensitive to form: a speaker's saying `u` rules out that the +speaker believes `x` just when `x` is no more complex than `u`. -/ +theorem mem_survivors_scalar_iff : + s ∈ survivors V size u (sayScalar V u x) ↔ + s.Nonempty ∧ u.Believes V s ∧ (x.size ≤ u.size → ¬ x.Believes V s) := by + simp only [survivors, mem_ofPred_eq, say] + refine and_congr_right fun hs ↦ and_congr_right fun _ ↦ ?_ + rw [← not_poss_neg] + by_cases hp : x.Poss V s <;> by_cases hn : (neg x).Poss V s + · simp [hp, hn, size] + · simp [hp, hn] + · simp [hp, hn, size] + · rw [not_poss_neg] at hn + exact absurd (let ⟨w, hw⟩ := hs; ⟨w, hw, hn hw⟩) hp + +-- p. 113: (14) are alternatives in the sense of the method +theorem areAlternatives_sayScalar (hx : x.Entails V u) : AreAlternatives V u (sayScalar V u x) := + fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V u) + (fun hp _ ↦ ⟨believes_and.2 ⟨h, (believes_may hs).2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩) + (fun _ hn ↦ ⟨not_poss_neg.1 hn, hx⟩) + fun hp ↦ ⟨believes_and.2 ⟨h, believes_neg.2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩ + +-- p. 114: Competence eliminates the cell of no opinion, which leaves the strong implicature +theorem subset_compl_of_mem_survivors_scalar + (h : s ∈ survivors V size (atom p) (sayScalar V (atom p) (atom q))) (hc : s ∈ polar (V q)) : + s ⊆ (V q)ᶜ := + (Question.mem_polar.1 hc).resolve_left ((mem_survivors_scalar_iff.1 h).2.2 le_rfl) + +-- (23), p. 122: with *many though not all* in the discourse, previous use lowers that alternative, +-- the state of believing *not all* goes too, and no opinion is left +theorem mem_survivors_indicator_iff (hx : x.size ≤ u.size) : + s ∈ survivors V (({and u (neg x)}ᶜ : Set (Sentence P)).indicator size) u (sayScalar V u x) ↔ + s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ (neg x).Poss V s := by + have hu : u ∈ ({and u (neg x)}ᶜ : Set (Sentence P)) := fun h ↦ by + have := congrArg size (mem_singleton_iff.1 h) + simp only [size] at this + omega + have hc : and u (may x) ∈ ({and u (neg x)}ᶜ : Set (Sentence P)) := fun h ↦ by + simpa using mem_singleton_iff.1 h + refine mem_survivors_say_iff ?_ ?_ ?_ + · rw [indicator_of_mem hu] + by_cases h : x ∈ ({and u (neg x)}ᶜ : Set (Sentence P)) + · rwa [indicator_of_mem h] + · simp [indicator_of_notMem h] + · simp [indicator_of_notMem] + · rw [indicator_of_mem hu, indicator_of_mem hc] + simp only [size] + omega + +end Sentence + +open Sentence + +section Pizza + +variable {D : Type*} + +/-- The clauses of (20), *many people had pizza or pasta*, and of its alternatives. -/ +inductive PizzaClause where + | manyEither | manyPizza | manyPasta | somePizza | somePasta + +/-- The worlds at which a clause of (20) holds, where `pizza w` and `pasta w` are those who had +pizza and pasta at `w`. -/ +def PizzaClause.val (many : Set D → Prop) (pizza pasta : W → Set D) : PizzaClause → Set W + | manyEither => {w | many (pizza w ∪ pasta w)} + | manyPizza => {w | many (pizza w)} + | manyPasta => {w | many (pasta w)} + | somePizza => {w | (pizza w).Nonempty} + | somePasta => {w | (pasta w).Nonempty} + +variable {many : Set D → Prop} {pizza pasta : W → Set D} + +local notation "V₂₀" => PizzaClause.val many pizza pasta + +/-- Alternatives to (20), reconstructed after (18) for the partition of p. 120 by *some people had +pizza* and *some people had pasta*. -/ +noncomputable abbrev sayMany (many : Set D → Prop) (pizza pasta : W → Set D) : + Set W → Sentence PizzaClause := + sayEither (PizzaClause.val many pizza pasta) (atom .somePizza) (atom .somePasta) (atom .manyPizza) + (atom .manyPasta) (atom .manyEither) + +-- (20), p. 120: free choice with no modal +theorem mem_survivors_many_iff : + s ∈ survivors V₂₀ size (atom .manyEither) (sayMany many pizza pasta) ↔ + s.Nonempty ∧ (atom .manyEither).Believes V₂₀ s ∧ (atom .somePizza).Poss V₂₀ s ∧ + (atom .somePasta).Poss V₂₀ s := + mem_survivors_sayEither_iff le_rfl le_rfl + +theorem areAlternatives_sayMany (hm : Monotone many) : + AreAlternatives V₂₀ (atom .manyEither) (sayMany many pizza pasta) := fun s hs h ↦ + say_rec (C := fun r ↦ r.Believes V₂₀ s ∧ r.Entails V₂₀ (atom .manyEither)) + (believes_entails_top hs h) + (fun _ hn ↦ ⟨fun w hw ↦ by + have he : pasta w = ∅ := not_nonempty_iff_eq_empty.1 fun hw' ↦ hn ⟨w, hw, hw'⟩ + simpa [eval, PizzaClause.val, he] using h hw, fun _ h' _ hw ↦ hm subset_union_left (h' hw)⟩) + fun hn ↦ ⟨fun w hw ↦ by + have he : pizza w = ∅ := not_nonempty_iff_eq_empty.1 fun hw' ↦ hn ⟨w, hw, hw'⟩ + simpa [eval, PizzaClause.val, he] using h hw, fun _ h' _ hw ↦ hm subset_union_right (h' hw)⟩ + +end Pizza + +-- (31), p. 61, with p. 115: a speaker who rules out a disjunct could have used the shorter +-- disjunction, so that the survivors of the heuristic consider every disjunct possible, at any +-- length +theorem inter_nonempty_of_forall_not_subset {ι : Type*} {A : ι → Set W} {J : Finset ι} {i : ι} + (hq : s ⊆ ⋃ j ∈ J, A j) (h : ∀ J' ⊂ J, ¬ s ⊆ ⋃ j ∈ J', A j) (hi : i ∈ J) : + (s ∩ A i).Nonempty := by + classical + by_contra hne + refine h _ (Finset.erase_ssubset hi) fun w hw ↦ ?_ + obtain ⟨j, hj, hwj⟩ := mem_iUnion₂.1 (hq hw) + exact mem_iUnion₂.2 ⟨j, Finset.mem_erase.2 ⟨fun he ↦ hne ⟨w, hw, he ▸ hwj⟩, hj⟩, hwj⟩ + +/-! ### Conventionalism -/ + +section Conventionalism + +open Quantifier Quantifier.Det GeurtsPouscoulous2009 Exhaustification + +private theorem someNotAllC_subset (R : Situation) : someNotAllC R ⊆ someC R := fun _ h ↦ h.1 + +/-- Enhanced lexicalism in its weak version (33) prefers the upper-bounded reading of (62) provided +this strengthens the sentence, which holds just under the upward-entailing quantifiers. -/ +theorem boundedReading_ssubset_iff (q : Quant) : + localReading q ⊂ classicalReading q ↔ PredictsLocalSIWeak (q.sem : Det (Fin 3)) := by + have pos {r : Quant} {t : Trial} (hr : PredictsLocalSIWeak (r.sem : Det (Fin 3))) + (hc : Classical r t) (hl : ¬ Local r t) : + (localReading r ⊂ classicalReading r) ↔ PredictsLocalSIWeak (r.sem : Det (Fin 3)) := + iff_of_true ⟨fun R hR ↦ hr univ (someNotAllC_subset R) hR, fun h ↦ hl (h hc)⟩ hr + have neg {r : Quant} {t : Trial} (hr : ¬ PredictsLocalSIWeak (r.sem : Det (Fin 3))) + (hc : ¬ Classical r t) (hl : Local r t) : + (localReading r ⊂ classicalReading r) ↔ PredictsLocalSIWeak (r.sem : Det (Fin 3)) := + iff_of_false (fun h ↦ hc (h.1 hl)) hr + cases q with + | all => exact pos all_predictsLocalSIWeak classical_all not_local_all + | moreThanOne => + exact pos moreThanOne_predictsLocalSIWeak classical_moreThanOne not_local_moreThanOne + | exactlyTwo => + exact neg exactlyTwo_not_predictsLocalSIWeak not_classical_exactlyTwo_b local_exactlyTwo_b + | notAll => exact neg notAll_not_predictsLocalSIWeak not_classical_notAll local_notAll + | notMoreThanOne => + exact neg notMoreThanOne_not_predictsLocalSIWeak not_classical_notMoreThanOne + local_notMoreThanOne + +-- (32), pp. 146–147: the strong version prefers it unless this weakens the sentence, which also +-- covers the non-monotone *exactly two* +theorem not_classicalReading_ssubset_iff (q : Quant) : + ¬ classicalReading q ⊂ localReading q ↔ PredictsLocalSI (q.sem : Det (Fin 3)) := by + have anti {r : Quant} (hr : ¬ PredictsLocalSI (r.sem : Det (Fin 3))) {t : Trial} + (hc : ¬ Classical r t) (hl : Local r t) : + (¬ classicalReading r ⊂ localReading r) ↔ PredictsLocalSI (r.sem : Det (Fin 3)) := + iff_of_false (not_not.2 ⟨fun R hR ↦ not_not.1 hr univ (someNotAllC_subset R) hR, + fun h' ↦ hc (h' hl)⟩) hr + cases q with + | all => + exact iff_of_true ((boundedReading_ssubset_iff .all).2 all_predictsLocalSIWeak).not_gt + all_predictsLocalSI + | moreThanOne => + exact iff_of_true + ((boundedReading_ssubset_iff .moreThanOne).2 moreThanOne_predictsLocalSIWeak).not_gt + moreThanOne_predictsLocalSI + | exactlyTwo => + exact iff_of_true (fun h ↦ not_local_exactlyTwo_a (h.1 classical_exactlyTwo_a)) + exactlyTwo_predictsLocalSI + | notAll => exact anti notAll_not_predictsLocalSI not_classical_notAll local_notAll + | notMoreThanOne => + exact anti notMoreThanOne_not_predictsLocalSI not_classical_notMoreThanOne + local_notMoreThanOne + +-- p. 159: of the squares of Figure 1, one is connected to all the circles +theorem existsUnique_figure2 : ∃! s : Fin 3, ∀ c, figure2 s c := + ⟨0, fun _ ↦ .inl rfl, by decide⟩ + +variable {some many all : Set W} + +-- (39)–(40): `exh` is the operator O of (39); O (44b), the parse under negation (42c) +theorem exh_many (hs : many ⊆ some) (ha : all ⊂ many) : + exh {some, many, all} many = many \ all := + exh_eq_sdiff_of_forall (by simp) ha.2 (by + rintro r (rfl | rfl | rfl) + exacts [.inl hs, .inl subset_rfl, .inr subset_rfl]) + +-- (43): O (43b), the parse (42b) +theorem exh_compl_many (hs : many ⊂ some) (ha : all ⊆ many) : + exh {someᶜ, manyᶜ, allᶜ} manyᶜ = manyᶜ ∩ some := by + rw [exh_eq_sdiff_of_forall (q := someᶜ) (by simp) (fun h ↦ hs.2 (compl_subset_compl.1 h)) (by + rintro r (rfl | rfl | rfl) + exacts [.inr subset_rfl, .inl subset_rfl, .inl (compl_subset_compl.2 ha)]), sdiff_compl] + +-- (47), p. 150: the Power Principle prefers (42b) to the readings (42a) and (42c) +theorem isLeast_readings_negation (hs : many ⊂ some) (ha : all ⊂ many) : + IsLeast {manyᶜ, exh {someᶜ, manyᶜ, allᶜ} manyᶜ, (exh {some, many, all} many)ᶜ} + (exh {someᶜ, manyᶜ, allᶜ} manyᶜ) := by + rw [exh_compl_many hs ha.1, exh_many hs.1 ha] + refine ⟨by simp, ?_⟩ + rintro _ (rfl | rfl | rfl) + · exact inter_subset_left + · exact subset_rfl + · exact fun w hw hn ↦ hw.1 hn.1 + +-- (57), pp. 156–157: the Power Principle prefers the narrow-scope parse (57b) of (56b), which +-- yields the inference the text says does not go through. That it is the stronger needs a serial +-- relation, which the text leaves tacit +theorem isLeast_readings_core (R : SetRel W W) [ModalLogic.IsSerial R] (ha : all ⊂ some) : + IsLeast {R.core some, exh {R.core some, R.core all} (R.core some), + R.core (exh {some, all} some)} (R.core (exh {some, all} some)) := by + have hsome : exh {some, all} some = some \ all := + exh_eq_sdiff_of_forall (by simp) ha.2 (by + rintro r (rfl | rfl) + exacts [.inl subset_rfl, .inr subset_rfl]) + have hcore : R.core (some \ all) ⊆ R.core some := fun _ hw _ hv ↦ (hw hv).1 + rw [hsome] + refine ⟨by simp, ?_⟩ + rintro _ (rfl | rfl | rfl) + · exact hcore + · refine fun w hw ↦ ⟨hcore hw, ?_⟩ + rintro q (rfl | rfl) hwq + · exact subset_rfl + · obtain ⟨v, hv⟩ := ModalLogic.IsSerial.serial (R := R) w + exact absurd (hwq hv) (hw hv).2 + · exact subset_rfl + +-- (25), p. 143: the negated upper-bounded *like* is *don't like or love*, not the printed *don't +-- like or don't love*, which excludes the continuation *we LOVE it* +theorem compl_sdiff_like {like love : Set W} (h : love ⊆ like) : + (like \ love)ᶜ = likeᶜ ∪ love ∧ Disjoint (likeᶜ ∪ loveᶜ) love := by + refine ⟨by ext w; simp only [mem_compl_iff, mem_sdiff, mem_union]; tauto, ?_⟩ + exact disjoint_left.2 fun _ hw hl ↦ hw.elim (· (h hl)) (· hl) + +-- (48)–(49), p. 189: O can shift a lower bound too, given the alternative RICH₁ +theorem exh_rich {rich rich₂ : Set W} (h : rich₂ ⊆ rich) (hne : rich₂.Nonempty) : + exh {rich \ rich₂} rich = rich₂ := by + obtain ⟨v, hv⟩ := hne + rw [exh_eq_sdiff_of_forall (mem_singleton _) (fun hs ↦ (hs (h hv)).2 hv) + (by rintro r rfl; exact .inr subset_rfl), sdiff_sdiff_eq_self h] + +end Conventionalism + +/-! ### Embedded implicatures -/ + +section Embedded + +variable {M A F : Set W} + +-- §8.1, (6)–(8): the implicature *not all the figs* passes the consistency check +theorem isSecondaryImplicature_mango (hA : A ⊆ F) (hM : (M \ F).Nonempty) + (hF : (F \ (M ∪ A)).Nonempty) : IsSecondaryImplicature (M ∪ F) {M, F, A, M ∪ A} A := by + obtain ⟨f, hf, hfn⟩ := hF + obtain ⟨m, hm, hmn⟩ := hM + simp only [mem_union, not_or] at hfn + have hfd : f ∈ (M ∪ F) \ A := ⟨.inr hf, hfn.2⟩ + have hmd : m ∈ (M ∪ F) \ A := ⟨.inl hm, fun h ↦ hmn (hA h)⟩ + refine isSecondaryImplicature_iff.2 + ⟨by simp, ⟨fun _ hw ↦ .inr (hA hw), fun h ↦ hfn.2 (h hfd.1)⟩, ?_⟩ + rintro χ (rfl | rfl | rfl | rfl) - h + · exact hfn.1 (h hfd) + · exact hmn (h hmd) + · exact hfn.2 (h hfd) + · exact (h hfd).elim hfn.1 hfn.2 + +-- §8.1: Competence fails for (7a), (7b) and (7d), so no strong implicature that Cleo had no mango +theorem isSecondaryImplicature_mango_iff (hA : A ⊆ F) (hM : (M \ F).Nonempty) + (hF : (F \ (M ∪ A)).Nonempty) {χ : Set W} (hχ : χ ∈ ({M, F, A, M ∪ A} : Set (Set W))) : + IsSecondaryImplicature (M ∪ F) {M, F, A, M ∪ A} χ ↔ χ = A := by + have hFφ : F ⊂ M ∪ F := ⟨subset_union_right, fun h ↦ + let ⟨_, hw, hwF⟩ := hM; hwF (h (.inl hw))⟩ + have hMφ : M ⊂ M ∪ F := ⟨subset_union_left, fun h ↦ + let ⟨_, hw, hn⟩ := hF; hn (.inl (h (.inr hw)))⟩ + refine ⟨fun h ↦ ?_, fun h ↦ by subst h; exact isSecondaryImplicature_mango hA hM hF⟩ + have hb := (isSecondaryImplicature_iff.1 h).2.2 + rcases hχ with rfl | rfl | rfl | rfl + · exact absurd (fun w hw ↦ hw.1.resolve_left hw.2) (hb _ (by simp) hFφ) + · exact absurd (fun w hw ↦ hw.1.resolve_right hw.2) (hb _ (by simp) hMφ) + · rfl + · exact absurd (fun w hw ↦ hw.1.resolve_left fun hwM ↦ hw.2 (.inl hwM)) (hb _ (by simp) hFφ) + +open GeurtsPouscoulous2009 in +-- §8.2, (10)–(12), pp. 168–169, after [vanrooij-schulz-2004] and [russell-2006]: the reading of (9) +-- that looks local, from the strong implicature at the speaker and Competence of the subject +theorem subset_core_sdiff {R : SetRel W W} {some all : Set W} (hall : all ⊂ some) + (hq : s ⊆ R.core some) (h10 : s ⊆ (R.core all)ᶜ) (h11 : s ⊆ R.core all ∪ R.core allᶜ) : + s ⊆ R.core (some \ all) := + so_pair hall ▸ fun _ hw ↦ local_of_global_of_opinionated R hall (hq hw) (h10 hw) (h11 hw) + +-- (10)–(12) and, for *hope*, (15)–(17), pp. 170–171, share this form, for any attitude: what +-- separates them is the plausibility of the second premise. (11) and (16), as printed, have the +-- disjunction outside the speaker's belief; given the first premise that says the same, and without +-- it it is strictly stronger +theorem subset_or_subset_iff {X Y : Set W} (h10 : s ⊆ Xᶜ) : (s ⊆ X ∨ s ⊆ Y) ↔ s ⊆ X ∪ Y := + ⟨fun h ↦ h.elim (·.trans subset_union_left) (·.trans subset_union_right), + fun h ↦ .inr fun _ hw ↦ (h hw).resolve_left (h10 hw)⟩ + +example : ∃ (s X Y : Set (Fin 2)), s ⊆ X ∪ Y ∧ ¬ (s ⊆ X ∨ s ⊆ Y) := + ⟨univ, {0}, {0}ᶜ, (union_compl_self _).ge, by + rintro (h | h) + · exact absurd (h (mem_univ 1)) (by simp) + · exact h (mem_univ 0) rfl⟩ + +section Indefinites + +variable {D : Type*} {sailor some all : W → Set D} {t : SetRel W D} + +-- (32)–(35), pp. 179–180: the state of (32) is a relation between worlds and values of the +-- discourse referent, which the hearer's question is about, and the Standard Recipe runs as usual: +-- (34) with Competence about the referent gives the model (35) +theorem subset_inter_compl_ofSuccessors + (h32 : t ⊆ SetRel.ofSuccessors sailor ∩ SetRel.ofSuccessors some) + (h34 : ¬ t ⊆ SetRel.ofSuccessors all) (hc : t ∈ polar (SetRel.ofSuccessors all)) : + t ⊆ SetRel.ofSuccessors sailor ∩ SetRel.ofSuccessors some ∩ (SetRel.ofSuccessors all)ᶜ := + subset_inter h32 ((Question.mem_polar.1 hc).resolve_left h34) + +-- p. 139: that (14) is false, given (32), entails (35), so that the alternative-based inference is +-- the stronger +theorem subset_compl_ofSuccessors (h32 : t ⊆ SetRel.ofSuccessors sailor) + (h14 : t ⊆ Prod.fst ⁻¹' (SetRel.ofSuccessors (sailor ⊓ all)).dom ᶜ) : + t ⊆ (SetRel.ofSuccessors all)ᶜ := + fun p hp hall ↦ h14 hp ⟨p.2, h32 hp, hall⟩ + +end Indefinites + +end Embedded + +/-! ### The judgments -/ + +section Rows + +open GeurtsPouscoulous2009 + +/-- The Horn set of Table 2, in order of increasing strength. -/ +def quantifierTable : List (String × Fin 4) := [("some", 0), ("many", 1), ("most", 2), ("all", 3)] + +/-- A row of Table 2: the polarity of the frame, the quantifier filling it and the predicted +alternatives. -/ +structure Table2Row where + polarity : Polarity + quantifier : Fin 4 + alternatives : List (Fin 4) + deriving DecidableEq + +/-- Reads a row of Table 2. -/ +def Table2Row.ofDatum (ex : Datum) : Option Table2Row := do + let polarity ← ex.parse? "negated" [("false", Polarity.positive), ("true", .negative)] + let quantifier ← ex.parse? "quantifier" quantifierTable + pure ⟨polarity, quantifier, (ex.features "alternative").filterMap (List.lookup · quantifierTable)⟩ + +example : Datum.ReadCount Table2Row.ofDatum Examples.all 8 := by decide + +-- Table 2: the alternatives printed are those of the definition (24) by Horn sets, on which a +-- sentence is an alternative iff it is stronger, for any strictly stronger meanings of the four +-- quantifiers. The reversal under negation is among sentences; the meanings keep their order, and +-- the ordering a Horn scale (4) would impose plays no part (pp. 57–59) +theorem rows_table2 {a : Fin 4 → Set W} (ha : StrictAnti a) : + ∀ r ∈ Examples.all.filterMap Table2Row.ofDatum, ∀ k, + k ∈ r.alternatives ↔ r.polarity • a k ⊂ r.polarity • a r.quantifier := by + have key : ∀ r ∈ Examples.all.filterMap Table2Row.ofDatum, ∀ k, k ∈ r.alternatives ↔ + if r.polarity = .positive then r.quantifier < k else k < r.quantifier := by decide + intro r hr k + rw [key r hr k] + rcases r.polarity with _ | _ + · simpa using ha.lt_iff_gt.symm + · simpa using (compl_lt_compl_iff_lt.trans ha.lt_iff_gt).symm + +/-- The inferences of the rows that a Gricean derivation bears on, which the text says are conveyed +or not. -/ +inductive Item where + | disjunct | freeChoice | sameLength | afterUse | longer | figs | mango | referent | everySailor + deriving DecidableEq + +/-- The statement that the theory derives the inference, over any model of the sentence. -/ +def Item.Derived : Item → Prop + | .disjunct => ∀ {W : Type} (V : Bool → Set W) (s : Set W), + s ∈ survivors V size (or (atom true) (atom false)) (sayOr V true false) → + (atom true).Poss V s ∧ (atom false).Poss V s + | .freeChoice => ∀ {W : Type} (V : Bool → Set W) (s : Set W), + s ∈ survivors V size (may (or (atom true) (atom false))) (sayMayOr V true false) → + (atom true).Poss V s ∧ (atom false).Poss V s + | .sameLength => ∀ {W : Type} (V : Bool → Set W) (s : Set W), + s ∈ survivors V size (atom true) (sayScalar V (atom true) (atom false)) → + ¬ (atom false).Believes V s + | .afterUse => ∀ {W : Type} (V : Bool → Set W) (s : Set W), + s ∈ survivors V (({and (atom true) (neg (atom false))}ᶜ : Set (Sentence Bool)).indicator size) + (atom true) (sayScalar V (atom true) (atom false)) → + ¬ (atom false).Believes V s ∧ (atom false).Poss V s + | .longer => ∀ {W : Type} (V : Bool → Set W) (s : Set W), + s ∈ survivors V size (atom true) (sayScalar V (atom true) (and (atom false) (atom true))) → + ¬ (and (atom false) (atom true)).Believes V s + | .figs => ∀ {W : Type} (M F A : Set W), A ⊆ F → (M \ F).Nonempty → (F \ (M ∪ A)).Nonempty → + IsSecondaryImplicature (M ∪ F) {M, F, A, M ∪ A} A + | .mango => ∀ {W : Type} (M F A : Set W), A ⊆ F → (M \ F).Nonempty → (F \ (M ∪ A)).Nonempty → + IsSecondaryImplicature (M ∪ F) {M, F, A, M ∪ A} M + | .referent => ∀ {W D : Type} (sailor some all : W → Set D) (t : SetRel W D), + t ⊆ SetRel.ofSuccessors sailor ∩ SetRel.ofSuccessors some → ¬ t ⊆ SetRel.ofSuccessors all → + t ∈ polar (SetRel.ofSuccessors all) → t ⊆ (SetRel.ofSuccessors all)ᶜ + | .everySailor => ∀ {W D : Type} (sailor all : W → Set D) (t : SetRel W D), + t ⊆ SetRel.ofSuccessors sailor → t ⊆ (SetRel.ofSuccessors all)ᶜ → + t ⊆ Prod.fst ⁻¹' (SetRel.ofSuccessors (sailor ⊓ all)).dom ᶜ + +-- (26b), p. 124: *big toe* is longer than *toe*, so that nothing rules out believing it +theorem Item.not_derived_longer : ¬ Item.longer.Derived := fun h ↦ + @h Unit (fun _ ↦ univ) univ + (mem_survivors_scalar_iff.2 ⟨univ_nonempty, fun _ _ ↦ mem_univ _, by simp [size]⟩) + fun _ _ ↦ ⟨mem_univ _, mem_univ _⟩ + +-- (3), p. 165: Competence is not consistent for the first disjunct +theorem Item.not_derived_mango : ¬ Item.mango.Derived := fun h ↦ by + have hA : ({2} : Set (Fin 3)) ⊆ {1, 2} := by simp + have hM : (({0} : Set (Fin 3)) \ {1, 2}).Nonempty := ⟨0, by simp⟩ + have hF : (({1, 2} : Set (Fin 3)) \ ({0} ∪ {2})).Nonempty := ⟨1, by simp⟩ + have := (isSecondaryImplicature_mango_iff hA hM hF (by simp)).1 + (@h (Fin 3) {0} {1, 2} {2} hA hM hF) + exact absurd (mem_singleton_iff.1 (this ▸ mem_singleton (0 : Fin 3))) (by decide) + +-- pp. 139, 180: (35) does not entail that (14) is false, so that the story need not be about every +-- sailor +theorem Item.not_derived_everySailor : ¬ Item.everySailor.Derived := fun h ↦ by + have := @h Unit Bool (fun _ ↦ univ) (fun _ ↦ {true}) {((), false)} + (fun _ _ ↦ mem_univ _) (by rintro _ rfl hb; simp [SetRel.ofSuccessors] at hb) + exact this rfl ⟨true, mem_univ _, rfl⟩ + +theorem Item.derived_iff : ∀ i : Item, i.Derived ↔ i ∉ [Item.longer, .mango, .everySailor] + | .disjunct => iff_of_true (fun _ _ h ↦ (mem_survivors_or_iff.1 h).2.2) (by decide) + | .freeChoice => iff_of_true (fun _ _ h ↦ (mem_survivors_may_or_iff.1 h).2) (by decide) + | .sameLength => iff_of_true (fun _ _ h ↦ (mem_survivors_scalar_iff.1 h).2.2 le_rfl) (by decide) + | .afterUse => iff_of_true (fun _ _ h ↦ by + obtain ⟨_, _, hp, hn⟩ := + (mem_survivors_indicator_iff (x := atom false) (u := atom true) le_rfl).1 h + exact ⟨poss_neg.1 hn, hp⟩) (by decide) + | .longer => iff_of_false Item.not_derived_longer (by decide) + | .figs => iff_of_true (fun _ _ _ ↦ isSecondaryImplicature_mango) (by decide) + | .mango => iff_of_false Item.not_derived_mango (by decide) + | .referent => iff_of_true (fun _ _ _ _ h32 h34 hc ↦ + (subset_inter_compl_ofSuccessors h32 h34 hc).trans inter_subset_right) (by decide) + | .everySailor => iff_of_false Item.not_derived_everySailor (by decide) + +/-- Reads the item of a row and whether the text says the inference is conveyed. -/ +def inference? (ex : Datum) : Option (Item × Bool) := do + let item ← ex.parse? "item" [("disjunct", Item.disjunct), ("freeChoice", .freeChoice), + ("sameLength", .sameLength), ("afterUse", .afterUse), ("longer", .longer), ("figs", .figs), + ("mango", .mango), ("referent", .referent), ("everySailor", .everySailor)] + let conveys ← ex.bool? "conveys" + pure (item, conveys) + +example : Datum.ReadCount inference? Examples.all 11 := by decide + +-- the rows on which a derivation bears: the theory derives what the text says is conveyed +theorem rows_conveys : ∀ r ∈ Examples.all.filterMap inference?, (r.2 = true ↔ r.1.Derived) := by + simp only [Item.derived_iff] decide -theorem notAll_not_scopeUp : ¬ ScopeMonotone (Quant.notAll.sem : Det (Fin 3)) := fun h ↦ - h Set.univ (Set.empty_subset Set.univ) (fun hall ↦ hall (Set.mem_univ 0)) subset_rfl - -/-- Every conventionalist theory predicts the local reading under *all* and *more than one*, but -only the stronger ones under *exactly two* (Section 7.3, (62)). -/ -theorem conventionalist_predictions : - PredictsLocalSIWeak (Quant.all.sem : Det (Fin 3)) ∧ - PredictsLocalSIWeak (Quant.moreThanOne.sem : Det (Fin 3)) ∧ - ¬ PredictsLocalSIWeak (Quant.exactlyTwo.sem : Det (Fin 3)) ∧ - PredictsLocalSI (Quant.exactlyTwo.sem : Det (Fin 3)) := - ⟨all_predictsLocalSIWeak, moreThanOne_predictsLocalSIWeak, exactlyTwo_not_scopeUp, - exactlyTwo_predictsLocalSI⟩ - -/-- Section 3.2: the downward-entailing scope of *not all* supports no local inference on either -version of the prediction. -/ -theorem downward_entailing_blocks : - ¬ PredictsLocalSI (Quant.notAll.sem : Det (Fin 3)) ∧ - ¬ PredictsLocalSIWeak (Quant.notAll.sem : Det (Fin 3)) := - ⟨notAll_not_predictsLocalSI, notAll_not_scopeUp⟩ +/-- Reads the quantifier of a row of (61) and whether the inference is conveyed. -/ +def quantifierRow? (ex : Datum) : Option (Quant × Bool) := do + let q ← ex.parse? "quantifier" [("all", Quant.all), ("moreThanOne", .moreThanOne), + ("exactlyTwo", .exactlyTwo)] + let conveys ← ex.bool? "conveys" + pure (q, conveys) + +example : Datum.ReadCount quantifierRow? Examples.all 3 := by decide + +-- (61), p. 158: (32) prefers the upper-bounded reading of each sentence, and the text says that +-- none of these inferences goes through +theorem rows_61 : ∀ r ∈ Examples.all.filterMap quantifierRow?, + ¬ classicalReading r.1 ⊂ localReading r.1 ∧ r.2 = false := by + have key : ∀ r ∈ Examples.all.filterMap quantifierRow?, + r.1 ∈ [Quant.all, .moreThanOne, .exactlyTwo] ∧ r.2 = false := by decide + intro r hr + refine ⟨(not_classicalReading_ssubset_iff _).2 ?_, (key r hr).2⟩ + rcases List.mem_cons.1 (key r hr).1 with h | h + · exact h ▸ all_predictsLocalSI + rcases List.mem_cons.1 h with h | h + · exact h ▸ moreThanOne_predictsLocalSI + rcases List.mem_singleton.1 h with h + exact h ▸ exactlyTwo_predictsLocalSI + +/-- Reads whether the inference of a row of (56) is conveyed. -/ +def attitudeRow? (ex : Datum) : Option Bool := + (ex.feature? "attitude").bind fun _ ↦ ex.bool? "conveys" + +example : Datum.ReadCount attitudeRow? Examples.all 3 := by decide + +-- (56), pp. 156–157: the Power Principle prefers the parse (57b) that yields each inference, and +-- the text calls that prediction plain false +theorem rows_56 (R : SetRel W W) [ModalLogic.IsSerial R] {some all : Set W} (ha : all ⊂ some) : + ∀ r ∈ Examples.all.filterMap attitudeRow?, + IsLeast {R.core some, Exhaustification.exh {R.core some, R.core all} (R.core some), + R.core (Exhaustification.exh {some, all} some)} + (R.core (Exhaustification.exh {some, all} some)) ∧ r = false := by + have key : ∀ r ∈ Examples.all.filterMap attitudeRow?, r = false := by decide + exact fun r hr ↦ ⟨isLeast_readings_core R ha, key r hr⟩ + +end Rows end Geurts2010 diff --git a/Studies/GeurtsPouscoulous2009.lean b/Studies/GeurtsPouscoulous2009.lean index 50c0d78f15..a7debcc9e7 100644 --- a/Studies/GeurtsPouscoulous2009.lean +++ b/Studies/GeurtsPouscoulous2009.lean @@ -35,8 +35,8 @@ monotonicity of the five quantifiers (`rows_predicted_mainstream`). verification and bracketed prediction rates turned into majority responses; the paper's statistical tests and its methodological argument that the inference paradigm inflates rates stay in prose. -* The verification situations are three squares and three circles; the exact figures of the - stimuli are not given in the paper, only the conditions they satisfy, which the three situations +* The verification situations are three squares and three circles. The paper prints the stimulus + for *all* (`figure2`) and gives only the conditions the others satisfy, which the other situations here meet. * The paper's remark that lexicalist conventionalism reaches only the local reading is not formalized; `so` is the syntax-based variant's operator. @@ -117,6 +117,24 @@ theorem moreThanOne_predictsLocalSIWeak [Fintype α] : PredictsLocalSIWeak (Quant.moreThanOne.sem : Det α) := scopeMonotone_atLeast 2 +theorem exactlyTwo_not_predictsLocalSIWeak : + ¬ PredictsLocalSIWeak (Quant.exactlyTwo.sem : Det (Fin 3)) := + fun h ↦ not_monotone_exactly (n := 2) (by simp) (h Set.univ) + +theorem notAll_not_predictsLocalSIWeak : + ¬ PredictsLocalSIWeak (Quant.notAll.sem : Det (Fin 3)) := fun h ↦ + h Set.univ (Set.empty_subset Set.univ) (fun hall ↦ hall (Set.mem_univ 0)) subset_rfl + +theorem notMoreThanOne_not_predictsLocalSIWeak : + ¬ PredictsLocalSIWeak (Quant.notMoreThanOne.sem : Det (Fin 3)) := by + intro h + have key : Quant.notMoreThanOne.sem (Set.univ : Set (Fin 3)) ∅ → + Quant.notMoreThanOne.sem (Set.univ : Set (Fin 3)) Set.univ := + h Set.univ (Set.empty_subset _) + simp only [Quant.sem] at key + revert key + decide + theorem notAll_not_predictsLocalSI [Fintype α] : ¬ PredictsLocalSI (Quant.notAll.sem : Det α) := not_not.mpr scopeMonotone_every.compl @@ -130,8 +148,12 @@ theorem notMoreThanOne_not_predictsLocalSI [Fintype α] : circles. -/ abbrev Situation := Fin 3 → Fin 3 → Prop -/-- The situation for *all*, *more than one* and the two downward-entailing sentences, in which -every square is connected with some circle and two of them with all. -/ +/-- Figure 2, the printed stimulus for *all*: the top square is connected with all three circles, +and each of the others with two of them. -/ +abbrev figure2 : Situation := fun s c ↦ s = 0 ∨ (s = 1 ∧ c ≠ 2) ∨ (s = 2 ∧ c ≠ 0) + +/-- The situation for *more than one* and the two downward-entailing sentences, in which every +square is connected with some circle and two of them with all. -/ abbrev allSome : Situation := fun s c ↦ s ≠ 0 ∨ c = 0 /-- One square connected with some but not all circles, one with all, one with none. -/ @@ -152,15 +174,22 @@ inductive Trial deriving DecidableEq, Repr def situation : Quant → Trial → Situation + | .all, _ => figure2 | .exactlyTwo, .a => onePartial | .exactlyTwo, .b => twoPartial | _, _ => allSome +/-- The situations in which the sentence with quantifier `q` is true on its classical construal. -/ +def classicalReading (q : Quant) : Set Situation := {R | q.sem Set.univ (someC R)} + +/-- The situations in which it is true on its local-implicature construal. -/ +def localReading (q : Quant) : Set Situation := {R | q.sem Set.univ (someNotAllC R)} + /-- The classical construal of a verification item. -/ -def Classical (q : Quant) (t : Trial) : Prop := q.sem Set.univ (someC (situation q t)) +def Classical (q : Quant) (t : Trial) : Prop := situation q t ∈ classicalReading q /-- The local-implicature construal of a verification item. -/ -def Local (q : Quant) (t : Trial) : Prop := q.sem Set.univ (someNotAllC (situation q t)) +def Local (q : Quant) (t : Trial) : Prop := situation q t ∈ localReading q /-- What mainstream conventionalism predicts of an item, the local construal outside downward-entailing scopes and the classical one within them. -/ @@ -190,33 +219,33 @@ theorem exactlyTwo_predictsLocalSI : PredictsLocalSI (Quant.exactlyTwo.sem : Det decide theorem classical_all : Classical .all .none := - show ∀ s : Fin 3, True → s ∈ someC allSome by decide + show ∀ s : Fin 3, True → s ∈ someC figure2 by decide theorem not_local_all : ¬ Local .all .none := - show ¬ ∀ s : Fin 3, True → s ∈ someNotAllC allSome by decide + show ¬ ∀ s : Fin 3, True → s ∈ someNotAllC figure2 by decide theorem classical_moreThanOne : Classical .moreThanOne .none := by - simp only [Classical, Quant.sem, situation] + simp only [Classical, classicalReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem not_local_moreThanOne : ¬ Local .moreThanOne .none := by - simp only [Local, Quant.sem, situation] + simp only [Local, localReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem classical_exactlyTwo_a : Classical .exactlyTwo .a := by - simp only [Classical, Quant.sem, situation] + simp only [Classical, classicalReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem not_local_exactlyTwo_a : ¬ Local .exactlyTwo .a := by - simp only [Local, Quant.sem, situation] + simp only [Local, localReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem not_classical_exactlyTwo_b : ¬ Classical .exactlyTwo .b := by - simp only [Classical, Quant.sem, situation] + simp only [Classical, classicalReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem local_exactlyTwo_b : Local .exactlyTwo .b := by - simp only [Local, Quant.sem, situation] + simp only [Local, localReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem not_classical_notAll : ¬ Classical .notAll .none := @@ -226,11 +255,11 @@ theorem local_notAll : Local .notAll .none := show ¬ ∀ s : Fin 3, True → s ∈ someNotAllC allSome by decide theorem not_classical_notMoreThanOne : ¬ Classical .notMoreThanOne .none := by - simp only [Classical, Quant.sem, situation] + simp only [Classical, classicalReading, Set.mem_ofPred_eq, Quant.sem, situation] decide theorem local_notMoreThanOne : Local .notMoreThanOne .none := by - simp only [Local, Quant.sem, situation] + simp only [Local, localReading, Set.mem_ofPred_eq, Quant.sem, situation] decide /-! ### The verification rows -/ From aecbe41ce31b753eeb8835d50bb0011eee044e8e Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 3 Nov 2026 14:31:20 -0800 Subject: [PATCH 2/5] docs(Studies/Geurts2010): shorten the module docstring --- Studies/Geurts2010.lean | 117 +++++++++++++++------------------------- 1 file changed, 42 insertions(+), 75 deletions(-) diff --git a/Studies/Geurts2010.lean b/Studies/Geurts2010.lean index 5abe2a9c51..4b584ac64d 100644 --- a/Studies/Geurts2010.lean +++ b/Studies/Geurts2010.lean @@ -13,84 +13,51 @@ public import Mathlib.Order.UpperLower.Basic # Geurts (2010): Quantity Implicatures A quantity implicature is an inference about a speaker's beliefs, drawn from the speaker's not -having said something stronger. If alternatives are closed under conjunction and disjunction, as -the book declines to do, and Competence is assumed wherever it is consistent, the Standard Recipe -[gives exactly the exclusive reading of a long -disjunction](##Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom), but under *may* it [leaves -the speaker no consistent state](##Sentence.standardRecipe_may_or_eq_empty). Starting from a -partition of the speaker's states gives [free choice](##Sentence.mem_survivors_may_or_iff) and -[form-sensitive scalar inferences](##Sentence.mem_survivors_scalar_iff). Comparing readings for -strength [picks out the upward-entailing scopes](##boundedReading_ssubset_iff) in which the -verification experiment finds no upper bound. +having said something stronger. With alternatives closed under conjunction and disjunction, which +the book declines, and Competence assumed wherever consistent, the Standard Recipe [gives exactly +the exclusive reading of a long +disjunction](##Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom); under *may* it [leaves no +consistent state](##Sentence.standardRecipe_may_or_eq_empty). Partitioning the speaker's states +instead gives [free choice](##Sentence.mem_survivors_may_or_iff) and [form-sensitive scalar +inferences](##Sentence.mem_survivors_scalar_iff). Comparing readings for strength [picks out the +upward-entailing scopes](##boundedReading_ssubset_iff), where the experiment finds no upper bound. ## Implementation notes -* A state is the set of worlds compatible with what the speaker believes. For the performative (19), - p. 118, it is read as what the speaker permits, the text giving the case the same logical - structure. -* `may` quantifies over the speaker's own state, so that the assumption of p. 111, footnote 5, that - a speaker who does not believe that something may be so believes that it is not, holds by - construction. -* `NeoGricean.IsSecondaryImplicature` is not the book's rule: the Standard Recipe is a heuristic and - the hearer may adopt or reject Competence (pp. 37, 39–40). It is used as the necessary condition - on Competence of p. 41, checked per alternative rather than jointly, and strengthening wherever it - holds is an assumption made here. -* `Sentence.survivors` applies the heuristic (i) categorically to single states with one alternative - per cell, where p. 116 has "probably", p. 121 weighs states against each other and pp. 113 and 115 - allow several sentences. `Sentence.Entails` preserves belief, not truth. -* `Sentence.size` stands in for economy and is one instance of the preorder `cost`, where lower - means more available (p. 123). Previous use in (23), p. 122, is modelled by lowering the sentence - to zero, although the text has the *construction* used, of the interns. -* (26b), p. 124, comes out under the heuristic (i) alone, by length, where the text credits - monolexicality and salience. -* The upper sets of the worlds of (29), p. 61, are the closure of the disjuncts under conjunction - and disjunction ([each is a union of conjunctions](##eq_iUnion_iInter_of_isUpperSet)), up to the - empty set and the whole space, neither of which bears on a strong implicature. -* The alternatives of (20) are a reconstruction, since p. 120 prints none; the extension to any - number of disjuncts in `inter_nonempty_of_forall_not_subset` is not the text's. A state of (32), - p. 179, as a relation between worlds and values of the referent, renders a model the text calls - "extremely sketchy" (p. 178). -* The operator O of (39), p. 148, is `Exhaustification.exh`. -* (61b) and (61c) are read through the quantifiers of (62), which the text calls parallel (p. 159). +* A state is the worlds compatible with the speaker's beliefs. `may` quantifies over it, which + builds in footnote 5 of p. 111. +* `IsSecondaryImplicature` serves as the necessary condition on Competence of p. 41, per + alternative; strengthening wherever it holds is an assumption made here, the book's Recipe being + a heuristic. +* `Sentence.survivors` applies heuristic (i) categorically, with one alternative per cell and `size` + for economy, so (26b) comes out by length rather than the monolexicality p. 124 credits. +* Upper sets are the closure of the disjuncts under conjunction and disjunction ([each is a union of + conjunctions](##eq_iUnion_iInter_of_isUpperSet)). +* The alternatives of (20), p. 120, are reconstructed; (61b, c) are read through the quantifiers of + (62). ## Errata -* pp. 63–64 say that (35) enables the inferences that the speaker does not know whether or not `x`. - With three disjuncts they enable only that the speaker does not believe `x`: [believing a disjunct - false stays consistent](##isSecondaryImplicature_Ici) with Quality and the weak implicatures of - (34) and (35), though [not of all disjuncts together](##eq_empty_of_forall_subset_compl_Ici). So - the looseness p. 40 calls immaterial matters here, and "why not infer one of the two?" (p. 41) is - answered only for two. -* p. 64 rejects closing the alternatives under disjunction as repeating the trouble of (32). Under - that closure the weak implicature of *A or B* blocks the strong implicature of (32b), since - Quality would then give belief in *A or B*: [only alternatives false wherever just one disjunct - holds pass](##isSecondaryImplicature_upperSets_iff), and the closure [gives ignorance about every - disjunct](##notMem_polar_Ici_of_mem_primaryImplicatures). (7d), p. 167, is such a disjunctive - alternative, and p. 168 itself blocks its strengthening. -* p. 115 concludes that George "may be American", for British. -* p. 143 paraphrases the negated upper-bounded *like* in (25) as "either we don't like coffee or we - don't love it". [It is *or we love it*](##compl_sdiff_like): the printed form excludes the - continuation *we LOVE it*, and p. 187 has "like but not love". -* p. 149 says that (42b) expresses the "many but not all" reading of (41). The computation on the - same page, p. 150, and [`exh`](##exh_compl_many) give *some but not many*. -* p. 168 cites (9a), but (9) has no parts. -* (11), p. 169, prints the disjunction outside the speaker's belief, where the prose has it inside, - as Competence of the subject, and (16), p. 170, follows it. [Given (10) or (15) the two - coincide](##subset_or_subset_iff), so the derivation stands. -* (46), p. 188, prints *drinking and drinking non-alcoholic beverages*. By (39) the prejacent is - conjoined with the *denial* of the alternative. -* p. 189 overstates in putting the shift of a lower bound "simply out of reach" of O: [O reaches it - given the alternative RICH₁](##exh_rich), the stipulation pp. 188–189 grant elsewhere as "wildly - ad hoc". +* pp. 63–64: with three disjuncts (35) gives only non-belief in `x`, since [believing it false stays + consistent](##isSecondaryImplicature_Ici). +* p. 64: closure under disjunction does not repeat the trouble of (32): [only alternatives false + wherever just one disjunct holds pass](##isSecondaryImplicature_upperSets_iff), and it [gives + ignorance](##notMem_polar_Ici_of_mem_primaryImplicatures). +* p. 115: "American" for British. +* p. 143: (25) should end [*or we love it*](##compl_sdiff_like). +* p. 149: (42b) is [*some but not many*](##exh_compl_many), not "many but not all". +* p. 168: (9a) for (9). +* pp. 169–170: (11) and (16) put the disjunction outside the belief, [harmlessly given (10) or + (15)](##subset_or_subset_iff). +* p. 188: (46) omits *not*. +* p. 189: [O reaches RICH₂ given RICH₁](##exh_rich), so "out of reach" overstates. ## TODO -* The presupposition-based implicatures of §8.3, the open alternatives of §6.6 with conditional - perfection, and Spector's route for belief reports (pp. 169–170, [spector-2006]) are not - formalized. -* Separate the consistency check from the innocent exclusion of [fox-2007] at (34) and (35), which - should locate what disjunctive closure adds. -* The experiments of Chapters 4 and 5 belong in `Data/Statistics`. +* §8.3 presupposition implicatures, §6.6 open alternatives, and Spector's route (pp. 169–170, + [spector-2006]). +* The consistency check against the innocent exclusion of [fox-2007] at (34) and (35). +* The experiments of Chapters 4 and 5, for `Data/Statistics`. ## References @@ -475,7 +442,8 @@ private theorem believes_entails_top (hs : s.Nonempty) (hu : u.Believes V s) (hx noncomputable abbrev sayOr (V : P → Set W) (p q : P) : Set W → Sentence P := sayEither V (atom p) (atom q) (atom p) (atom q) (or (atom p) (atom q)) -/-- (17), p. 117: *George may be British or Canadian*, with the alternatives (18). -/ +/-- (17), p. 117: *George may be British or Canadian*, with the alternatives (18). For the +performative (19), p. 118, a state is what the speaker permits. -/ noncomputable abbrev sayMayOr (V : P → Set W) (p q : P) : Set W → Sentence P := say V (atom p) (atom q) (may (atom p)) (may (atom q)) (and (may (atom p)) (may (atom q))) @@ -579,8 +547,8 @@ theorem subset_compl_of_mem_survivors_scalar s ⊆ (V q)ᶜ := (Question.mem_polar.1 hc).resolve_left ((mem_survivors_scalar_iff.1 h).2.2 le_rfl) --- (23), p. 122: with *many though not all* in the discourse, previous use lowers that alternative, --- the state of believing *not all* goes too, and no opinion is left +-- (23), p. 122: with *many though not all* in the discourse (of the interns, in the text), previous +-- use lowers that alternative, the state of believing *not all* goes too, and no opinion is left theorem mem_survivors_indicator_iff (hx : x.size ≤ u.size) : s ∈ survivors V (({and u (neg x)}ᶜ : Set (Sentence P)).indicator size) u (sayScalar V u x) ↔ s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ (neg x).Poss V s := by @@ -652,9 +620,8 @@ theorem areAlternatives_sayMany (hm : Monotone many) : end Pizza --- (31), p. 61, with p. 115: a speaker who rules out a disjunct could have used the shorter --- disjunction, so that the survivors of the heuristic consider every disjunct possible, at any --- length +-- (31), p. 61, with p. 115, extending the text: a speaker who rules out a disjunct could have used +-- the shorter disjunction, so the survivors of the heuristic consider every disjunct possible theorem inter_nonempty_of_forall_not_subset {ι : Type*} {A : ι → Set W} {J : Finset ι} {i : ι} (hq : s ⊆ ⋃ j ∈ J, A j) (h : ∀ J' ⊂ J, ¬ s ⊆ ⋃ j ∈ J', A j) (hi : i ∈ J) : (s ∩ A i).Nonempty := by From 01259e1cdd3634abf2e4415d1aa0d5032f46422a Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 3 Nov 2026 15:01:23 -0800 Subject: [PATCH 3/5] refactor(Studies/Geurts2010): use exh for so, share the atom step --- Linglib/Semantics/Exhaustification/Basic.lean | 5 ++ .../Exhaustification/InnocentExclusion.lean | 4 +- Studies/Geurts2010.lean | 56 ++++++++----------- Studies/GeurtsPouscoulous2009.lean | 52 +++++++++-------- 4 files changed, 55 insertions(+), 62 deletions(-) diff --git a/Linglib/Semantics/Exhaustification/Basic.lean b/Linglib/Semantics/Exhaustification/Basic.lean index 93b294e31b..8d0afe1a1d 100644 --- a/Linglib/Semantics/Exhaustification/Basic.lean +++ b/Linglib/Semantics/Exhaustification/Basic.lean @@ -112,6 +112,11 @@ theorem exh_eq_sdiff_of_forall (hq : q ∈ C) (hpq : ¬ p ⊆ q) (h : ∀ r ∈ Set.ext fun _ ↦ and_congr_right fun _ ↦ ⟨fun hw hwq ↦ hpq (hw q hq hwq), fun hw r hr hwr ↦ (h r hr).resolve_right fun hrq ↦ hw (hrq hwr)⟩ +theorem exh_pair (h : ¬ p ⊆ q) : exh {p, q} p = p \ q := + exh_eq_sdiff_of_forall (by simp) h (by + rintro r (rfl | rfl) + exacts [.inl subset_rfl, .inr subset_rfl]) + theorem exh_eq_self_iff : exh C p = p ↔ ∀ q ∈ C, (p ∩ q).Nonempty → p ⊆ q := ⟨fun h q hq ⟨w, hw, hwq⟩ ↦ by rw [← h] at hw; exact hw.2 q hq hwq, fun h ↦ (exh_subset C p).antisymm fun w hw ↦ ⟨hw, fun q hq hwq ↦ h q hq ⟨w, hw, hwq⟩⟩⟩ diff --git a/Linglib/Semantics/Exhaustification/InnocentExclusion.lean b/Linglib/Semantics/Exhaustification/InnocentExclusion.lean index 502cd33a3e..c9e23ce226 100644 --- a/Linglib/Semantics/Exhaustification/InnocentExclusion.lean +++ b/Linglib/Semantics/Exhaustification/InnocentExclusion.lean @@ -298,9 +298,7 @@ theorem exhIE_singleton_self : exhIE {φ} φ = φ := exhIE_eq_self_of_forall _ _ fun _ ha _ ↦ (mem_singleton_iff.1 ha).ge theorem exhIE_pair_sdiff {d : Set World} (hne : (φ \ d).Nonempty) : exhIE {φ, d} φ = φ \ d := by - have hexh : exh {φ, d} φ = φ \ d := exh_eq_sdiff_of_forall (by simp) - (fun h ↦ let ⟨_, hw, hwd⟩ := hne; hwd (h hw)) - (by rintro r (rfl | rfl); exacts [.inl subset_rfl, .inr subset_rfl]) + have hexh : exh {φ, d} φ = φ \ d := exh_pair fun h ↦ let ⟨_, hw, hwd⟩ := hne; hwd (h hw) rw [exhIE_eq_exh_of_nonempty _ _ (hexh ▸ hne), hexh] theorem not_isInnocentlyExcludable_of_subset_union (hfin : ALT.Finite) {p q : Set World} diff --git a/Studies/Geurts2010.lean b/Studies/Geurts2010.lean index 4b584ac64d..b1be117bf1 100644 --- a/Studies/Geurts2010.lean +++ b/Studies/Geurts2010.lean @@ -226,6 +226,15 @@ example : ({0, 1} : Set (Fin 3)) ∈ Ioi ⊥ \ Ici ⊤ ∧ ¬ IsAtom ({0, 1} : S variable [IsAtomic α] +private theorem exists_isAtom_le {y : α} (hy : y ∈ Ioi ⊥) : ∃ b, IsAtom b ∧ b ≤ y := + (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 hy).ne' + +-- an upper set with every atom in it holds wherever a disjunct does +private theorem Ioi_bot_subset_of_forall_isAtom_mem {χ : Set α} (hχ : IsUpperSet χ) + (h : ∀ x, IsAtom x → x ∈ χ) : Ioi ⊥ ⊆ χ := fun _ hy ↦ + let ⟨_, hb, hby⟩ := exists_isAtom_le hy + hχ hby (h _ hb) + -- contra p. 64: over alternatives closed under conjunction and disjunction, an alternative passes -- the consistency check just when it holds in no world in which only one disjunct does theorem isSecondaryImplicature_upperSets_iff : @@ -236,9 +245,7 @@ theorem isSecondaryImplicature_upperSets_iff : ⟨fun h x hx hxt ↦ ?_, fun h χ hχ hχφ hsub ↦ ?_⟩ · exact h _ (isLowerSet_Iic x).compl (compl_Iic_ssubset_Ioi_bot hx) fun y hy hle ↦ hy.2 ((hx.le_iff_eq (mem_Ioi.1 hy.1).ne').1 hle ▸ hxt) - · obtain ⟨y, hy, hyχ⟩ := not_subset.1 hχφ.2 - obtain ⟨b, hb, hby⟩ := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 hy).ne' - exact hyχ (hχ hby (hsub ⟨hb.bot_lt, h b hb⟩)) + · exact hχφ.2 (Ioi_bot_subset_of_forall_isAtom_mem hχ fun b hb ↦ hsub ⟨hb.bot_lt, h b hb⟩) /-- Closing the alternatives of a long disjunction under conjunction and under disjunction, and strengthening wherever Competence is consistent, yields exactly the exclusive reading. -/ @@ -248,7 +255,7 @@ theorem Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom : simp only [mem_sdiff, mem_Ioi, mem_sUnion, mem_ofPred_eq, isSecondaryImplicature_upperSets_iff] refine ⟨fun ⟨hx, hn⟩ ↦ ?_, fun hx ↦ ⟨hx.bot_lt, fun ⟨t, ⟨_, _, h⟩, hxt⟩ ↦ h x hx hxt⟩⟩ by_contra hna - obtain ⟨b, hb, hbx⟩ := (eq_bot_or_exists_atom_le x).resolve_left hx.ne' + obtain ⟨b, hb, hbx⟩ := exists_isAtom_le hx refine hn ⟨Ici x, ⟨isUpperSet_Ici x, ⟨fun _ hy ↦ hx.trans_le hy, fun h ↦ ?_⟩, fun y hy hxy ↦ ?_⟩, le_rfl⟩ · exact hna (le_antisymm hbx (h hb.bot_lt) ▸ hb) @@ -259,15 +266,13 @@ theorem Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom : theorem setOf_isAtom_mem_primaryImplicatures : {x : α | IsAtom x} ∈ primaryImplicatures (Ioi ⊥) {χ | IsUpperSet χ} := mem_primaryImplicatures.2 fun _ hχ hχφ hsub ↦ - let ⟨y, hy, hyχ⟩ := not_subset.1 hχφ.2 - let ⟨_, hb, hby⟩ := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 hy).ne' - hyχ (hχ hby (hsub hb)) + hχφ.2 (Ioi_bot_subset_of_forall_isAtom_mem hχ fun _ hb ↦ hsub hb) -- p. 41: that the speaker cannot believe all the disjuncts false holds at any length theorem eq_empty_of_forall_subset_compl_Ici {s : Set α} (hq : s ⊆ Ioi ⊥) (h : ∀ a, IsAtom a → s ⊆ (Ici a)ᶜ) : s = ∅ := - eq_empty_of_forall_notMem fun y hy ↦ - let ⟨_, hb, hby⟩ := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 (hq hy)).ne' + eq_empty_of_forall_notMem fun _ hy ↦ + let ⟨_, hb, hby⟩ := exists_isAtom_le (hq hy) h _ hb hy hby example : Ioi ⊥ \ ⋃₀ {t | IsSecondaryImplicature (Ioi ⊥) {χ | IsUpperSet χ} t} = @@ -454,7 +459,7 @@ theorem mem_survivors_or_iff : mem_survivors_sayEither_iff (by simp [size]) (by simp [size]) -- p. 115: (16) are alternatives in the sense of the method -theorem areAlternatives_sayOr : AreAlternatives V (or (atom p) (atom q)) (sayOr V p q) := +example : AreAlternatives V (or (atom p) (atom q)) (sayOr V p q) := fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V (or (atom p) (atom q))) (believes_entails_top hs h) (fun _ hq ↦ ⟨fun w hw ↦ (h hw).resolve_right fun hwq ↦ hq ⟨w, hw, hwq⟩, @@ -472,8 +477,7 @@ theorem mem_survivors_may_or_iff : exact (believes_may hs).2 (poss_or.2 (.inl hp)) -- p. 117: (18) are alternatives in the sense of the method -theorem areAlternatives_sayMayOr : - AreAlternatives V (may (or (atom p) (atom q))) (sayMayOr V p q) := fun s hs h ↦ by +example : AreAlternatives V (may (or (atom p) (atom q))) (sayMayOr V p q) := fun s hs h ↦ by have key {r : P} (hr : V r ⊆ V p ∪ V q) : (may (atom r)).Entails V (may (or (atom p) (atom q))) := fun _ h' _ hw ↦ (h' hw).mono (inter_subset_inter_right _ hr) refine say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V (may (or (atom p) (atom q)))) @@ -535,7 +539,7 @@ theorem mem_survivors_scalar_iff : exact absurd (let ⟨w, hw⟩ := hs; ⟨w, hw, hn hw⟩) hp -- p. 113: (14) are alternatives in the sense of the method -theorem areAlternatives_sayScalar (hx : x.Entails V u) : AreAlternatives V u (sayScalar V u x) := +example (hx : x.Entails V u) : AreAlternatives V u (sayScalar V u x) := fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V u) (fun hp _ ↦ ⟨believes_and.2 ⟨h, (believes_may hs).2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩) (fun _ hn ↦ ⟨not_poss_neg.1 hn, hx⟩) @@ -607,7 +611,7 @@ theorem mem_survivors_many_iff : (atom .somePasta).Poss V₂₀ s := mem_survivors_sayEither_iff le_rfl le_rfl -theorem areAlternatives_sayMany (hm : Monotone many) : +example (hm : Monotone many) : AreAlternatives V₂₀ (atom .manyEither) (sayMany many pizza pasta) := fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V₂₀ s ∧ r.Entails V₂₀ (atom .manyEither)) (believes_entails_top hs h) @@ -724,12 +728,8 @@ theorem isLeast_readings_negation (hs : many ⊂ some) (ha : all ⊂ many) : theorem isLeast_readings_core (R : SetRel W W) [ModalLogic.IsSerial R] (ha : all ⊂ some) : IsLeast {R.core some, exh {R.core some, R.core all} (R.core some), R.core (exh {some, all} some)} (R.core (exh {some, all} some)) := by - have hsome : exh {some, all} some = some \ all := - exh_eq_sdiff_of_forall (by simp) ha.2 (by - rintro r (rfl | rfl) - exacts [.inl subset_rfl, .inr subset_rfl]) have hcore : R.core (some \ all) ⊆ R.core some := fun _ hw _ hv ↦ (hw hv).1 - rw [hsome] + rw [exh_pair ha.2] refine ⟨by simp, ?_⟩ rintro _ (rfl | rfl | rfl) · exact hcore @@ -797,10 +797,10 @@ theorem isSecondaryImplicature_mango_iff (hA : A ⊆ F) (hM : (M \ F).Nonempty) open GeurtsPouscoulous2009 in -- §8.2, (10)–(12), pp. 168–169, after [vanrooij-schulz-2004] and [russell-2006]: the reading of (9) -- that looks local, from the strong implicature at the speaker and Competence of the subject -theorem subset_core_sdiff {R : SetRel W W} {some all : Set W} (hall : all ⊂ some) +theorem subset_core_exh {R : SetRel W W} {some all : Set W} (hall : all ⊂ some) (hq : s ⊆ R.core some) (h10 : s ⊆ (R.core all)ᶜ) (h11 : s ⊆ R.core all ∪ R.core allᶜ) : - s ⊆ R.core (some \ all) := - so_pair hall ▸ fun _ hw ↦ local_of_global_of_opinionated R hall (hq hw) (h10 hw) (h11 hw) + s ⊆ R.core (Exhaustification.exh {some, all} some) := + fun _ hw ↦ local_of_global_of_opinionated R hall (hq hw) (h10 hw) (h11 hw) -- (10)–(12) and, for *hope*, (15)–(17), pp. 170–171, share this form, for any attitude: what -- separates them is the plausibility of the second premise. (11) and (16), as printed, have the @@ -980,16 +980,8 @@ example : Datum.ReadCount quantifierRow? Examples.all 3 := by decide -- none of these inferences goes through theorem rows_61 : ∀ r ∈ Examples.all.filterMap quantifierRow?, ¬ classicalReading r.1 ⊂ localReading r.1 ∧ r.2 = false := by - have key : ∀ r ∈ Examples.all.filterMap quantifierRow?, - r.1 ∈ [Quant.all, .moreThanOne, .exactlyTwo] ∧ r.2 = false := by decide - intro r hr - refine ⟨(not_classicalReading_ssubset_iff _).2 ?_, (key r hr).2⟩ - rcases List.mem_cons.1 (key r hr).1 with h | h - · exact h ▸ all_predictsLocalSI - rcases List.mem_cons.1 h with h | h - · exact h ▸ moreThanOne_predictsLocalSI - rcases List.mem_singleton.1 h with h - exact h ▸ exactlyTwo_predictsLocalSI + simp only [not_classicalReading_ssubset_iff, Quant.predictsLocalSI_iff] + decide /-- Reads whether the inference of a row of (56) is conveyed. -/ def attitudeRow? (ex : Datum) : Option Bool := diff --git a/Studies/GeurtsPouscoulous2009.lean b/Studies/GeurtsPouscoulous2009.lean index a7debcc9e7..d9f0bcb526 100644 --- a/Studies/GeurtsPouscoulous2009.lean +++ b/Studies/GeurtsPouscoulous2009.lean @@ -1,6 +1,7 @@ module public import Linglib.Logic.Modal.Defs +public import Linglib.Semantics.Exhaustification.Basic public import Linglib.Semantics.Quantification.Counting public import Linglib.Semantics.Quantification.Properties public import Linglib.Data.Examples.GeurtsPouscoulous2009 @@ -9,18 +10,18 @@ public import Linglib.Data.Examples.Readers /-! # Geurts and Pouscoulous (2009): Embedded implicatures?!? -This file formalizes the theoretical frame of [geurts-pouscoulous-2009]'s experimental case -against conventionalist theories of scalar implicature ([chierchia-2004], [fox-2007], -[chierchia-fox-spector-2008]), which posit a silent exhaustivity operator adjoinable to any -clause and predict local scalar inferences systematically. The operator `so` negates every -stronger alternative of its prejacent; under a belief verb the parse with `so` below the verb +This file formalizes the theoretical frame of [geurts-pouscoulous-2009]'s experimental case against +conventionalist theories of scalar implicature ([chierchia-2004], [fox-2007], +[chierchia-fox-spector-2008]), which posit a silent exhaustivity operator adjoinable to any clause +and predict local scalar inferences systematically. The operator `Exhaustification.exh` denies every +alternative its prejacent does not entail; under a belief verb the parse with it below the verb yields the local reading, that the agent believes *some but not all*, and the parse above it the -global reading, that the agent believes *some* and does not believe *all* -(`local_reading`, `so_pair`). The paper's Gricean reply is that the local reading follows from the -global one whenever the agent is opinionated on the stronger alternative -(`local_of_global_of_opinionated`), while the analogous derivation for a universal quantifier -needs a uniformity assumption across the domain (`all_not_all_of_uniform`) that is far less -plausible, so seemingly local inferences are expected under *believe* and nowhere else. +global reading, that the agent believes *some* and does not believe *all* (`local_reading`). The +paper's Gricean reply is that the local reading follows from the global one whenever the agent is +opinionated on the stronger alternative (`local_of_global_of_opinionated`), while the analogous +derivation for a universal quantifier needs a uniformity assumption across the domain +(`all_not_all_of_uniform`) that is far less plausible, so seemingly local inferences are expected +under *believe* and nowhere else. Mainstream conventionalism predicts the local construal wherever the embedding scope is not downward entailing (`PredictsLocalSI`, weakly `PredictsLocalSIWeak`). The third experiment's @@ -39,7 +40,7 @@ monotonicity of the five quantifiers (`rows_predicted_mainstream`). for *all* (`figure2`) and gives only the conditions the others satisfy, which the other situations here meet. * The paper's remark that lexicalist conventionalism reaches only the local reading is not - formalized; `so` is the syntax-based variant's operator. + formalized; `exh` is the syntax-based variant's operator. ## References @@ -54,31 +55,20 @@ monotonicity of the five quantifiers (`rows_predicted_mainstream`). namespace GeurtsPouscoulous2009 -open Quantifier Quantifier.Det ModalLogic +open Quantifier Quantifier.Det ModalLogic Exhaustification open SetRel variable {W : Type*} /-! ### The silent exhaustivity operator -/ -/-- The silent operator of syntax-based conventionalism conjoins the prejacent with the negation -of every stronger alternative. -/ -def so (φ : Set W) (A : Set (Set W)) : Set W := {w | w ∈ φ ∧ ∀ ψ ∈ A, ψ ⊂ φ → w ∉ ψ} - -theorem so_pair {φ ψ : Set W} (h : ψ ⊂ φ) : so φ {φ, ψ} = φ \ ψ := by - ext w - simp only [so, Set.mem_ofPred_eq, Set.mem_sdiff, Set.mem_insert_iff, Set.mem_singleton_iff, - forall_eq_or_imp, forall_eq] - exact ⟨fun ⟨hw, _, hψ⟩ ↦ ⟨hw, hψ h⟩, - fun ⟨hw, hψ⟩ ↦ ⟨hw, fun hφ ↦ absurd hφ (lt_irrefl φ), fun _ ↦ hψ⟩⟩ - theorem local_reading (R : SetRel W W) {some all : Set W} (h : all ⊂ some) : - R.core (so some {some, all}) = R.core some ∩ R.core allᶜ := by - rw [so_pair h, Set.sdiff_eq, core_inter] + R.core (exh {some, all} some) = R.core some ∩ R.core allᶜ := by + rw [exh_pair h.2, Set.sdiff_eq, core_inter] theorem local_of_global_of_opinionated (R : SetRel W W) {some all : Set W} (h : all ⊂ some) {w : W} (h₃₁ : w ∈ R.core some) (h₃₂ : w ∉ R.core all) - (h₃₃ : w ∈ R.core all ∨ w ∈ R.core allᶜ) : w ∈ R.core (so some {some, all}) := by + (h₃₃ : w ∈ R.core all ∨ w ∈ R.core allᶜ) : w ∈ R.core (exh {some, all} some) := by rw [local_reading R h] exact ⟨h₃₁, h₃₃.resolve_left h₃₂⟩ @@ -218,6 +208,14 @@ theorem exactlyTwo_predictsLocalSI : PredictsLocalSI (Quant.exactlyTwo.sem : Det revert key decide +theorem Quant.predictsLocalSI_iff : + ∀ q : Quant, PredictsLocalSI (q.sem : Det (Fin 3)) ↔ q ∉ [Quant.notAll, .notMoreThanOne] + | .all => iff_of_true all_predictsLocalSI (by decide) + | .moreThanOne => iff_of_true moreThanOne_predictsLocalSI (by decide) + | .exactlyTwo => iff_of_true exactlyTwo_predictsLocalSI (by decide) + | .notAll => iff_of_false notAll_not_predictsLocalSI (by decide) + | .notMoreThanOne => iff_of_false notMoreThanOne_not_predictsLocalSI (by decide) + theorem classical_all : Classical .all .none := show ∀ s : Fin 3, True → s ∈ someC figure2 by decide From e1b9f6f6e8ba1b2099819c7eaae3d996077fbe29 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 3 Nov 2026 15:28:08 -0800 Subject: [PATCH 4/5] refactor(Studies/Geurts2010): list cells directly, exh_insert API --- Linglib/Semantics/Exhaustification/Basic.lean | 32 +- .../Exhaustification/InnocentExclusion.lean | 4 +- Studies/Chierchia2006.lean | 4 +- Studies/Fox2007.lean | 9 +- Studies/Geurts2010.lean | 562 ++++++------------ Studies/GeurtsPouscoulous2009.lean | 4 +- 6 files changed, 204 insertions(+), 411 deletions(-) diff --git a/Linglib/Semantics/Exhaustification/Basic.lean b/Linglib/Semantics/Exhaustification/Basic.lean index 8d0afe1a1d..d91b8ebb46 100644 --- a/Linglib/Semantics/Exhaustification/Basic.lean +++ b/Linglib/Semantics/Exhaustification/Basic.lean @@ -105,18 +105,6 @@ theorem excludes_eq_compl_sUnion (C : Set (Set W)) (p : Set W) : theorem exh_eq_sdiff (C : Set (Set W)) (p : Set W) : exh C p = p \ ⋃₀ {q ∈ C | ¬ p ⊆ q} := by rw [exh, excludes_eq_compl_sUnion, Set.sdiff_eq] -/-- When every alternative is entailed by the prejacent or entails the non-entailed `q`, -exhaustifying removes just `q`. -/ -theorem exh_eq_sdiff_of_forall (hq : q ∈ C) (hpq : ¬ p ⊆ q) (h : ∀ r ∈ C, p ⊆ r ∨ r ⊆ q) : - exh C p = p \ q := - Set.ext fun _ ↦ and_congr_right fun _ ↦ ⟨fun hw hwq ↦ hpq (hw q hq hwq), - fun hw r hr hwr ↦ (h r hr).resolve_right fun hrq ↦ hw (hrq hwr)⟩ - -theorem exh_pair (h : ¬ p ⊆ q) : exh {p, q} p = p \ q := - exh_eq_sdiff_of_forall (by simp) h (by - rintro r (rfl | rfl) - exacts [.inl subset_rfl, .inr subset_rfl]) - theorem exh_eq_self_iff : exh C p = p ↔ ∀ q ∈ C, (p ∩ q).Nonempty → p ⊆ q := ⟨fun h q hq ⟨w, hw, hwq⟩ ↦ by rw [← h] at hw; exact hw.2 q hq hwq, fun h ↦ (exh_subset C p).antisymm fun w hw ↦ ⟨hw, fun q hq hwq ↦ h q hq ⟨w, hw, hwq⟩⟩⟩ @@ -124,6 +112,26 @@ theorem exh_eq_self_iff : exh C p = p ↔ ∀ q ∈ C, (p ∩ q).Nonempty → p theorem exh_eq_self (h : ∀ q ∈ C, p ⊆ q) : exh C p = p := exh_eq_self_iff.2 fun q hq _ ↦ h q hq +@[simp] theorem exh_empty (p : Set W) : exh ∅ p = p := exh_eq_self fun _ h ↦ h.elim + +/-- An alternative the prejacent entails is inert. -/ +theorem exh_insert_of_subset (h : p ⊆ q) : exh (insert q C) p = exh C p := + Set.ext fun _ ↦ and_congr_right fun _ ↦ ⟨fun hw r hr ↦ hw r (.inr hr), + fun hw r hr hwr ↦ hr.elim (fun e ↦ e ▸ h) (hw r · hwr)⟩ + +/-- An alternative the prejacent does not entail is denied. -/ +theorem exh_insert_of_not_subset (h : ¬ p ⊆ q) : exh (insert q C) p = exh C p \ q := + Set.ext fun _ ↦ ⟨fun ⟨hp, hw⟩ ↦ + ⟨⟨hp, fun r hr ↦ hw r (.inr hr)⟩, fun hq ↦ h (hw q (.inl rfl) hq)⟩, + fun ⟨⟨hp, hw⟩, hq⟩ ↦ ⟨hp, fun r hr hwr ↦ + hr.elim (fun e ↦ absurd (e ▸ hwr) hq) (hw r · hwr)⟩⟩ + +theorem exh_singleton_of_subset (h : p ⊆ q) : exh {q} p = p := + exh_eq_self fun _ hr ↦ (Set.mem_singleton_iff.1 hr) ▸ h + +theorem exh_singleton_of_not_subset (h : ¬ p ⊆ q) : exh {q} p = p \ q := by + rw [← insert_empty_eq, exh_insert_of_not_subset h, exh_empty] + theorem excludes_antitone (h : C ⊆ C') (p : Set W) : excludes C' p ⊆ excludes C p := fun _ hw q hq ↦ hw q (h hq) diff --git a/Linglib/Semantics/Exhaustification/InnocentExclusion.lean b/Linglib/Semantics/Exhaustification/InnocentExclusion.lean index c9e23ce226..d6e469ad65 100644 --- a/Linglib/Semantics/Exhaustification/InnocentExclusion.lean +++ b/Linglib/Semantics/Exhaustification/InnocentExclusion.lean @@ -298,7 +298,9 @@ theorem exhIE_singleton_self : exhIE {φ} φ = φ := exhIE_eq_self_of_forall _ _ fun _ ha _ ↦ (mem_singleton_iff.1 ha).ge theorem exhIE_pair_sdiff {d : Set World} (hne : (φ \ d).Nonempty) : exhIE {φ, d} φ = φ \ d := by - have hexh : exh {φ, d} φ = φ \ d := exh_pair fun h ↦ let ⟨_, hw, hwd⟩ := hne; hwd (h hw) + have hexh : exh {φ, d} φ = φ \ d := by + rw [exh_insert_of_subset subset_rfl, + exh_singleton_of_not_subset fun h ↦ let ⟨_, hw, hwd⟩ := hne; hwd (h hw)] rw [exhIE_eq_exh_of_nonempty _ _ (hexh ▸ hne), hexh] theorem not_isInnocentlyExcludable_of_subset_union (hfin : ALT.Finite) {p q : Set World} diff --git a/Studies/Chierchia2006.lean b/Studies/Chierchia2006.lean index bfc602922b..665b0f36db 100644 --- a/Studies/Chierchia2006.lean +++ b/Studies/Chierchia2006.lean @@ -173,9 +173,9 @@ def atLeastTwo (S : Finset E) : Set W := {w | ∃ x ∈ S, ∃ y ∈ S, x ≠ y -- (81a), (81b) theorem exh_atLeastTwo_eq_exactlyOne (h : ¬ (⋃ x ∈ S, P x) ⊆ atLeastTwo P S) : exh {atLeastTwo P S} (⋃ x ∈ S, P x) = exactlyOne P S := by + rw [exh_singleton_of_not_subset h] ext w - simp only [mem_exh, Set.mem_singleton_iff, forall_eq, imp_iff_not h] - simp only [Set.mem_iUnion, exists_prop, exactlyOne, atLeastTwo, Set.mem_ofPred_eq] + simp only [Set.mem_sdiff, Set.mem_iUnion, exists_prop, exactlyOne, atLeastTwo, Set.mem_ofPred_eq] constructor · rintro ⟨⟨x, hx, hPx⟩, h2⟩ exact ⟨x, ⟨hx, hPx⟩, fun y ⟨hy, hPy⟩ ↦ by_contra fun hyx ↦ h2 ⟨y, hy, x, hx, hyx, hPy, hPx⟩⟩ diff --git a/Studies/Fox2007.lean b/Studies/Fox2007.lean index 2cbbcd2bd0..3d28d9b3d6 100644 --- a/Studies/Fox2007.lean +++ b/Studies/Fox2007.lean @@ -231,10 +231,11 @@ theorem exhIE_w : exhIE {w, s, n, e} w = w \ e := by theorem exhIE_s : exhIE {w, s, n, e} s = s \ n := by obtain ⟨rfl, -, hn, ⟨a, has, han⟩, -⟩ := h - have hexh : exh {s ∪ n, s, n, e} s = s \ n := exh_eq_sdiff_of_forall (by simp) - (fun h ↦ han (h has)) (by - rintro r (rfl | rfl | rfl | rfl) - exacts [.inl subset_union_left, .inl subset_rfl, .inr subset_rfl, .inr hn]) + have hsn : ¬ s ⊆ n := fun h ↦ han (h has) + have hexh : exh {s ∪ n, s, n, e} s = s \ n := by + rw [exh_insert_of_subset subset_union_left, exh_insert_of_subset subset_rfl, + exh_insert_of_not_subset hsn, exh_singleton_of_not_subset (hsn <| ·.trans hn), + sdiff_sdiff_left, sup_eq_right.2 hn] rw [exhIE_eq_exh_of_nonempty _ _ (hexh ▸ ⟨a, has, han⟩), hexh] theorem exhIE_n : exhIE {w, s, n, e} n = n \ s := by diff --git a/Studies/Geurts2010.lean b/Studies/Geurts2010.lean index b1be117bf1..200c3c530b 100644 --- a/Studies/Geurts2010.lean +++ b/Studies/Geurts2010.lean @@ -4,9 +4,8 @@ public import Studies.GeurtsPouscoulous2009 public import Linglib.Pragmatics.NeoGricean.Basic public import Linglib.Semantics.Exhaustification.Basic public import Linglib.Data.Examples.Geurts2010 -public import Mathlib.Algebra.Notation.Indicator public import Mathlib.Order.Atoms -public import Mathlib.Order.Minimal +public import Mathlib.Order.Bounds.Defs public import Mathlib.Order.UpperLower.Basic /-! @@ -20,7 +19,7 @@ disjunction](##Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom); under * consistent state](##Sentence.standardRecipe_may_or_eq_empty). Partitioning the speaker's states instead gives [free choice](##Sentence.mem_survivors_may_or_iff) and [form-sensitive scalar inferences](##Sentence.mem_survivors_scalar_iff). Comparing readings for strength [picks out the -upward-entailing scopes](##boundedReading_ssubset_iff), where the experiment finds no upper bound. +upward-entailing scopes](##readings_ssubset_iff), where the experiment finds no upper bound. ## Implementation notes @@ -30,11 +29,11 @@ upward-entailing scopes](##boundedReading_ssubset_iff), where the experiment fin alternative; strengthening wherever it holds is an assumption made here, the book's Recipe being a heuristic. * `Sentence.survivors` applies heuristic (i) categorically, with one alternative per cell and `size` - for economy, so (26b) comes out by length rather than the monolexicality p. 124 credits. + for economy, so (26b) comes out by length rather than the monolexicality p. 124 credits. Heuristic + (ii), which p. 117 invokes, is not formalized. * Upper sets are the closure of the disjuncts under conjunction and disjunction ([each is a union of conjunctions](##eq_iUnion_iInter_of_isUpperSet)). -* The alternatives of (20), p. 120, are reconstructed; (61b, c) are read through the quantifiers of - (62). +* (61b, c) are read through the quantifiers of (62). ## Errata @@ -54,8 +53,8 @@ upward-entailing scopes](##boundedReading_ssubset_iff), where the experiment fin ## TODO -* §8.3 presupposition implicatures, §6.6 open alternatives, and Spector's route (pp. 169–170, - [spector-2006]). +* §8.3 presupposition implicatures, §6.6 open alternatives, Spector's route (pp. 169–170, + [spector-2006]), and the free choice of (20), p. 120, without a modal. * The consistency check against the innocent exclusion of [fox-2007] at (34) and (35). * The experiments of Chapters 4 and 5, for `Data/Statistics`. @@ -81,19 +80,6 @@ variable {W : Type*} {s φ ψ : Set W} /-! ### The Standard Recipe -/ -/-- Soames's Competence⁺ (12), p. 37: the speaker's beliefs agree with the facts at `w`. -/ -def CompetentPlus (w : W) (s ψ : Set W) : Prop := (w ∈ ψ → s ⊆ ψ) ∧ (w ∉ ψ → s ⊆ ψᶜ) - --- p. 38 -theorem CompetentPlus.mem_polar {w : W} (h : CompetentPlus w s ψ) : s ∈ polar ψ := - Question.mem_polar.2 ((em (w ∈ ψ)).imp h.1 h.2) - --- p. 38, Travis, who has an opinion on everything regardless of the facts -theorem not_competentPlus_of_subset {w : W} (hs : s.Nonempty) (hw : w ∉ ψ) (h : s ⊆ ψ) : - ¬ CompetentPlus w s ψ := fun hc ↦ - let ⟨_, hv⟩ := hs - hc.2 hw hv (h hv) - -- the diagram of p. 39: non-belief is disbelief or no opinion, no opinion being non-competence theorem compl_Iic_eq_union (ψ : Set W) : (Iic ψ)ᶜ = (Iic ψᶜ \ {∅}) ∪ (polar ψ : Set (Set W))ᶜ := by @@ -120,23 +106,16 @@ theorem notMem_polar_of_subset_union (hq : s ⊆ φ ∪ ψ) (hφ : ¬ s ⊆ φ) let ⟨_, hw, hwφ⟩ := inter_nonempty_of_subset_union hq hψ hc hw hwφ --- p. 120: what is possible and on which the speaker has an opinion, the speaker believes +-- pp. 114, 120: what is possible and on which the speaker has an opinion, the speaker believes theorem subset_of_inter_nonempty_of_mem_polar (hp : (s ∩ ψ).Nonempty) (hc : s ∈ polar ψ) : s ⊆ ψ := (mem_polar.1 hc).resolve_right fun h ↦ let ⟨_, hw, hwψ⟩ := hp; h hw hwψ --- p. 54: the Horn scale (4) makes (10) an alternative to (9), but (9) entails (10), so that the --- weak implicature contradicts Quality -theorem Iic_inter_compl_Iic_eq_empty {ι : Type*} [Preorder ι] {E : Set W → Set W} {a : ι → Set W} - {i j : ι} (hE : Antitone E) (ha : Antitone a) (h : i ≤ j) : - Iic (E (a i)) ∩ (Iic (E (a j)))ᶜ = ∅ := - eq_empty_of_forall_notMem fun _ hs ↦ hs.2 (subset_trans hs.1 (hE (ha h))) - /-! ### Long disjunctions -The worlds of (29) are ordered by what they make true. A world with `⊥` below it is one in which no -disjunct holds, so the long disjunction (31) is `Ioi ⊥`; the conjunction of the disjuncts below `x` -is `Ici x`, and a world in which just one disjunct holds is an atom. -/ +The worlds of (29), p. 61, are ordered by what they make true. A world with `⊥` below it is one in +which no disjunct holds, so the long disjunction (31) is `Ioi ⊥`; the conjunction of the disjuncts +below `x` is `Ici x`, and a world in which just one disjunct holds is an atom. -/ section LongDisjunction @@ -164,38 +143,14 @@ theorem isSecondaryImplicature_Ici (ha : IsAtom a) (hb : IsAtom b) (hc : IsAtom have hxc : x = c := (hc.le_iff_eq hx).1 (hsub ⟨hc.bot_lt, notMem_Ici_of_isAtom hc ha.1 hac⟩) exact hbc (hxb.symm.trans hxc) --- (32), p. 62: over the alternatives of the parse (A ∨ B) ∨ C, the strong implicature of (32b) --- goes through, which rules out the world in which only C holds -theorem isSecondaryImplicature_parse (ha : IsAtom a) (hb : IsAtom b) (hc : IsAtom c) (hab : a ≠ b) - (hac : a ≠ c) : - IsSecondaryImplicature (Ioi ⊥) - {(Ici a ∪ Ici b) ∩ Ici c, (Ici a ∩ Ici b) ∪ Ici c, Ici a ∩ Ici b ∩ Ici c} - ((Ici a ∩ Ici b) ∪ Ici c) := by - have hb' : a ∉ Ici b := notMem_Ici_of_isAtom ha hb.1 hab.symm - have hc' : a ∉ Ici c := notMem_Ici_of_isAtom ha hc.1 hac.symm - have hψ : a ∉ (Ici a ∩ Ici b) ∪ Ici c := by rintro (h | h); exacts [hb' h.2, hc' h] - refine isSecondaryImplicature_iff.2 ⟨by simp, ⟨?_, fun h ↦ hψ (h ha.bot_lt)⟩, ?_⟩ - · rintro y (h | h) - exacts [ha.bot_lt.trans_le h.1, hc.bot_lt.trans_le h] - · have hsdiff : a ∈ Ioi ⊥ \ ((Ici a ∩ Ici b) ∪ Ici c) := ⟨ha.bot_lt, hψ⟩ - rintro χ (rfl | rfl | rfl) - h - exacts [hc' (h hsdiff).2, hψ (h hsdiff), hc' (h hsdiff).2] - --- pp. 62–63: the two binary parses each eliminate one column too many -theorem union_sdiff_parse_left (A B C : Set W) : +-- pp. 62–63: the binary parse (32) eliminates one column too many, and (33) symmetrically +theorem union_sdiff_parse (A B C : Set W) : ((A ∪ B) ∪ C) \ (((A ∪ B) ∩ C) ∪ ((A ∩ B) ∪ C) ∪ (A ∩ B ∩ C)) = ((A ∪ B) \ (A ∩ B)) \ C := by ext w simp only [mem_sdiff, mem_union, mem_inter_iff] tauto -theorem union_sdiff_parse_right (A B C : Set W) : - (A ∪ (B ∪ C)) \ ((A ∪ (B ∩ C)) ∪ (A ∩ (B ∪ C)) ∪ (A ∩ (B ∩ C))) = - ((B ∪ C) \ (B ∩ C)) \ A := by - ext w - simp only [mem_sdiff, mem_union, mem_inter_iff] - tauto - -- contra p. 64: over the closure the text rejects, the weak implicatures give ignorance about every -- disjunct theorem notMem_polar_Ici_of_mem_primaryImplicatures (ha : IsAtom a) (hb : IsAtom b) (hab : a ≠ b) @@ -215,15 +170,6 @@ theorem eq_iUnion_iInter_of_isUpperSet {κ : Type*} {u : Set (Set κ)} (hu : IsU simp only [mem_iUnion, mem_iInter, mem_Ici, singleton_subset_iff, exists_prop] exact ⟨fun hw ↦ ⟨w, hw, fun _ h ↦ h⟩, fun ⟨x, hx, h⟩ ↦ hu (fun i hi ↦ h i hi) hx⟩ --- p. 61: the only alternative (30) of the substitution method leaves worlds with two disjuncts -example : ({0, 1} : Set (Fin 3)) ∈ Ioi ⊥ \ Ici ⊤ ∧ ¬ IsAtom ({0, 1} : Set (Fin 3)) := by - refine ⟨⟨bot_lt_iff_ne_bot.2 (insert_nonempty _ _).ne_empty, fun h ↦ ?_⟩, fun h ↦ ?_⟩ - · simpa using h (mem_univ (2 : Fin 3)) - · obtain ⟨i, hi⟩ := Set.isAtom_iff.1 h - have h0 : (0 : Fin 3) ∈ ({i} : Set (Fin 3)) := hi ▸ (by simp) - have h1 : (1 : Fin 3) ∈ ({i} : Set (Fin 3)) := hi ▸ (by simp) - exact absurd (subsingleton_singleton h0 h1) (by decide) - variable [IsAtomic α] private theorem exists_isAtom_le {y : α} (hy : y ∈ Ioi ⊥) : ∃ b, IsAtom b ∧ b ≤ y := @@ -268,13 +214,6 @@ theorem setOf_isAtom_mem_primaryImplicatures : mem_primaryImplicatures.2 fun _ hχ hχφ hsub ↦ hχφ.2 (Ioi_bot_subset_of_forall_isAtom_mem hχ fun _ hb ↦ hsub hb) --- p. 41: that the speaker cannot believe all the disjuncts false holds at any length -theorem eq_empty_of_forall_subset_compl_Ici {s : Set α} (hq : s ⊆ Ioi ⊥) - (h : ∀ a, IsAtom a → s ⊆ (Ici a)ᶜ) : s = ∅ := - eq_empty_of_forall_notMem fun _ hy ↦ - let ⟨_, hb, hby⟩ := exists_isAtom_le (hq hy) - h _ hb hy hby - example : Ioi ⊥ \ ⋃₀ {t | IsSecondaryImplicature (Ioi ⊥) {χ | IsUpperSet χ} t} = {w : Set (Fin 3) | ∃ i, w = {i}} := by rw [Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom] @@ -324,6 +263,10 @@ def Poss (V : P → Set W) (s : Set W) (x : Sentence P) : Prop := (s ∩ x.eval /-- The sentence `x` entails the sentence `y`. -/ def Entails (V : P → Set W) (x y : Sentence P) : Prop := ∀ s, x.Believes V s → y.Believes V s +theorem poss_of_believes (hs : s.Nonempty) (h : x.Believes V s) : x.Poss V s := + let ⟨w, hw⟩ := hs + ⟨w, hw, h hw⟩ + theorem believes_may (hs : s.Nonempty) : (may x).Believes V s ↔ x.Poss V s := ⟨fun h ↦ let ⟨_, hw⟩ := hs; h hw, fun h _ _ ↦ h⟩ @@ -371,270 +314,132 @@ theorem standardRecipe_may_or_eq_empty (p q : P) : · exact ha _ (by simp) ((believes_may hs).2 h) · exact ha _ (by simp) ((believes_may hs).2 h) -open Classical in -/-- The sentence a speaker in state `s` could have used to express what the speaker considers -possible, among `x` and `y`: `c` in cell $i_1$, where both are, `a` in $i_2$, where only `x` is, and -`b` in $i_3$, where only `y` is. Cell $i_4$, where neither is, falls with $i_3$; the examples -discard it by Quality or consistency. -/ -noncomputable def say (V : P → Set W) (x y a b c : Sentence P) (s : Set W) : Sentence P := - if x.Poss V s then (if y.Poss V s then c else a) else b - -theorem say_of_poss (hx : x.Poss V s) (hy : y.Poss V s) : say V x y a b c s = c := by - simp [say, hx, hy] - -theorem say_rec {C : Sentence P → Prop} (hc : x.Poss V s → y.Poss V s → C c) - (ha : x.Poss V s → ¬ y.Poss V s → C a) (hb : ¬ x.Poss V s → C b) : - C (say V x y a b c s) := by - unfold say - split_ifs with h h' - exacts [hc h h', ha h h', hb h] - -/-- The alternatives of pp. 115–116: what a consistent speaker of `u` would say is something the -speaker believes and which entails `u`. -/ -def AreAlternatives (V : P → Set W) (u : Sentence P) (say : Set W → Sentence P) : Prop := - ∀ s, s.Nonempty → u.Believes V s → (say s).Believes V s ∧ (say s).Entails V u +/-- The partition of pp. 113–117 by what the speaker considers possible among `x` and `y`, with the +sentence that expresses each cell: `c` for $i_1$, where both are, `a` for $i_2$, where only `x` is, +and `b` for $i_3$, where only `y` is. -/ +abbrev cells (V : P → Set W) (x y a b c : Sentence P) : List (Set (Set W) × Sentence P) := + [({s | x.Poss V s ∧ y.Poss V s}, c), ({s | x.Poss V s ∧ ¬ y.Poss V s}, a), + ({s | ¬ x.Poss V s ∧ y.Poss V s}, b)] + +/-- The alternatives of pp. 115–116: in its cell, a consistent speaker of `u` believes the sentence, +and the sentence entails `u`. -/ +def AreAlternatives (V : P → Set W) (u : Sentence P) (alts : List (Set (Set W) × Sentence P)) : + Prop := + ∀ c ∈ alts, ∀ s ∈ c.1, s.Nonempty → u.Believes V s → c.2.Believes V s ∧ c.2.Entails V u variable {κ : Type*} [Preorder κ] {cost : Sentence P → κ} /-- The alternative heuristic (i): the consistent states that believe the sentence uttered and -could not have expressed which cell they are in by a sentence at most as complex. The partition is -the fibres of `say`, and `cost` ranks sentences, lower meaning more available. -/ +could not have expressed their cell by a sentence at most as complex, lower `cost` meaning more +available. -/ def survivors (V : P → Set W) (cost : Sentence P → κ) (u : Sentence P) - (say : Set W → Sentence P) : Set (Set W) := - {s | s.Nonempty ∧ u.Believes V s ∧ ¬ cost (say s) ≤ cost u} + (alts : List (Set (Set W) × Sentence P)) : Set (Set W) := + {s | s.Nonempty ∧ u.Believes V s ∧ ∀ c ∈ alts, s ∈ c.1 → ¬ cost c.2 ≤ cost u} -theorem mem_survivors_say_iff (ha : cost a ≤ cost u) (hb : cost b ≤ cost u) - (hc : ¬ cost c ≤ cost u) : - s ∈ survivors V cost u (say V x y a b c) ↔ +-- `i₂` and `i₃` go by the heuristic, and `i₄` by Quality +theorem mem_survivors_cells_iff (ha : cost a ≤ cost u) (hb : cost b ≤ cost u) + (hc : ¬ cost c ≤ cost u) (hq : ∀ s, s.Nonempty → u.Believes V s → x.Poss V s ∨ y.Poss V s) : + s ∈ survivors V cost u (cells V x y a b c) ↔ s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ y.Poss V s := by - simp only [survivors, mem_ofPred_eq, say] - split_ifs <;> simp_all - --- the alternative heuristic (ii), p. 116: where the alternative of cell `i₁` is the hardest to --- express, the most likely states are those of `i₁` -theorem maximalFor_say_iff {Q : Set W → Prop} (ha : cost a < cost c) (hb : cost b < cost c) - {s₀ : Set W} (h₀ : Q s₀) (hx₀ : x.Poss V s₀) (hy₀ : y.Poss V s₀) : - MaximalFor Q (fun s ↦ cost (say V x y a b c s)) s ↔ Q s ∧ x.Poss V s ∧ y.Poss V s := by - have hle : ∀ t, cost (say V x y a b c t) ≤ cost c := fun _ ↦ - say_rec (C := fun r ↦ cost r ≤ cost c) (fun _ _ ↦ le_rfl) (fun _ _ ↦ ha.le) fun _ ↦ hb.le - refine ⟨fun h ↦ ⟨h.1, ?_⟩, fun ⟨hs, hx, hy⟩ ↦ ⟨hs, fun t _ _ ↦ ?_⟩⟩ - · have hge : cost c ≤ cost (say V x y a b c s) := by - simpa only [say_of_poss hx₀ hy₀] using - h.2 h₀ (by simpa only [say_of_poss hx₀ hy₀] using hle s) - by_contra hn - have hlt : cost (say V x y a b c s) < cost c := - say_rec (C := fun r ↦ cost r < cost c) (fun h1 h2 ↦ absurd ⟨h1, h2⟩ hn) (fun _ _ ↦ ha) - fun _ ↦ hb - exact hlt.not_ge hge - · simpa only [say_of_poss hx hy] using hle t - -/-- The partition of (15) and (20): `c` says that `x` and `y` are possible, on top of `u`. -/ -noncomputable abbrev sayEither (V : P → Set W) (x y a b u : Sentence P) : Set W → Sentence P := - say V x y a b (and (may x) (and (may y) u)) - -theorem mem_survivors_sayEither_iff (ha : a.size ≤ u.size) (hb : b.size ≤ u.size) : - s ∈ survivors V size u (sayEither V x y a b u) ↔ - s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ y.Poss V s := - mem_survivors_say_iff ha hb (by simp only [size]; omega) - -private theorem believes_entails_top (hs : s.Nonempty) (hu : u.Believes V s) (hx : x.Poss V s) - (hy : y.Poss V s) : - (and (may x) (and (may y) u)).Believes V s ∧ (and (may x) (and (may y) u)).Entails V u := - ⟨believes_and.2 ⟨(believes_may hs).2 hx, believes_and.2 ⟨(believes_may hs).2 hy, hu⟩⟩, - fun _ h ↦ (believes_and.1 (believes_and.1 h).2).2⟩ + simp only [survivors, mem_ofPred_eq, List.forall_mem_cons, List.not_mem_nil, false_implies, + implies_true, and_true] + refine and_congr_right fun hs ↦ and_congr_right fun hu ↦ ⟨fun ⟨_, h2, h3⟩ ↦ ?_, + fun ⟨hx, hy⟩ ↦ ⟨fun _ ↦ hc, fun h ↦ absurd hy h.2, fun h ↦ absurd hx h.1⟩⟩ + rcases hq s hs hu with hx | hy + · exact ⟨hx, by_contra fun hy ↦ h2 ⟨hx, hy⟩ ha⟩ + · exact ⟨by_contra fun hx ↦ h3 ⟨hx, hy⟩ hb, hy⟩ /-- (15), p. 115: *George is British or Canadian*, with the alternatives (16). -/ -noncomputable abbrev sayOr (V : P → Set W) (p q : P) : Set W → Sentence P := - sayEither V (atom p) (atom q) (atom p) (atom q) (or (atom p) (atom q)) +abbrev altsOr (V : P → Set W) (p q : P) : List (Set (Set W) × Sentence P) := + cells V (atom p) (atom q) (atom p) (atom q) + (and (may (atom p)) (and (may (atom q)) (or (atom p) (atom q)))) /-- (17), p. 117: *George may be British or Canadian*, with the alternatives (18). For the performative (19), p. 118, a state is what the speaker permits. -/ -noncomputable abbrev sayMayOr (V : P → Set W) (p q : P) : Set W → Sentence P := - say V (atom p) (atom q) (may (atom p)) (may (atom q)) (and (may (atom p)) (may (atom q))) +abbrev altsMayOr (V : P → Set W) (p q : P) : List (Set (Set W) × Sentence P) := + cells V (atom p) (atom q) (may (atom p)) (may (atom q)) (and (may (atom p)) (may (atom q))) + +/-- (13), p. 112: *many of the nurses were drunk*, with the alternatives (14), p. 113: `x` in the +cell of believing `x`, `u` and not `x` in that of believing its negation, and `u` and maybe `x` in +that of no opinion. The three-way partition of p. 113 is the partition by what is possible, among +`x` and its negation, since only the inconsistent state considers neither possible. The last two +alternatives have the same size, as p. 122 says of (22). -/ +abbrev altsScalar (V : P → Set W) (u x : Sentence P) : List (Set (Set W) × Sentence P) := + cells V x (neg x) x (and u (neg x)) (and u (may x)) + +example : AreAlternatives V (or (atom p) (atom q)) (altsOr V p q) := by + simp only [AreAlternatives, List.forall_mem_cons, List.not_mem_nil, false_implies, implies_true, + and_true] + refine ⟨fun s ⟨hp, hq⟩ hs h ↦ ⟨believes_and.2 ⟨(believes_may hs).2 hp, + believes_and.2 ⟨(believes_may hs).2 hq, h⟩⟩, + fun _ h' ↦ (believes_and.1 (believes_and.1 h').2).2⟩, + fun s ⟨_, hq⟩ _ h ↦ ⟨fun w hw ↦ (h hw).resolve_right fun hwq ↦ hq ⟨w, hw, hwq⟩, + fun _ h' _ hw ↦ .inl (h' hw)⟩, + fun s ⟨hp, _⟩ _ h ↦ ⟨fun w hw ↦ (h hw).resolve_left fun hwp ↦ hp ⟨w, hw, hwp⟩, + fun _ h' _ hw ↦ .inr (h' hw)⟩⟩ + +example : AreAlternatives V (may (or (atom p) (atom q))) (altsMayOr V p q) := by + have key {r : P} (hr : V r ⊆ V p ∪ V q) : (may (atom r)).Entails V (may (or (atom p) (atom q))) := + fun _ h _ hw ↦ (h hw).mono (inter_subset_inter_right _ hr) + simp only [AreAlternatives, List.forall_mem_cons, List.not_mem_nil, false_implies, implies_true, + and_true] + exact ⟨fun s ⟨hp, hq⟩ hs _ ↦ ⟨believes_and.2 ⟨(believes_may hs).2 hp, (believes_may hs).2 hq⟩, + fun t h ↦ key subset_union_left t (believes_and.1 h).1⟩, + fun s ⟨hp, _⟩ hs _ ↦ ⟨(believes_may hs).2 hp, key subset_union_left⟩, + fun s ⟨_, hq⟩ hs _ ↦ ⟨(believes_may hs).2 hq, key subset_union_right⟩⟩ + +example (hx : x.Entails V u) : AreAlternatives V u (altsScalar V u x) := by + simp only [AreAlternatives, List.forall_mem_cons, List.not_mem_nil, false_implies, implies_true, + and_true] + exact ⟨fun s ⟨hp, _⟩ hs h ↦ ⟨believes_and.2 ⟨h, (believes_may hs).2 hp⟩, + fun _ h' ↦ (believes_and.1 h').1⟩, + fun s ⟨_, hn⟩ _ _ ↦ ⟨not_poss_neg.1 hn, hx⟩, + fun s ⟨hp, _⟩ _ h ↦ ⟨believes_and.2 ⟨h, believes_neg.2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩⟩ -- p. 115: the speaker of (15) considers both disjuncts possible theorem mem_survivors_or_iff : - s ∈ survivors V size (or (atom p) (atom q)) (sayOr V p q) ↔ + s ∈ survivors V size (or (atom p) (atom q)) (altsOr V p q) ↔ s.Nonempty ∧ s ⊆ V p ∪ V q ∧ (atom p).Poss V s ∧ (atom q).Poss V s := - mem_survivors_sayEither_iff (by simp [size]) (by simp [size]) - --- p. 115: (16) are alternatives in the sense of the method -example : AreAlternatives V (or (atom p) (atom q)) (sayOr V p q) := - fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V (or (atom p) (atom q))) - (believes_entails_top hs h) - (fun _ hq ↦ ⟨fun w hw ↦ (h hw).resolve_right fun hwq ↦ hq ⟨w, hw, hwq⟩, - fun _ h' _ hw ↦ .inl (h' hw)⟩) - fun hp ↦ ⟨fun w hw ↦ (h hw).resolve_left fun hwp ↦ hp ⟨w, hw, hwp⟩, - fun _ h' _ hw ↦ .inr (h' hw)⟩ + mem_survivors_cells_iff (by simp [size]) (by simp [size]) (by simp [size]) + fun _ hs hu ↦ poss_or.1 (poss_of_believes hs hu) /-- Free choice: of the speakers of *George may be British or Canadian*, those that survive the -alternative heuristic are just the consistent ones that consider each disjunct possible. -/ +alternative heuristic are just the consistent ones that believe *may* of each disjunct, the very +alternatives the Standard Recipe has them not believe. -/ theorem mem_survivors_may_or_iff : - s ∈ survivors V size (may (or (atom p) (atom q))) (sayMayOr V p q) ↔ - s.Nonempty ∧ (atom p).Poss V s ∧ (atom q).Poss V s := by - rw [mem_survivors_say_iff (by simp [size]) (by simp [size]) (by simp [size])] - refine ⟨fun ⟨hs, _, h⟩ ↦ ⟨hs, h⟩, fun ⟨hs, hp, hq⟩ ↦ ⟨hs, ?_, hp, hq⟩⟩ - exact (believes_may hs).2 (poss_or.2 (.inl hp)) - --- p. 117: (18) are alternatives in the sense of the method -example : AreAlternatives V (may (or (atom p) (atom q))) (sayMayOr V p q) := fun s hs h ↦ by - have key {r : P} (hr : V r ⊆ V p ∪ V q) : (may (atom r)).Entails V (may (or (atom p) (atom q))) := - fun _ h' _ hw ↦ (h' hw).mono (inter_subset_inter_right _ hr) - refine say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V (may (or (atom p) (atom q)))) - (fun hp hq ↦ ⟨believes_and.2 ⟨(believes_may hs).2 hp, (believes_may hs).2 hq⟩, - fun t h' ↦ key subset_union_left t (believes_and.1 h').1⟩) - (fun hp _ ↦ ⟨(believes_may hs).2 hp, key subset_union_left⟩) fun hp ↦ ?_ - rcases poss_or.1 ((believes_may hs).1 h) with h' | h' - · exact absurd h' hp - · exact ⟨(believes_may hs).2 h', key subset_union_right⟩ - --- p. 118: the survivors believe the very alternative the Standard Recipe has them not believe -theorem believes_of_mem_survivors_may_or - (h : s ∈ survivors V size (may (or (atom p) (atom q))) (sayMayOr V p q)) : - (may (atom p)).Believes V s ∧ (may (atom q)).Believes V s := - have ⟨hs, hp, hq⟩ := mem_survivors_may_or_iff.1 h - ⟨(believes_may hs).2 hp, (believes_may hs).2 hq⟩ - --- p. 117 applies the heuristic (ii) to (17), and p. 119 reasons by (i) for (19): both single out --- `i₁` -theorem maximalFor_sayMayOr_iff (hp : (V p).Nonempty) (hq : (V q).Nonempty) : - MaximalFor (fun s : Set W ↦ s.Nonempty ∧ (may (or (atom p) (atom q))).Believes V s) - (fun s ↦ (sayMayOr V p q s).size) s ↔ - (s.Nonempty ∧ (may (or (atom p) (atom q))).Believes V s) ∧ - (atom p).Poss V s ∧ (atom q).Poss V s := by - obtain ⟨w, hw⟩ := hp - obtain ⟨v, hv⟩ := hq - exact maximalFor_say_iff (by simp [size]) (by simp [size]) (s₀ := V p ∪ V q) - ⟨⟨w, .inl hw⟩, fun _ _ ↦ ⟨w, .inl hw, .inl hw⟩⟩ ⟨w, .inl hw, hw⟩ ⟨v, .inr hv, hv⟩ - --- pp. 119–120: free choice reports, where `V` gives the restaurant's permissions: with Competence --- for each proposition at issue the weak inferences become beliefs -theorem subset_of_mem_survivors_or - (h : s ∈ survivors V size (or (atom p) (atom q)) (sayOr V p q)) (hp : s ∈ polar (V p)) - (hq : s ∈ polar (V q)) : s ⊆ V p ∧ s ⊆ V q := - have ⟨_, _, hpp, hpq⟩ := mem_survivors_or_iff.1 h - ⟨subset_of_inter_nonempty_of_mem_polar hpp hp, subset_of_inter_nonempty_of_mem_polar hpq hq⟩ - -/-- (13), p. 112: *many of the nurses were drunk*, with the alternatives (14), p. 113: `x` in the -cell of believing `x`, `u` and not `x` in that of believing its negation, and `u` and maybe `x` in -that of no opinion. The three-way partition of p. 113 is the partition by what is possible, among -`x` and its negation, since only the inconsistent state considers neither possible. The last two -alternatives have the same size, as p. 122 says of (22). -/ -noncomputable abbrev sayScalar (V : P → Set W) (u x : Sentence P) : Set W → Sentence P := - say V x (neg x) x (and u (neg x)) (and u (may x)) + s ∈ survivors V size (may (or (atom p) (atom q))) (altsMayOr V p q) ↔ + s.Nonempty ∧ (may (atom p)).Believes V s ∧ (may (atom q)).Believes V s := by + rw [mem_survivors_cells_iff (by simp [size]) (by simp [size]) (by simp [size]) + fun _ hs hu ↦ poss_or.1 ((believes_may hs).1 hu)] + refine and_congr_right fun hs ↦ ?_ + simp only [believes_may hs] + exact ⟨fun ⟨_, h⟩ ↦ h, fun h ↦ ⟨poss_or.2 (.inl h.1), h⟩⟩ /-- The alternative heuristic is sensitive to form: a speaker's saying `u` rules out that the speaker believes `x` just when `x` is no more complex than `u`. -/ theorem mem_survivors_scalar_iff : - s ∈ survivors V size u (sayScalar V u x) ↔ + s ∈ survivors V size u (altsScalar V u x) ↔ s.Nonempty ∧ u.Believes V s ∧ (x.size ≤ u.size → ¬ x.Believes V s) := by - simp only [survivors, mem_ofPred_eq, say] - refine and_congr_right fun hs ↦ and_congr_right fun _ ↦ ?_ - rw [← not_poss_neg] - by_cases hp : x.Poss V s <;> by_cases hn : (neg x).Poss V s - · simp [hp, hn, size] - · simp [hp, hn] - · simp [hp, hn, size] - · rw [not_poss_neg] at hn - exact absurd (let ⟨w, hw⟩ := hs; ⟨w, hw, hn hw⟩) hp - --- p. 113: (14) are alternatives in the sense of the method -example (hx : x.Entails V u) : AreAlternatives V u (sayScalar V u x) := - fun s hs h ↦ say_rec (C := fun r ↦ r.Believes V s ∧ r.Entails V u) - (fun hp _ ↦ ⟨believes_and.2 ⟨h, (believes_may hs).2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩) - (fun _ hn ↦ ⟨not_poss_neg.1 hn, hx⟩) - fun hp ↦ ⟨believes_and.2 ⟨h, believes_neg.2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩ - --- p. 114: Competence eliminates the cell of no opinion, which leaves the strong implicature -theorem subset_compl_of_mem_survivors_scalar - (h : s ∈ survivors V size (atom p) (sayScalar V (atom p) (atom q))) (hc : s ∈ polar (V q)) : - s ⊆ (V q)ᶜ := - (Question.mem_polar.1 hc).resolve_left ((mem_survivors_scalar_iff.1 h).2.2 le_rfl) - --- (23), p. 122: with *many though not all* in the discourse (of the interns, in the text), previous --- use lowers that alternative, the state of believing *not all* goes too, and no opinion is left -theorem mem_survivors_indicator_iff (hx : x.size ≤ u.size) : - s ∈ survivors V (({and u (neg x)}ᶜ : Set (Sentence P)).indicator size) u (sayScalar V u x) ↔ - s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ (neg x).Poss V s := by - have hu : u ∈ ({and u (neg x)}ᶜ : Set (Sentence P)) := fun h ↦ by - have := congrArg size (mem_singleton_iff.1 h) - simp only [size] at this - omega - have hc : and u (may x) ∈ ({and u (neg x)}ᶜ : Set (Sentence P)) := fun h ↦ by - simpa using mem_singleton_iff.1 h - refine mem_survivors_say_iff ?_ ?_ ?_ - · rw [indicator_of_mem hu] - by_cases h : x ∈ ({and u (neg x)}ᶜ : Set (Sentence P)) - · rwa [indicator_of_mem h] - · simp [indicator_of_notMem h] - · simp [indicator_of_notMem] - · rw [indicator_of_mem hu, indicator_of_mem hc] - simp only [size] - omega + simp only [survivors, mem_ofPred_eq, List.forall_mem_cons, List.not_mem_nil, false_implies, + implies_true, and_true, not_poss_neg] + refine and_congr_right fun hs ↦ and_congr_right fun _ ↦ + ⟨fun ⟨_, h, _⟩ hle hb ↦ h ⟨poss_of_believes hs hb, hb⟩ hle, fun h ↦ ⟨fun _ ↦ ?_, + fun hb hle ↦ h hle hb.2, fun _ ↦ ?_⟩⟩ <;> simp only [size] <;> omega + +-- (23), p. 122: once previous use makes (22a) as available as what was said, the state of believing +-- *not all* goes too and no opinion is left +theorem mem_survivors_of_available (ha : cost x ≤ cost u) (hb : cost (and u (neg x)) ≤ cost u) + (hc : ¬ cost (and u (may x)) ≤ cost u) : + s ∈ survivors V cost u (altsScalar V u x) ↔ + s.Nonempty ∧ u.Believes V s ∧ x.Poss V s ∧ (neg x).Poss V s := + mem_survivors_cells_iff ha hb hc fun s hs _ ↦ + let ⟨w, hw⟩ := hs + (em (w ∈ x.eval V s)).imp (⟨w, hw, ·⟩) (⟨w, hw, ·⟩) end Sentence open Sentence -section Pizza - -variable {D : Type*} - -/-- The clauses of (20), *many people had pizza or pasta*, and of its alternatives. -/ -inductive PizzaClause where - | manyEither | manyPizza | manyPasta | somePizza | somePasta - -/-- The worlds at which a clause of (20) holds, where `pizza w` and `pasta w` are those who had -pizza and pasta at `w`. -/ -def PizzaClause.val (many : Set D → Prop) (pizza pasta : W → Set D) : PizzaClause → Set W - | manyEither => {w | many (pizza w ∪ pasta w)} - | manyPizza => {w | many (pizza w)} - | manyPasta => {w | many (pasta w)} - | somePizza => {w | (pizza w).Nonempty} - | somePasta => {w | (pasta w).Nonempty} - -variable {many : Set D → Prop} {pizza pasta : W → Set D} - -local notation "V₂₀" => PizzaClause.val many pizza pasta - -/-- Alternatives to (20), reconstructed after (18) for the partition of p. 120 by *some people had -pizza* and *some people had pasta*. -/ -noncomputable abbrev sayMany (many : Set D → Prop) (pizza pasta : W → Set D) : - Set W → Sentence PizzaClause := - sayEither (PizzaClause.val many pizza pasta) (atom .somePizza) (atom .somePasta) (atom .manyPizza) - (atom .manyPasta) (atom .manyEither) - --- (20), p. 120: free choice with no modal -theorem mem_survivors_many_iff : - s ∈ survivors V₂₀ size (atom .manyEither) (sayMany many pizza pasta) ↔ - s.Nonempty ∧ (atom .manyEither).Believes V₂₀ s ∧ (atom .somePizza).Poss V₂₀ s ∧ - (atom .somePasta).Poss V₂₀ s := - mem_survivors_sayEither_iff le_rfl le_rfl - -example (hm : Monotone many) : - AreAlternatives V₂₀ (atom .manyEither) (sayMany many pizza pasta) := fun s hs h ↦ - say_rec (C := fun r ↦ r.Believes V₂₀ s ∧ r.Entails V₂₀ (atom .manyEither)) - (believes_entails_top hs h) - (fun _ hn ↦ ⟨fun w hw ↦ by - have he : pasta w = ∅ := not_nonempty_iff_eq_empty.1 fun hw' ↦ hn ⟨w, hw, hw'⟩ - simpa [eval, PizzaClause.val, he] using h hw, fun _ h' _ hw ↦ hm subset_union_left (h' hw)⟩) - fun hn ↦ ⟨fun w hw ↦ by - have he : pizza w = ∅ := not_nonempty_iff_eq_empty.1 fun hw' ↦ hn ⟨w, hw, hw'⟩ - simpa [eval, PizzaClause.val, he] using h hw, fun _ h' _ hw ↦ hm subset_union_right (h' hw)⟩ - -end Pizza - --- (31), p. 61, with p. 115, extending the text: a speaker who rules out a disjunct could have used --- the shorter disjunction, so the survivors of the heuristic consider every disjunct possible -theorem inter_nonempty_of_forall_not_subset {ι : Type*} {A : ι → Set W} {J : Finset ι} {i : ι} - (hq : s ⊆ ⋃ j ∈ J, A j) (h : ∀ J' ⊂ J, ¬ s ⊆ ⋃ j ∈ J', A j) (hi : i ∈ J) : - (s ∩ A i).Nonempty := by - classical - by_contra hne - refine h _ (Finset.erase_ssubset hi) fun w hw ↦ ?_ - obtain ⟨j, hj, hwj⟩ := mem_iUnion₂.1 (hq hw) - exact mem_iUnion₂.2 ⟨j, Finset.mem_erase.2 ⟨fun he ↦ hne ⟨w, hw, he ▸ hwj⟩, hj⟩, hwj⟩ - /-! ### Conventionalism -/ section Conventionalism @@ -643,73 +448,54 @@ open Quantifier Quantifier.Det GeurtsPouscoulous2009 Exhaustification private theorem someNotAllC_subset (R : Situation) : someNotAllC R ⊆ someC R := fun _ h ↦ h.1 -/-- Enhanced lexicalism in its weak version (33) prefers the upper-bounded reading of (62) provided -this strengthens the sentence, which holds just under the upward-entailing quantifiers. -/ -theorem boundedReading_ssubset_iff (q : Quant) : - localReading q ⊂ classicalReading q ↔ PredictsLocalSIWeak (q.sem : Det (Fin 3)) := by - have pos {r : Quant} {t : Trial} (hr : PredictsLocalSIWeak (r.sem : Det (Fin 3))) - (hc : Classical r t) (hl : ¬ Local r t) : - (localReading r ⊂ classicalReading r) ↔ PredictsLocalSIWeak (r.sem : Det (Fin 3)) := - iff_of_true ⟨fun R hR ↦ hr univ (someNotAllC_subset R) hR, fun h ↦ hl (h hc)⟩ hr - have neg {r : Quant} {t : Trial} (hr : ¬ PredictsLocalSIWeak (r.sem : Det (Fin 3))) - (hc : ¬ Classical r t) (hl : Local r t) : - (localReading r ⊂ classicalReading r) ↔ PredictsLocalSIWeak (r.sem : Det (Fin 3)) := - iff_of_false (fun h ↦ hc (h.1 hl)) hr - cases q with - | all => exact pos all_predictsLocalSIWeak classical_all not_local_all - | moreThanOne => - exact pos moreThanOne_predictsLocalSIWeak classical_moreThanOne not_local_moreThanOne - | exactlyTwo => - exact neg exactlyTwo_not_predictsLocalSIWeak not_classical_exactlyTwo_b local_exactlyTwo_b - | notAll => exact neg notAll_not_predictsLocalSIWeak not_classical_notAll local_notAll - | notMoreThanOne => - exact neg notMoreThanOne_not_predictsLocalSIWeak not_classical_notMoreThanOne - local_notMoreThanOne - --- (32), pp. 146–147: the strong version prefers it unless this weakens the sentence, which also --- covers the non-monotone *exactly two* -theorem not_classicalReading_ssubset_iff (q : Quant) : - ¬ classicalReading q ⊂ localReading q ↔ PredictsLocalSI (q.sem : Det (Fin 3)) := by - have anti {r : Quant} (hr : ¬ PredictsLocalSI (r.sem : Det (Fin 3))) {t : Trial} - (hc : ¬ Classical r t) (hl : Local r t) : - (¬ classicalReading r ⊂ localReading r) ↔ PredictsLocalSI (r.sem : Det (Fin 3)) := - iff_of_false (not_not.2 ⟨fun R hR ↦ not_not.1 hr univ (someNotAllC_subset R) hR, - fun h' ↦ hc (h' hl)⟩) hr +/-- Enhanced lexicalism prefers the upper-bounded reading of (62): in its weak version (33) provided +this strengthens the sentence, just under the upward-entailing quantifiers, and in its strong +version (32) unless it weakens the sentence, which adds the non-monotone *exactly two*. -/ +theorem readings_ssubset_iff (q : Quant) : + (localReading q ⊂ classicalReading q ↔ PredictsLocalSIWeak (q.sem : Det (Fin 3))) ∧ + (¬ classicalReading q ⊂ localReading q ↔ PredictsLocalSI (q.sem : Det (Fin 3))) := by + have up {r : Quant} {t : Trial} (hw : PredictsLocalSIWeak (r.sem : Det (Fin 3))) + (hs : PredictsLocalSI (r.sem : Det (Fin 3))) (hc : Classical r t) (hl : ¬ Local r t) : + (localReading r ⊂ classicalReading r ↔ PredictsLocalSIWeak (r.sem : Det (Fin 3))) ∧ + (¬ classicalReading r ⊂ localReading r ↔ PredictsLocalSI (r.sem : Det (Fin 3))) := + ⟨iff_of_true ⟨fun R hR ↦ hw univ (someNotAllC_subset R) hR, fun h ↦ hl (h hc)⟩ hw, + iff_of_true (fun h ↦ hl (h.1 hc)) hs⟩ + have down {r : Quant} {t : Trial} (hw : ¬ PredictsLocalSIWeak (r.sem : Det (Fin 3))) + (hs : ¬ PredictsLocalSI (r.sem : Det (Fin 3))) (hc : ¬ Classical r t) (hl : Local r t) : + (localReading r ⊂ classicalReading r ↔ PredictsLocalSIWeak (r.sem : Det (Fin 3))) ∧ + (¬ classicalReading r ⊂ localReading r ↔ PredictsLocalSI (r.sem : Det (Fin 3))) := + ⟨iff_of_false (fun h ↦ hc (h.1 hl)) hw, iff_of_false (not_not.2 + ⟨fun R hR ↦ not_not.1 hs univ (someNotAllC_subset R) hR, fun h' ↦ hc (h' hl)⟩) hs⟩ cases q with - | all => - exact iff_of_true ((boundedReading_ssubset_iff .all).2 all_predictsLocalSIWeak).not_gt - all_predictsLocalSI + | all => exact up all_predictsLocalSIWeak all_predictsLocalSI classical_all not_local_all | moreThanOne => - exact iff_of_true - ((boundedReading_ssubset_iff .moreThanOne).2 moreThanOne_predictsLocalSIWeak).not_gt - moreThanOne_predictsLocalSI + exact up moreThanOne_predictsLocalSIWeak moreThanOne_predictsLocalSI classical_moreThanOne + not_local_moreThanOne | exactlyTwo => - exact iff_of_true (fun h ↦ not_local_exactlyTwo_a (h.1 classical_exactlyTwo_a)) - exactlyTwo_predictsLocalSI - | notAll => exact anti notAll_not_predictsLocalSI not_classical_notAll local_notAll + exact ⟨iff_of_false (fun h ↦ not_classical_exactlyTwo_b (h.1 local_exactlyTwo_b)) + exactlyTwo_not_predictsLocalSIWeak, + iff_of_true (fun h ↦ not_local_exactlyTwo_a (h.1 classical_exactlyTwo_a)) + exactlyTwo_predictsLocalSI⟩ + | notAll => + exact down notAll_not_predictsLocalSIWeak notAll_not_predictsLocalSI not_classical_notAll + local_notAll | notMoreThanOne => - exact anti notMoreThanOne_not_predictsLocalSI not_classical_notMoreThanOne - local_notMoreThanOne - --- p. 159: of the squares of Figure 1, one is connected to all the circles -theorem existsUnique_figure2 : ∃! s : Fin 3, ∀ c, figure2 s c := - ⟨0, fun _ ↦ .inl rfl, by decide⟩ + exact down notMoreThanOne_not_predictsLocalSIWeak notMoreThanOne_not_predictsLocalSI + not_classical_notMoreThanOne local_notMoreThanOne variable {some many all : Set W} --- (39)–(40): `exh` is the operator O of (39); O (44b), the parse under negation (42c) +-- (39)–(40), p. 148: `exh` is the operator O of (39); O (44b), the parse under negation (42c) theorem exh_many (hs : many ⊆ some) (ha : all ⊂ many) : - exh {some, many, all} many = many \ all := - exh_eq_sdiff_of_forall (by simp) ha.2 (by - rintro r (rfl | rfl | rfl) - exacts [.inl hs, .inl subset_rfl, .inr subset_rfl]) + exh {some, many, all} many = many \ all := by + rw [exh_insert_of_subset hs, exh_insert_of_subset subset_rfl, exh_singleton_of_not_subset ha.2] --- (43): O (43b), the parse (42b) +-- (43), p. 149: O (43b), the parse (42b) theorem exh_compl_many (hs : many ⊂ some) (ha : all ⊆ many) : exh {someᶜ, manyᶜ, allᶜ} manyᶜ = manyᶜ ∩ some := by - rw [exh_eq_sdiff_of_forall (q := someᶜ) (by simp) (fun h ↦ hs.2 (compl_subset_compl.1 h)) (by - rintro r (rfl | rfl | rfl) - exacts [.inr subset_rfl, .inl subset_rfl, .inl (compl_subset_compl.2 ha)]), sdiff_compl] + rw [exh_insert_of_not_subset fun h ↦ hs.2 (compl_subset_compl.1 h), + exh_insert_of_subset subset_rfl, exh_singleton_of_subset (compl_subset_compl.2 ha), + sdiff_compl] -- (47), p. 150: the Power Principle prefers (42b) to the readings (42a) and (42c) theorem isLeast_readings_negation (hs : many ⊂ some) (ha : all ⊂ many) : @@ -729,7 +515,7 @@ theorem isLeast_readings_core (R : SetRel W W) [ModalLogic.IsSerial R] (ha : all IsLeast {R.core some, exh {R.core some, R.core all} (R.core some), R.core (exh {some, all} some)} (R.core (exh {some, all} some)) := by have hcore : R.core (some \ all) ⊆ R.core some := fun _ hw _ hv ↦ (hw hv).1 - rw [exh_pair ha.2] + rw [exh_insert_of_subset (p := some) subset_rfl, exh_singleton_of_not_subset ha.2] refine ⟨by simp, ?_⟩ rintro _ (rfl | rfl | rfl) · exact hcore @@ -751,8 +537,7 @@ theorem compl_sdiff_like {like love : Set W} (h : love ⊆ like) : theorem exh_rich {rich rich₂ : Set W} (h : rich₂ ⊆ rich) (hne : rich₂.Nonempty) : exh {rich \ rich₂} rich = rich₂ := by obtain ⟨v, hv⟩ := hne - rw [exh_eq_sdiff_of_forall (mem_singleton _) (fun hs ↦ (hs (h hv)).2 hv) - (by rintro r rfl; exact .inr subset_rfl), sdiff_sdiff_eq_self h] + rw [exh_singleton_of_not_subset fun hs ↦ (hs (h hv)).2 hv, sdiff_sdiff_eq_self h] end Conventionalism @@ -762,7 +547,7 @@ section Embedded variable {M A F : Set W} --- §8.1, (6)–(8): the implicature *not all the figs* passes the consistency check +-- §8.1, (6)–(8), pp. 166–167: the implicature *not all the figs* passes the consistency check theorem isSecondaryImplicature_mango (hA : A ⊆ F) (hM : (M \ F).Nonempty) (hF : (F \ (M ∪ A)).Nonempty) : IsSecondaryImplicature (M ∪ F) {M, F, A, M ∪ A} A := by obtain ⟨f, hf, hfn⟩ := hF @@ -804,18 +589,11 @@ theorem subset_core_exh {R : SetRel W W} {some all : Set W} (hall : all ⊂ some -- (10)–(12) and, for *hope*, (15)–(17), pp. 170–171, share this form, for any attitude: what -- separates them is the plausibility of the second premise. (11) and (16), as printed, have the --- disjunction outside the speaker's belief; given the first premise that says the same, and without --- it it is strictly stronger +-- disjunction outside the speaker's belief; given the first premise that says the same theorem subset_or_subset_iff {X Y : Set W} (h10 : s ⊆ Xᶜ) : (s ⊆ X ∨ s ⊆ Y) ↔ s ⊆ X ∪ Y := ⟨fun h ↦ h.elim (·.trans subset_union_left) (·.trans subset_union_right), fun h ↦ .inr fun _ hw ↦ (h hw).resolve_left (h10 hw)⟩ -example : ∃ (s X Y : Set (Fin 2)), s ⊆ X ∪ Y ∧ ¬ (s ⊆ X ∨ s ⊆ Y) := - ⟨univ, {0}, {0}ᶜ, (union_compl_self _).ge, by - rintro (h | h) - · exact absurd (h (mem_univ 1)) (by simp) - · exact h (mem_univ 0) rfl⟩ - section Indefinites variable {D : Type*} {sailor some all : W → Set D} {t : SetRel W D} @@ -868,7 +646,7 @@ example : Datum.ReadCount Table2Row.ofDatum Examples.all 8 := by decide -- Table 2: the alternatives printed are those of the definition (24) by Horn sets, on which a -- sentence is an alternative iff it is stronger, for any strictly stronger meanings of the four -- quantifiers. The reversal under negation is among sentences; the meanings keep their order, and --- the ordering a Horn scale (4) would impose plays no part (pp. 57–59) +-- the ordering a Horn scale (4), p. 51, would impose plays no part (pp. 57–59) theorem rows_table2 {a : Fin 4 → Set W} (ha : StrictAnti a) : ∀ r ∈ Examples.all.filterMap Table2Row.ofDatum, ∀ k, k ∈ r.alternatives ↔ r.polarity • a k ⊂ r.polarity • a r.quantifier := by @@ -889,20 +667,22 @@ inductive Item where /-- The statement that the theory derives the inference, over any model of the sentence. -/ def Item.Derived : Item → Prop | .disjunct => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V size (or (atom true) (atom false)) (sayOr V true false) → + s ∈ survivors V size (or (atom true) (atom false)) (altsOr V true false) → (atom true).Poss V s ∧ (atom false).Poss V s | .freeChoice => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V size (may (or (atom true) (atom false))) (sayMayOr V true false) → - (atom true).Poss V s ∧ (atom false).Poss V s + s ∈ survivors V size (may (or (atom true) (atom false))) (altsMayOr V true false) → + (may (atom true)).Believes V s ∧ (may (atom false)).Believes V s | .sameLength => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V size (atom true) (sayScalar V (atom true) (atom false)) → + s ∈ survivors V size (atom true) (altsScalar V (atom true) (atom false)) → ¬ (atom false).Believes V s - | .afterUse => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V (({and (atom true) (neg (atom false))}ᶜ : Set (Sentence Bool)).indicator size) - (atom true) (sayScalar V (atom true) (atom false)) → + | .afterUse => ∀ {W : Type} (V : Bool → Set W) (cost : Sentence Bool → ℕ) (s : Set W), + cost (atom false) ≤ cost (atom true) → + cost (and (atom true) (neg (atom false))) ≤ cost (atom true) → + ¬ cost (and (atom true) (may (atom false))) ≤ cost (atom true) → + s ∈ survivors V cost (atom true) (altsScalar V (atom true) (atom false)) → ¬ (atom false).Believes V s ∧ (atom false).Poss V s | .longer => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V size (atom true) (sayScalar V (atom true) (and (atom false) (atom true))) → + s ∈ survivors V size (atom true) (altsScalar V (atom true) (and (atom false) (atom true))) → ¬ (and (atom false) (atom true)).Believes V s | .figs => ∀ {W : Type} (M F A : Set W), A ⊆ F → (M \ F).Nonempty → (F \ (M ∪ A)).Nonempty → IsSecondaryImplicature (M ∪ F) {M, F, A, M ∪ A} A @@ -941,10 +721,9 @@ theorem Item.derived_iff : ∀ i : Item, i.Derived ↔ i ∉ [Item.longer, .mang | .disjunct => iff_of_true (fun _ _ h ↦ (mem_survivors_or_iff.1 h).2.2) (by decide) | .freeChoice => iff_of_true (fun _ _ h ↦ (mem_survivors_may_or_iff.1 h).2) (by decide) | .sameLength => iff_of_true (fun _ _ h ↦ (mem_survivors_scalar_iff.1 h).2.2 le_rfl) (by decide) - | .afterUse => iff_of_true (fun _ _ h ↦ by - obtain ⟨_, _, hp, hn⟩ := - (mem_survivors_indicator_iff (x := atom false) (u := atom true) le_rfl).1 h - exact ⟨poss_neg.1 hn, hp⟩) (by decide) + | .afterUse => iff_of_true (fun _ _ _ ha hb hc h ↦ + have ⟨_, _, hp, hn⟩ := (mem_survivors_of_available ha hb hc).1 h + ⟨poss_neg.1 hn, hp⟩) (by decide) | .longer => iff_of_false Item.not_derived_longer (by decide) | .figs => iff_of_true (fun _ _ _ ↦ isSecondaryImplicature_mango) (by decide) | .mango => iff_of_false Item.not_derived_mango (by decide) @@ -980,7 +759,8 @@ example : Datum.ReadCount quantifierRow? Examples.all 3 := by decide -- none of these inferences goes through theorem rows_61 : ∀ r ∈ Examples.all.filterMap quantifierRow?, ¬ classicalReading r.1 ⊂ localReading r.1 ∧ r.2 = false := by - simp only [not_classicalReading_ssubset_iff, Quant.predictsLocalSI_iff] + have h (q : Quant) := (readings_ssubset_iff q).2 + simp only [h, Quant.predictsLocalSI_iff] decide /-- Reads whether the inference of a row of (56) is conveyed. -/ diff --git a/Studies/GeurtsPouscoulous2009.lean b/Studies/GeurtsPouscoulous2009.lean index d9f0bcb526..ccb89a218a 100644 --- a/Studies/GeurtsPouscoulous2009.lean +++ b/Studies/GeurtsPouscoulous2009.lean @@ -64,7 +64,7 @@ variable {W : Type*} theorem local_reading (R : SetRel W W) {some all : Set W} (h : all ⊂ some) : R.core (exh {some, all} some) = R.core some ∩ R.core allᶜ := by - rw [exh_pair h.2, Set.sdiff_eq, core_inter] + rw [exh_insert_of_subset subset_rfl, exh_singleton_of_not_subset h.2, Set.sdiff_eq, core_inter] theorem local_of_global_of_opinionated (R : SetRel W W) {some all : Set W} (h : all ⊂ some) {w : W} (h₃₁ : w ∈ R.core some) (h₃₂ : w ∉ R.core all) @@ -142,6 +142,8 @@ abbrev Situation := Fin 3 → Fin 3 → Prop and each of the others with two of them. -/ abbrev figure2 : Situation := fun s c ↦ s = 0 ∨ (s = 1 ∧ c ≠ 2) ∨ (s = 2 ∧ c ≠ 0) +example : ∃! s : Fin 3, ∀ c, figure2 s c := ⟨0, fun _ ↦ .inl rfl, by decide⟩ + /-- The situation for *more than one* and the two downward-entailing sentences, in which every square is connected with some circle and two of them with all. -/ abbrev allSome : Situation := fun s c ↦ s ≠ 0 ∨ c = 0 From e8412b395be835a4b986557de71114561b7049c0 Mon Sep 17 00:00:00 2001 From: Robert Hawkins Date: Tue, 3 Nov 2026 15:38:25 -0800 Subject: [PATCH 5/5] refactor(Studies/Geurts2010): keep only theorems central to the argument --- Linglib/Data/Examples/Geurts2010.json | 4 - Linglib/Data/Examples/Geurts2010.lean | 8 +- Linglib/Semantics/Exhaustification/Basic.lean | 3 - Studies/Geurts2010.lean | 250 +++--------------- Studies/GeurtsPouscoulous2009.lean | 2 - 5 files changed, 44 insertions(+), 223 deletions(-) diff --git a/Linglib/Data/Examples/Geurts2010.json b/Linglib/Data/Examples/Geurts2010.json index 265be5191e..5109d9e3dd 100644 --- a/Linglib/Data/Examples/Geurts2010.json +++ b/Linglib/Data/Examples/Geurts2010.json @@ -185,7 +185,6 @@ "alternatives": [], "readings": [], "paperFeatures": [ - ["item", "disjunct"], ["inference", "He may be British."], ["conveys", "true"] ], @@ -206,7 +205,6 @@ "alternatives": [], "readings": [], "paperFeatures": [ - ["item", "freeChoice"], ["inference", "He may be British."], ["conveys", "true"] ], @@ -227,7 +225,6 @@ "alternatives": [], "readings": [], "paperFeatures": [ - ["item", "freeChoice"], ["inference", "You can have chocolate cake."], ["conveys", "true"] ], @@ -269,7 +266,6 @@ "alternatives": [], "readings": [], "paperFeatures": [ - ["item", "afterUse"], ["inference", "George doesn't know whether all the nurses were drunk."], ["conveys", "true"] ], diff --git a/Linglib/Data/Examples/Geurts2010.lean b/Linglib/Data/Examples/Geurts2010.lean index 026812a93d..8f336a5749 100644 --- a/Linglib/Data/Examples/Geurts2010.lean +++ b/Linglib/Data/Examples/Geurts2010.lean @@ -139,7 +139,7 @@ def ex_11 : Datum := judgment := .acceptable alternatives := [] readings := [] - paperFeatures := [("item", "disjunct"), ("inference", "He may be British."), ("conveys", "true")] } + paperFeatures := [("inference", "He may be British."), ("conveys", "true")] } def ex_12 : Datum := { id := "geurts2010_12" @@ -153,7 +153,7 @@ def ex_12 : Datum := judgment := .acceptable alternatives := [] readings := [] - paperFeatures := [("item", "freeChoice"), ("inference", "He may be British."), ("conveys", "true")] } + paperFeatures := [("inference", "He may be British."), ("conveys", "true")] } def ex_19 : Datum := { id := "geurts2010_19" @@ -167,7 +167,7 @@ def ex_19 : Datum := judgment := .acceptable alternatives := [] readings := [] - paperFeatures := [("item", "freeChoice"), ("inference", "You can have chocolate cake."), ("conveys", "true")] } + paperFeatures := [("inference", "You can have chocolate cake."), ("conveys", "true")] } def ex_13 : Datum := { id := "geurts2010_13" @@ -195,7 +195,7 @@ def ex_23 : Datum := judgment := .acceptable alternatives := [] readings := [] - paperFeatures := [("item", "afterUse"), ("inference", "George doesn't know whether all the nurses were drunk."), ("conveys", "true")] } + paperFeatures := [("inference", "George doesn't know whether all the nurses were drunk."), ("conveys", "true")] } def ex_26a : Datum := { id := "geurts2010_26a" diff --git a/Linglib/Semantics/Exhaustification/Basic.lean b/Linglib/Semantics/Exhaustification/Basic.lean index d91b8ebb46..ff317859ab 100644 --- a/Linglib/Semantics/Exhaustification/Basic.lean +++ b/Linglib/Semantics/Exhaustification/Basic.lean @@ -126,9 +126,6 @@ theorem exh_insert_of_not_subset (h : ¬ p ⊆ q) : exh (insert q C) p = exh C p fun ⟨⟨hp, hw⟩, hq⟩ ↦ ⟨hp, fun r hr hwr ↦ hr.elim (fun e ↦ absurd (e ▸ hwr) hq) (hw r · hwr)⟩⟩ -theorem exh_singleton_of_subset (h : p ⊆ q) : exh {q} p = p := - exh_eq_self fun _ hr ↦ (Set.mem_singleton_iff.1 hr) ▸ h - theorem exh_singleton_of_not_subset (h : ¬ p ⊆ q) : exh {q} p = p \ q := by rw [← insert_empty_eq, exh_insert_of_not_subset h, exh_empty] diff --git a/Studies/Geurts2010.lean b/Studies/Geurts2010.lean index 200c3c530b..ae8362a864 100644 --- a/Studies/Geurts2010.lean +++ b/Studies/Geurts2010.lean @@ -31,8 +31,8 @@ upward-entailing scopes](##readings_ssubset_iff), where the experiment finds no * `Sentence.survivors` applies heuristic (i) categorically, with one alternative per cell and `size` for economy, so (26b) comes out by length rather than the monolexicality p. 124 credits. Heuristic (ii), which p. 117 invokes, is not formalized. -* Upper sets are the closure of the disjuncts under conjunction and disjunction ([each is a union of - conjunctions](##eq_iUnion_iInter_of_isUpperSet)). +* Upper sets model the closure of the disjuncts under conjunction and disjunction, up to the empty + set and the whole space. * (61b, c) are read through the quantifiers of (62). ## Errata @@ -43,13 +43,12 @@ upward-entailing scopes](##readings_ssubset_iff), where the experiment finds no wherever just one disjunct holds pass](##isSecondaryImplicature_upperSets_iff), and it [gives ignorance](##notMem_polar_Ici_of_mem_primaryImplicatures). * p. 115: "American" for British. -* p. 143: (25) should end [*or we love it*](##compl_sdiff_like). -* p. 149: (42b) is [*some but not many*](##exh_compl_many), not "many but not all". +* p. 143: (25) should end *or we love it*. +* p. 149: (42b) is *some but not many*, as the computation there gives, not "many but not all". * p. 168: (9a) for (9). -* pp. 169–170: (11) and (16) put the disjunction outside the belief, [harmlessly given (10) or - (15)](##subset_or_subset_iff). +* pp. 169–170: (11) and (16) put the disjunction outside the belief, where the prose has it inside. * p. 188: (46) omits *not*. -* p. 189: [O reaches RICH₂ given RICH₁](##exh_rich), so "out of reach" overstates. +* p. 189: O reaches RICH₂ given the alternative RICH₁, so "out of reach" overstates. ## TODO @@ -80,19 +79,6 @@ variable {W : Type*} {s φ ψ : Set W} /-! ### The Standard Recipe -/ --- the diagram of p. 39: non-belief is disbelief or no opinion, no opinion being non-competence -theorem compl_Iic_eq_union (ψ : Set W) : - (Iic ψ)ᶜ = (Iic ψᶜ \ {∅}) ∪ (polar ψ : Set (Set W))ᶜ := by - rw [← compl_Iic_inter_polar] - ext s - simp only [mem_union, mem_inter_iff, mem_compl_iff, mem_Iic, SetLike.mem_coe, mem_polar] - tauto - --- p. 40: (16) and (17) exclude each other, so (16) cannot come from strengthening (17) -theorem disjoint_Iic_compl_polar (ψ : Set W) : - Disjoint (Iic ψᶜ) (polar ψ : Set (Set W))ᶜ := - disjoint_left.2 fun _ h hc ↦ hc (mem_polar.2 (.inr h)) - -- p. 110, footnote 4; p. 167 theorem inter_nonempty_of_subset_union (hq : s ⊆ φ ∪ ψ) (hψ : ¬ s ⊆ ψ) : (s ∩ φ).Nonempty := let ⟨_, hw, hwψ⟩ := not_subset.1 hψ @@ -106,11 +92,6 @@ theorem notMem_polar_of_subset_union (hq : s ⊆ φ ∪ ψ) (hφ : ¬ s ⊆ φ) let ⟨_, hw, hwφ⟩ := inter_nonempty_of_subset_union hq hψ hc hw hwφ --- pp. 114, 120: what is possible and on which the speaker has an opinion, the speaker believes -theorem subset_of_inter_nonempty_of_mem_polar (hp : (s ∩ ψ).Nonempty) (hc : s ∈ polar ψ) : - s ⊆ ψ := - (mem_polar.1 hc).resolve_right fun h ↦ let ⟨_, hw, hwψ⟩ := hp; h hw hwψ - /-! ### Long disjunctions The worlds of (29), p. 61, are ordered by what they make true. A world with `⊥` below it is one in @@ -162,25 +143,11 @@ theorem notMem_polar_Ici_of_mem_primaryImplicatures (ha : IsAtom a) (hb : IsAtom exact hweak _ (isLowerSet_Iic a).compl (compl_Iic_ssubset_Ioi_bot ha) fun y hy hya ↦ hna hy ((ha.le_iff_eq (mem_Ioi.1 (hq hy)).ne').1 hya).ge --- an upper set of the worlds of (29) is a union of conjunctions of disjuncts, so that the upper --- sets are the closure p. 64 considers -theorem eq_iUnion_iInter_of_isUpperSet {κ : Type*} {u : Set (Set κ)} (hu : IsUpperSet u) : - u = ⋃ x ∈ u, ⋂ i ∈ x, Ici ({i} : Set κ) := by - ext w - simp only [mem_iUnion, mem_iInter, mem_Ici, singleton_subset_iff, exists_prop] - exact ⟨fun hw ↦ ⟨w, hw, fun _ h ↦ h⟩, fun ⟨x, hx, h⟩ ↦ hu (fun i hi ↦ h i hi) hx⟩ - variable [IsAtomic α] private theorem exists_isAtom_le {y : α} (hy : y ∈ Ioi ⊥) : ∃ b, IsAtom b ∧ b ≤ y := (eq_bot_or_exists_atom_le y).resolve_left (mem_Ioi.1 hy).ne' --- an upper set with every atom in it holds wherever a disjunct does -private theorem Ioi_bot_subset_of_forall_isAtom_mem {χ : Set α} (hχ : IsUpperSet χ) - (h : ∀ x, IsAtom x → x ∈ χ) : Ioi ⊥ ⊆ χ := fun _ hy ↦ - let ⟨_, hb, hby⟩ := exists_isAtom_le hy - hχ hby (h _ hb) - -- contra p. 64: over alternatives closed under conjunction and disjunction, an alternative passes -- the consistency check just when it holds in no world in which only one disjunct does theorem isSecondaryImplicature_upperSets_iff : @@ -191,7 +158,9 @@ theorem isSecondaryImplicature_upperSets_iff : ⟨fun h x hx hxt ↦ ?_, fun h χ hχ hχφ hsub ↦ ?_⟩ · exact h _ (isLowerSet_Iic x).compl (compl_Iic_ssubset_Ioi_bot hx) fun y hy hle ↦ hy.2 ((hx.le_iff_eq (mem_Ioi.1 hy.1).ne').1 hle ▸ hxt) - · exact hχφ.2 (Ioi_bot_subset_of_forall_isAtom_mem hχ fun b hb ↦ hsub ⟨hb.bot_lt, h b hb⟩) + · exact hχφ.2 fun y hy ↦ + let ⟨b, hb, hby⟩ := exists_isAtom_le hy + hχ hby (hsub ⟨hb.bot_lt, h b hb⟩) /-- Closing the alternatives of a long disjunction under conjunction and under disjunction, and strengthening wherever Competence is consistent, yields exactly the exclusive reading. -/ @@ -207,18 +176,6 @@ theorem Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom : · exact hna (le_antisymm hbx (h hb.bot_lt) ▸ hb) · exact hna ((hy.le_iff_eq hx.ne').1 hxy ▸ hy) --- the exclusive state itself meets the weak implicatures of that closure, so the reading is not --- vacuous -theorem setOf_isAtom_mem_primaryImplicatures : - {x : α | IsAtom x} ∈ primaryImplicatures (Ioi ⊥) {χ | IsUpperSet χ} := - mem_primaryImplicatures.2 fun _ hχ hχφ hsub ↦ - hχφ.2 (Ioi_bot_subset_of_forall_isAtom_mem hχ fun _ hb ↦ hsub hb) - -example : Ioi ⊥ \ ⋃₀ {t | IsSecondaryImplicature (Ioi ⊥) {χ | IsUpperSet χ} t} = - {w : Set (Fin 3) | ∃ i, w = {i}} := by - rw [Ioi_sdiff_sUnion_isSecondaryImplicature_eq_setOf_isAtom] - exact Set.ext fun _ ↦ Set.isAtom_iff - end LongDisjunction /-! ### Intentions first @@ -260,9 +217,6 @@ def Believes (V : P → Set W) (s : Set W) (x : Sentence P) : Prop := s ⊆ x.ev /-- $\mathrm{Poss}_S$: a speaker in state `s` considers what the sentence says possible. -/ def Poss (V : P → Set W) (s : Set W) (x : Sentence P) : Prop := (s ∩ x.eval V s).Nonempty -/-- The sentence `x` entails the sentence `y`. -/ -def Entails (V : P → Set W) (x y : Sentence P) : Prop := ∀ s, x.Believes V s → y.Believes V s - theorem poss_of_believes (hs : s.Nonempty) (h : x.Believes V s) : x.Poss V s := let ⟨w, hw⟩ := hs ⟨w, hw, h hw⟩ @@ -270,12 +224,6 @@ theorem poss_of_believes (hs : s.Nonempty) (h : x.Believes V s) : x.Poss V s := theorem believes_may (hs : s.Nonempty) : (may x).Believes V s ↔ x.Poss V s := ⟨fun h ↦ let ⟨_, hw⟩ := hs; h hw, fun h _ _ ↦ h⟩ -theorem believes_and : (and x y).Believes V s ↔ x.Believes V s ∧ y.Believes V s := - subset_inter_iff - -theorem believes_neg : (neg x).Believes V s ↔ ¬ x.Poss V s := - ⟨fun h ⟨_, hw, hwx⟩ ↦ h hw hwx, fun h w hw hwx ↦ h ⟨w, hw, hwx⟩⟩ - theorem poss_neg : (neg x).Poss V s ↔ ¬ x.Believes V s := by simp [Poss, Believes, eval, inter_compl_nonempty_iff] @@ -289,15 +237,6 @@ sentence uttered and none of the alternatives `alts`. -/ def standardRecipe (V : P → Set W) (x : Sentence P) (alts : Set (Sentence P)) : Set (Set W) := {s | s.Nonempty ∧ x.Believes V s ∧ ∀ a ∈ alts, ¬ a.Believes V s} --- on a plain disjunction this is the recipe of `NeoGricean.primaryImplicatures` -theorem mem_standardRecipe_or_iff (hp : V p ⊂ V p ∪ V q) (hq : V q ⊂ V p ∪ V q) : - s ∈ standardRecipe V (or (atom p) (atom q)) {atom p, atom q} ↔ - s.Nonempty ∧ s ∈ Iic (V p ∪ V q) ∩ primaryImplicatures (V p ∪ V q) {V p, V q} := by - simp only [standardRecipe, mem_ofPred_eq, mem_inter_iff, mem_primaryImplicatures] - refine and_congr_right fun _ ↦ and_congr_right fun _ ↦ ?_ - simp only [mem_insert_iff, mem_singleton_iff, forall_eq_or_imp, forall_eq] - exact ⟨fun ⟨h1, h2⟩ ↦ ⟨fun _ ↦ h1, fun _ ↦ h2⟩, fun ⟨h1, h2⟩ ↦ ⟨h1 hp, h2 hq⟩⟩ - -- (11), steps i–iv of p. 110: for a plain disjunction the Standard Recipe delivers ignorance theorem poss_of_mem_standardRecipe_or (hs : s ∈ standardRecipe V (or (atom p) (atom q)) {atom p, atom q}) : @@ -321,12 +260,6 @@ abbrev cells (V : P → Set W) (x y a b c : Sentence P) : List (Set (Set W) × S [({s | x.Poss V s ∧ y.Poss V s}, c), ({s | x.Poss V s ∧ ¬ y.Poss V s}, a), ({s | ¬ x.Poss V s ∧ y.Poss V s}, b)] -/-- The alternatives of pp. 115–116: in its cell, a consistent speaker of `u` believes the sentence, -and the sentence entails `u`. -/ -def AreAlternatives (V : P → Set W) (u : Sentence P) (alts : List (Set (Set W) × Sentence P)) : - Prop := - ∀ c ∈ alts, ∀ s ∈ c.1, s.Nonempty → u.Believes V s → c.2.Believes V s ∧ c.2.Entails V u - variable {κ : Type*} [Preorder κ] {cost : Sentence P → κ} /-- The alternative heuristic (i): the consistent states that believe the sentence uttered and @@ -367,35 +300,6 @@ alternatives have the same size, as p. 122 says of (22). -/ abbrev altsScalar (V : P → Set W) (u x : Sentence P) : List (Set (Set W) × Sentence P) := cells V x (neg x) x (and u (neg x)) (and u (may x)) -example : AreAlternatives V (or (atom p) (atom q)) (altsOr V p q) := by - simp only [AreAlternatives, List.forall_mem_cons, List.not_mem_nil, false_implies, implies_true, - and_true] - refine ⟨fun s ⟨hp, hq⟩ hs h ↦ ⟨believes_and.2 ⟨(believes_may hs).2 hp, - believes_and.2 ⟨(believes_may hs).2 hq, h⟩⟩, - fun _ h' ↦ (believes_and.1 (believes_and.1 h').2).2⟩, - fun s ⟨_, hq⟩ _ h ↦ ⟨fun w hw ↦ (h hw).resolve_right fun hwq ↦ hq ⟨w, hw, hwq⟩, - fun _ h' _ hw ↦ .inl (h' hw)⟩, - fun s ⟨hp, _⟩ _ h ↦ ⟨fun w hw ↦ (h hw).resolve_left fun hwp ↦ hp ⟨w, hw, hwp⟩, - fun _ h' _ hw ↦ .inr (h' hw)⟩⟩ - -example : AreAlternatives V (may (or (atom p) (atom q))) (altsMayOr V p q) := by - have key {r : P} (hr : V r ⊆ V p ∪ V q) : (may (atom r)).Entails V (may (or (atom p) (atom q))) := - fun _ h _ hw ↦ (h hw).mono (inter_subset_inter_right _ hr) - simp only [AreAlternatives, List.forall_mem_cons, List.not_mem_nil, false_implies, implies_true, - and_true] - exact ⟨fun s ⟨hp, hq⟩ hs _ ↦ ⟨believes_and.2 ⟨(believes_may hs).2 hp, (believes_may hs).2 hq⟩, - fun t h ↦ key subset_union_left t (believes_and.1 h).1⟩, - fun s ⟨hp, _⟩ hs _ ↦ ⟨(believes_may hs).2 hp, key subset_union_left⟩, - fun s ⟨_, hq⟩ hs _ ↦ ⟨(believes_may hs).2 hq, key subset_union_right⟩⟩ - -example (hx : x.Entails V u) : AreAlternatives V u (altsScalar V u x) := by - simp only [AreAlternatives, List.forall_mem_cons, List.not_mem_nil, false_implies, implies_true, - and_true] - exact ⟨fun s ⟨hp, _⟩ hs h ↦ ⟨believes_and.2 ⟨h, (believes_may hs).2 hp⟩, - fun _ h' ↦ (believes_and.1 h').1⟩, - fun s ⟨_, hn⟩ _ _ ↦ ⟨not_poss_neg.1 hn, hx⟩, - fun s ⟨hp, _⟩ _ h ↦ ⟨believes_and.2 ⟨h, believes_neg.2 hp⟩, fun _ h' ↦ (believes_and.1 h').1⟩⟩ - -- p. 115: the speaker of (15) considers both disjuncts possible theorem mem_survivors_or_iff : s ∈ survivors V size (or (atom p) (atom q)) (altsOr V p q) ↔ @@ -483,34 +387,11 @@ theorem readings_ssubset_iff (q : Quant) : exact down notMoreThanOne_not_predictsLocalSIWeak notMoreThanOne_not_predictsLocalSI not_classical_notMoreThanOne local_notMoreThanOne -variable {some many all : Set W} - --- (39)–(40), p. 148: `exh` is the operator O of (39); O (44b), the parse under negation (42c) -theorem exh_many (hs : many ⊆ some) (ha : all ⊂ many) : - exh {some, many, all} many = many \ all := by - rw [exh_insert_of_subset hs, exh_insert_of_subset subset_rfl, exh_singleton_of_not_subset ha.2] - --- (43), p. 149: O (43b), the parse (42b) -theorem exh_compl_many (hs : many ⊂ some) (ha : all ⊆ many) : - exh {someᶜ, manyᶜ, allᶜ} manyᶜ = manyᶜ ∩ some := by - rw [exh_insert_of_not_subset fun h ↦ hs.2 (compl_subset_compl.1 h), - exh_insert_of_subset subset_rfl, exh_singleton_of_subset (compl_subset_compl.2 ha), - sdiff_compl] - --- (47), p. 150: the Power Principle prefers (42b) to the readings (42a) and (42c) -theorem isLeast_readings_negation (hs : many ⊂ some) (ha : all ⊂ many) : - IsLeast {manyᶜ, exh {someᶜ, manyᶜ, allᶜ} manyᶜ, (exh {some, many, all} many)ᶜ} - (exh {someᶜ, manyᶜ, allᶜ} manyᶜ) := by - rw [exh_compl_many hs ha.1, exh_many hs.1 ha] - refine ⟨by simp, ?_⟩ - rintro _ (rfl | rfl | rfl) - · exact inter_subset_left - · exact subset_rfl - · exact fun w hw hn ↦ hw.1 hn.1 +variable {some all : Set W} --- (57), pp. 156–157: the Power Principle prefers the narrow-scope parse (57b) of (56b), which --- yields the inference the text says does not go through. That it is the stronger needs a serial --- relation, which the text leaves tacit +-- (47), (57), pp. 150, 156–157, with O of (39) as `exh`: the Power Principle prefers the +-- narrow-scope parse (57b) of (56b), which yields the inference the text says does not go through. +-- That it is the stronger needs a serial relation, which the text leaves tacit theorem isLeast_readings_core (R : SetRel W W) [ModalLogic.IsSerial R] (ha : all ⊂ some) : IsLeast {R.core some, exh {R.core some, R.core all} (R.core some), R.core (exh {some, all} some)} (R.core (exh {some, all} some)) := by @@ -526,19 +407,6 @@ theorem isLeast_readings_core (R : SetRel W W) [ModalLogic.IsSerial R] (ha : all exact absurd (hwq hv) (hw hv).2 · exact subset_rfl --- (25), p. 143: the negated upper-bounded *like* is *don't like or love*, not the printed *don't --- like or don't love*, which excludes the continuation *we LOVE it* -theorem compl_sdiff_like {like love : Set W} (h : love ⊆ like) : - (like \ love)ᶜ = likeᶜ ∪ love ∧ Disjoint (likeᶜ ∪ loveᶜ) love := by - refine ⟨by ext w; simp only [mem_compl_iff, mem_sdiff, mem_union]; tauto, ?_⟩ - exact disjoint_left.2 fun _ hw hl ↦ hw.elim (· (h hl)) (· hl) - --- (48)–(49), p. 189: O can shift a lower bound too, given the alternative RICH₁ -theorem exh_rich {rich rich₂ : Set W} (h : rich₂ ⊆ rich) (hne : rich₂.Nonempty) : - exh {rich \ rich₂} rich = rich₂ := by - obtain ⟨v, hv⟩ := hne - rw [exh_singleton_of_not_subset fun hs ↦ (hs (h hv)).2 hv, sdiff_sdiff_eq_self h] - end Conventionalism /-! ### Embedded implicatures -/ @@ -581,19 +449,14 @@ theorem isSecondaryImplicature_mango_iff (hA : A ⊆ F) (hM : (M \ F).Nonempty) open GeurtsPouscoulous2009 in -- §8.2, (10)–(12), pp. 168–169, after [vanrooij-schulz-2004] and [russell-2006]: the reading of (9) --- that looks local, from the strong implicature at the speaker and Competence of the subject +-- that looks local, from the strong implicature at the speaker and Competence of the subject. The +-- step for *hope*, (15)–(17), pp. 170–171, has the same form and differs in the plausibility of +-- (16) theorem subset_core_exh {R : SetRel W W} {some all : Set W} (hall : all ⊂ some) (hq : s ⊆ R.core some) (h10 : s ⊆ (R.core all)ᶜ) (h11 : s ⊆ R.core all ∪ R.core allᶜ) : s ⊆ R.core (Exhaustification.exh {some, all} some) := fun _ hw ↦ local_of_global_of_opinionated R hall (hq hw) (h10 hw) (h11 hw) --- (10)–(12) and, for *hope*, (15)–(17), pp. 170–171, share this form, for any attitude: what --- separates them is the plausibility of the second premise. (11) and (16), as printed, have the --- disjunction outside the speaker's belief; given the first premise that says the same -theorem subset_or_subset_iff {X Y : Set W} (h10 : s ⊆ Xᶜ) : (s ⊆ X ∨ s ⊆ Y) ↔ s ⊆ X ∪ Y := - ⟨fun h ↦ h.elim (·.trans subset_union_left) (·.trans subset_union_right), - fun h ↦ .inr fun _ hw ↦ (h hw).resolve_left (h10 hw)⟩ - section Indefinites variable {D : Type*} {sailor some all : W → Set D} {t : SetRel W D} @@ -607,13 +470,6 @@ theorem subset_inter_compl_ofSuccessors t ⊆ SetRel.ofSuccessors sailor ∩ SetRel.ofSuccessors some ∩ (SetRel.ofSuccessors all)ᶜ := subset_inter h32 ((Question.mem_polar.1 hc).resolve_left h34) --- p. 139: that (14) is false, given (32), entails (35), so that the alternative-based inference is --- the stronger -theorem subset_compl_ofSuccessors (h32 : t ⊆ SetRel.ofSuccessors sailor) - (h14 : t ⊆ Prod.fst ⁻¹' (SetRel.ofSuccessors (sailor ⊓ all)).dom ᶜ) : - t ⊆ (SetRel.ofSuccessors all)ᶜ := - fun p hp hall ↦ h14 hp ⟨p.2, h32 hp, hall⟩ - end Indefinites end Embedded @@ -658,29 +514,16 @@ theorem rows_table2 {a : Fin 4 → Set W} (ha : StrictAnti a) : · simpa using ha.lt_iff_gt.symm · simpa using (compl_lt_compl_iff_lt.trans ha.lt_iff_gt).symm -/-- The inferences of the rows that a Gricean derivation bears on, which the text says are conveyed -or not. -/ +/-- The three contrasts on which Gricean reasoning derives one inference and not its neighbour. -/ inductive Item where - | disjunct | freeChoice | sameLength | afterUse | longer | figs | mango | referent | everySailor + | sameLength | longer | figs | mango | referent | everySailor deriving DecidableEq /-- The statement that the theory derives the inference, over any model of the sentence. -/ def Item.Derived : Item → Prop - | .disjunct => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V size (or (atom true) (atom false)) (altsOr V true false) → - (atom true).Poss V s ∧ (atom false).Poss V s - | .freeChoice => ∀ {W : Type} (V : Bool → Set W) (s : Set W), - s ∈ survivors V size (may (or (atom true) (atom false))) (altsMayOr V true false) → - (may (atom true)).Believes V s ∧ (may (atom false)).Believes V s | .sameLength => ∀ {W : Type} (V : Bool → Set W) (s : Set W), s ∈ survivors V size (atom true) (altsScalar V (atom true) (atom false)) → ¬ (atom false).Believes V s - | .afterUse => ∀ {W : Type} (V : Bool → Set W) (cost : Sentence Bool → ℕ) (s : Set W), - cost (atom false) ≤ cost (atom true) → - cost (and (atom true) (neg (atom false))) ≤ cost (atom true) → - ¬ cost (and (atom true) (may (atom false))) ≤ cost (atom true) → - s ∈ survivors V cost (atom true) (altsScalar V (atom true) (atom false)) → - ¬ (atom false).Believes V s ∧ (atom false).Poss V s | .longer => ∀ {W : Type} (V : Bool → Set W) (s : Set W), s ∈ survivors V size (atom true) (altsScalar V (atom true) (and (atom false) (atom true))) → ¬ (and (atom false) (atom true)).Believes V s @@ -695,53 +538,40 @@ def Item.Derived : Item → Prop t ⊆ SetRel.ofSuccessors sailor → t ⊆ (SetRel.ofSuccessors all)ᶜ → t ⊆ Prod.fst ⁻¹' (SetRel.ofSuccessors (sailor ⊓ all)).dom ᶜ --- (26b), p. 124: *big toe* is longer than *toe*, so that nothing rules out believing it -theorem Item.not_derived_longer : ¬ Item.longer.Derived := fun h ↦ - @h Unit (fun _ ↦ univ) univ - (mem_survivors_scalar_iff.2 ⟨univ_nonempty, fun _ _ ↦ mem_univ _, by simp [size]⟩) - fun _ _ ↦ ⟨mem_univ _, mem_univ _⟩ - --- (3), p. 165: Competence is not consistent for the first disjunct -theorem Item.not_derived_mango : ¬ Item.mango.Derived := fun h ↦ by - have hA : ({2} : Set (Fin 3)) ⊆ {1, 2} := by simp - have hM : (({0} : Set (Fin 3)) \ {1, 2}).Nonempty := ⟨0, by simp⟩ - have hF : (({1, 2} : Set (Fin 3)) \ ({0} ∪ {2})).Nonempty := ⟨1, by simp⟩ - have := (isSecondaryImplicature_mango_iff hA hM hF (by simp)).1 - (@h (Fin 3) {0} {1, 2} {2} hA hM hF) - exact absurd (mem_singleton_iff.1 (this ▸ mem_singleton (0 : Fin 3))) (by decide) - --- pp. 139, 180: (35) does not entail that (14) is false, so that the story need not be about every --- sailor -theorem Item.not_derived_everySailor : ¬ Item.everySailor.Derived := fun h ↦ by - have := @h Unit Bool (fun _ ↦ univ) (fun _ ↦ {true}) {((), false)} - (fun _ _ ↦ mem_univ _) (by rintro _ rfl hb; simp [SetRel.ofSuccessors] at hb) - exact this rfl ⟨true, mem_univ _, rfl⟩ - theorem Item.derived_iff : ∀ i : Item, i.Derived ↔ i ∉ [Item.longer, .mango, .everySailor] - | .disjunct => iff_of_true (fun _ _ h ↦ (mem_survivors_or_iff.1 h).2.2) (by decide) - | .freeChoice => iff_of_true (fun _ _ h ↦ (mem_survivors_may_or_iff.1 h).2) (by decide) | .sameLength => iff_of_true (fun _ _ h ↦ (mem_survivors_scalar_iff.1 h).2.2 le_rfl) (by decide) - | .afterUse => iff_of_true (fun _ _ _ ha hb hc h ↦ - have ⟨_, _, hp, hn⟩ := (mem_survivors_of_available ha hb hc).1 h - ⟨poss_neg.1 hn, hp⟩) (by decide) - | .longer => iff_of_false Item.not_derived_longer (by decide) + -- (26b), p. 124: *big toe* is longer than *toe*, so that nothing rules out believing it + | .longer => iff_of_false (fun h ↦ @h Unit (fun _ ↦ univ) univ + (mem_survivors_scalar_iff.2 ⟨univ_nonempty, fun _ _ ↦ mem_univ _, by simp [size]⟩) + fun _ _ ↦ ⟨mem_univ _, mem_univ _⟩) (by decide) | .figs => iff_of_true (fun _ _ _ ↦ isSecondaryImplicature_mango) (by decide) - | .mango => iff_of_false Item.not_derived_mango (by decide) + -- (3), p. 165: Competence is not consistent for the first disjunct + | .mango => iff_of_false (fun h ↦ by + have hA : ({2} : Set (Fin 3)) ⊆ {1, 2} := by simp + have hM : (({0} : Set (Fin 3)) \ {1, 2}).Nonempty := ⟨0, by simp⟩ + have hF : (({1, 2} : Set (Fin 3)) \ ({0} ∪ {2})).Nonempty := ⟨1, by simp⟩ + have := (isSecondaryImplicature_mango_iff hA hM hF (by simp)).1 + (@h (Fin 3) {0} {1, 2} {2} hA hM hF) + exact absurd (mem_singleton_iff.1 (this ▸ mem_singleton (0 : Fin 3))) (by decide)) (by decide) | .referent => iff_of_true (fun _ _ _ _ h32 h34 hc ↦ (subset_inter_compl_ofSuccessors h32 h34 hc).trans inter_subset_right) (by decide) - | .everySailor => iff_of_false Item.not_derived_everySailor (by decide) + -- pp. 139, 180: (35) does not entail that (14) is false: the story need not be about every sailor + | .everySailor => iff_of_false (fun h ↦ by + have := @h Unit Bool (fun _ ↦ univ) (fun _ ↦ {true}) {((), false)} + (fun _ _ ↦ mem_univ _) (by rintro _ rfl hb; simp [SetRel.ofSuccessors] at hb) + exact this rfl ⟨true, mem_univ _, rfl⟩) (by decide) /-- Reads the item of a row and whether the text says the inference is conveyed. -/ def inference? (ex : Datum) : Option (Item × Bool) := do - let item ← ex.parse? "item" [("disjunct", Item.disjunct), ("freeChoice", .freeChoice), - ("sameLength", .sameLength), ("afterUse", .afterUse), ("longer", .longer), ("figs", .figs), - ("mango", .mango), ("referent", .referent), ("everySailor", .everySailor)] + let item ← ex.parse? "item" [("sameLength", Item.sameLength), ("longer", .longer), + ("figs", .figs), ("mango", .mango), ("referent", .referent), ("everySailor", .everySailor)] let conveys ← ex.bool? "conveys" pure (item, conveys) -example : Datum.ReadCount inference? Examples.all 11 := by decide +example : Datum.ReadCount inference? Examples.all 7 := by decide --- the rows on which a derivation bears: the theory derives what the text says is conveyed +-- (13), (26), (6), (3), (31), (29): the theory derives what the text says is conveyed, and not its +-- neighbour theorem rows_conveys : ∀ r ∈ Examples.all.filterMap inference?, (r.2 = true ↔ r.1.Derived) := by simp only [Item.derived_iff] decide diff --git a/Studies/GeurtsPouscoulous2009.lean b/Studies/GeurtsPouscoulous2009.lean index ccb89a218a..ce86294abd 100644 --- a/Studies/GeurtsPouscoulous2009.lean +++ b/Studies/GeurtsPouscoulous2009.lean @@ -142,8 +142,6 @@ abbrev Situation := Fin 3 → Fin 3 → Prop and each of the others with two of them. -/ abbrev figure2 : Situation := fun s c ↦ s = 0 ∨ (s = 1 ∧ c ≠ 2) ∨ (s = 2 ∧ c ≠ 0) -example : ∃! s : Fin 3, ∀ c, figure2 s c := ⟨0, fun _ ↦ .inl rfl, by decide⟩ - /-- The situation for *more than one* and the two downward-entailing sentences, in which every square is connected with some circle and two of them with all. -/ abbrev allSome : Situation := fun s c ↦ s ≠ 0 ∨ c = 0