Fillmore, Kay & O'Connor (1988): Regularity and idiomaticity in grammatical constructions

This file formalizes Fillmore, Kay and O'Connor's semantics of the let alone construction. A let alone sentence F ⟨X A Y let alone B⟩ (20) asserts the two propositions F′(X A Y) and F′(X B Y) (24) and presupposes a scalar model in which they are distinct points, the full clause the stronger (§2.3). The Appendix defines the model in five steps: an argument space, the product of at least two linearly ordered dimensions (A1), with its product order as "lower than" (A2, lower_iff); a propositional function P such that, for distinct points, P b entails P a exactly when a is lower than b (A3, IsScalarModel); the same for the negated propositions (A4, IsScalarModel.not_le_not_iff); and informativeness as one-way entailment (A5), the strict order on propositions, which A3 turns into the order on points (IsScalarModel.lt_iff, IsScalarModel.not_lt_not_iff). The states of affairs of Tables 1–4, where truth propagates from the one-corner and falsity from the zero-corner, are the lower sets of the argument space, and every lower-set state space is a scalar model (isScalarModel_mem). The semantic conditions of §2.3.2 — one model, one polarity, the full clause stronger (Felicitous) — thus reduce to an order on the foci: under negation A is lower than B, under positive polarity higher (felicitous_negative_iff, felicitous_positive_iff). Hence a fragment naming the lowest point of its scale is anomalous, (107) against (106) (not_felicitous_of_isBot), and exchanging the foci of one dimension between points that differ on two leaves them incomparable, (122) against (121) (swap_incomparable). The ranks of (21), (106)–(107) and (130)–(132), the linguists and languages of Tables 1–4 and (109)–(112), and the four dimensions of (121)–(122) instantiate the theory; the paper's judgments are the rows of Data/Examples/FillmoreKayOConnor1988.json, and rankRows_predicted and focusRows_predicted check them against Felicitous and the order in which the conjunction presents the stronger clause (p. 533).

The construction itself is a formal idiom, a lexically open one in the sense of §1.1.3 (letAloneConstruction_isFormalIdiom). Its syntax (§2.2) — a coordination that neither topicalizes nor clefts as a unit (31)–(34), admits no VP ellipsis because the INFL-complex belongs to the trigger F (39)–(41), and is licensed in the affective environments of Klima (62)–(70) yet attested under positive polarity when the fragment denies the context proposition (71)–(73) — and its pragmatics (§2.4), the fragment answering Relevance and the full clause Quantity, are the rows' comments and the docstrings below. Scales are pragmatic, in the tradition of Fauconnier rather than the semantic scales of Horn and Gazdar, and a scalar model needs a second dimension to bear its degrees (fn. 16, after Cresswell).

Implementation notes

• IsScalarModel is stated over any partial order; the product order of (A1)–(A2) enters through lower_iff, and the stipulation of at least two dimensions (fn. 16) is not part of the predicate. The one-dimensional rank chain is therefore treated as the slice of the persons × ranks model that fn. 16 envisages, and a slice of a scalar model is a scalar model (IsScalarModel.slice).
• A state of affairs is a LowerSet of the argument space and the propositional function is membership: "he made colonel" holds in a career exactly when colonel is among the ranks reached. The paper's Tables 2 and 4 draw four such states; table2c is the one that separates Brilliant can read English from Brilliant can read Greek.
• force renders F′ as negation or identity. The paper leaves open why only the negative part of barely reaches the fragment (§2.3.3, (118)–(119)); the barely rows are judgment data without a model, as are the constituency and licensing rows of §2.2.
• The ranks are the three the paper names; a commissioned officer in (106)–(107) is "made the lowest commissioned rank", since in a lower-set state holding some rank is holding the lowest.
• The (104)/(105) contrast rests on the two-dimension stipulation and on a lottery model the paper describes but does not build; (104) is a row without a model.

TODO

• The §1 typology of idioms (decoding and encoding, grammatical and extragrammatical, and §1.2's familiarity of pieces and of arrangement), once rows classify idioms by it. Its fourth cell, unfamiliar pieces familiarly arranged, is excluded by the argument of §1.2.1 that unique pieces have no standard principles of arrangement, which the typology should derive rather than omit.

References

• [FKOC88]
• [Kli64]
• [Fau75]
• [Hor72]
• [Gaz79]
• [Cre76]

Scalar models (Appendix)

theorem FillmoreKayOConnor1988.lower_iff {ι : Type u_3} {δ : ι → Type u_4} [(i : ι) → LinearOrder (δ i)] (a b : (i : ι) → δ i) : a < b ↔ (∀ (i : ι), a i ≤ b i) ∧ ∃ (i : ι), a i < b i

In a product of linear orders, a is lower than b iff no coordinate of a is higher than that of b and at least one is lower, which is the strict product order (A2).

def FillmoreKayOConnor1988.IsScalarModel {D : Type u_1} {S : Type u_2} [PartialOrder D] (P : D → S → Prop) : Prop

By (A3), ⟨S, T, Dˣ, P⟩ is a scalar model iff, for distinct points a and b, P b entails P a just in case a is lower than b. Propositions are ordered by entailment, the pointwise order on S → Prop.

Equations

• FillmoreKayOConnor1988.IsScalarModel P = ∀ ⦃a b : D⦄, a ≠ b → (P b ≤ P a ↔ a < b)

theorem FillmoreKayOConnor1988.IsScalarModel.not_le_not_iff {D : Type u_1} {S : Type u_2} [PartialOrder D] {P : D → S → Prop} {a b : D} (h : IsScalarModel P) (hab : a ≠ b) : ((fun (x : S) => ¬P a x) ≤ fun (x : S) => ¬P b x) ↔ a < b

By (A4), ¬ P a entails ¬ P b just in case a is lower than b.

theorem FillmoreKayOConnor1988.IsScalarModel.lt_iff {D : Type u_1} {S : Type u_2} [PartialOrder D] {P : D → S → Prop} {a b : D} (h : IsScalarModel P) : P b < P a ↔ a < b

By (A5), P b is more informative than P a, entailing it and not conversely, just in case a is lower than b.

theorem FillmoreKayOConnor1988.IsScalarModel.not_lt_not_iff {D : Type u_1} {S : Type u_2} [PartialOrder D] {P : D → S → Prop} {a b : D} (h : IsScalarModel P) : ((fun (x : S) => ¬P a x) < fun (x : S) => ¬P b x) ↔ a < b

By (A5) for the negated propositions, ¬ P a is more informative than ¬ P b just in case a is lower than b.

theorem FillmoreKayOConnor1988.IsScalarModel.slice {D : Type u_1} {S : Type u_2} [PartialOrder D] {E : Type u_3} [PartialOrder E] {P : D × E → S → Prop} (h : IsScalarModel P) (d : D) : IsScalarModel fun (e : E) => P (d, e)

Fixing a coordinate of a scalar model leaves a scalar model, so the bearers of a degree (fn. 16) may be held fixed.

theorem FillmoreKayOConnor1988.isScalarModel_mem {D : Type u_1} [PartialOrder D] : IsScalarModel fun (d : D) (s : LowerSet D) => d ∈ s

The states of affairs conforming to a scalar model are the lower sets of its argument space — truth propagating from the one-corner, falsity from the zero-corner (Tables 1–4) — and with membership as the propositional function every lower-set state space is a scalar model.

The semantic conditions on let alone sentences (§2.3.2)

def FillmoreKayOConnor1988.force {S : Type u_2} : Polarity → (S → Prop) → S → Prop

F′ of (24), the semantic operator derived from the trigger F, is negation under negative polarity and identity under positive.

Equations

• FillmoreKayOConnor1988.force Polarity.negative x✝ = fun (x : S) => ¬x✝ x
• FillmoreKayOConnor1988.force Polarity.positive x✝ = x✝

def FillmoreKayOConnor1988.Felicitous {D : Type u_1} {S : Type u_2} (P : D → S → Prop) (pol : Polarity) (a b : D) : Prop

The conditions of §2.3.2 on a let alone sentence with foci a and b are that F′(X A Y) and F′(X B Y) are propositions of one scalar model and one polarity, and that the full clause F′(X A Y) is the more informative (A5).

Equations

• FillmoreKayOConnor1988.Felicitous P pol a b = (FillmoreKayOConnor1988.force pol (P a) < FillmoreKayOConnor1988.force pol (P b))

theorem FillmoreKayOConnor1988.felicitous_negative_iff {D : Type u_1} {S : Type u_2} [PartialOrder D] {P : D → S → Prop} {a b : D} (h : IsScalarModel P) : Felicitous P Polarity.negative a b ↔ a < b

Under negation the full clause is the stronger exactly when A is the lower point, as in he didn't make colonel, let alone general.

theorem FillmoreKayOConnor1988.felicitous_positive_iff {D : Type u_1} {S : Type u_2} [PartialOrder D] {P : D → S → Prop} {a b : D} (h : IsScalarModel P) : Felicitous P Polarity.positive a b ↔ b < a

Under positive polarity the full clause is the stronger exactly when A is the higher point: you've got enough material for a whole semester, let alone a week (71).

theorem FillmoreKayOConnor1988.not_felicitous_of_isBot {D : Type u_1} {S : Type u_2} [PartialOrder D] {P : D → S → Prop} {a b : D} (h : IsScalarModel P) (hb : IsBot b) : ¬Felicitous P Polarity.negative a b

A fragment naming the lowest point of the scale is anomalous (107). Nothing is lower than it, so the a-fortiori inference from the full clause has no lower point to start from.

theorem FillmoreKayOConnor1988.swap_incomparable {ι : Type u_3} [DecidableEq ι] {δ : ι → Type u_4} [(i : ι) → Preorder (δ i)] {a b : (i : ι) → δ i} {j k : ι} (hjk : j ≠ k) (hj : a j < b j) (hk : a k < b k) : ¬Function.update a j (b j) < Function.update b j (a j) ∧ ¬Function.update b j (a j) < Function.update a j (b j)

Exchanging the foci of one dimension between two points that differ on two dimensions leaves the points incomparable, so neither clause is the stronger (122).

The construction (§2.1)

def FillmoreKayOConnor1988.letAloneConstruction : ConstructionGrammar.Construction Unit

In the let alone construction F ⟨X A Y let alone B⟩ (20a) the paired foci A and B flank let alone; the shared material X and Y and the trigger F are elided from the typed form.

Equations

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

theorem FillmoreKayOConnor1988.letAloneConstruction_isFormalIdiom : letAloneConstruction.IsFormalIdiom

The form of let alone is lexically open, since such sentences "must therefore be given treatment as the kind of formal idiom or special construction we have been discussing" (§2.1).

def FillmoreKayOConnor1988.incredulityResponse : ConstructionGrammar.Construction Unit

The incredulity type Him be a doctor? (14h), §1.1.4's formal idiom that exists "in the service of specific pragmatic or rhetorical purposes": a non-nominative subject with a bare-stem predicate.

Equations

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

The conjunction family (p. 533)

inductive FillmoreKayOConnor1988.Conjunction : Type

The fragment-taking conjunctions that presuppose a scale relating their conjuncts: let alone, much less and not to mention present the stronger clause first, in fact and if not present it second (130)–(132).

• letAlone : Conjunction
• muchLess : Conjunction
• notToMention : Conjunction
• inFact : Conjunction
• ifNot : Conjunction

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqConjunction : DecidableEq Conjunction

Equations

• FillmoreKayOConnor1988.instDecidableEqConjunction x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FillmoreKayOConnor1988.instReprConjunction.repr : Conjunction → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprConjunction : Repr Conjunction

Equations

• FillmoreKayOConnor1988.instReprConjunction = { reprPrec := FillmoreKayOConnor1988.instReprConjunction.repr }

def FillmoreKayOConnor1988.Conjunction.StrongerFirst : Conjunction → Prop

Whether the conjunction presents the stronger clause first.

Equations

• FillmoreKayOConnor1988.Conjunction.letAlone.StrongerFirst = True
• FillmoreKayOConnor1988.Conjunction.muchLess.StrongerFirst = True
• FillmoreKayOConnor1988.Conjunction.notToMention.StrongerFirst = True
• FillmoreKayOConnor1988.Conjunction.inFact.StrongerFirst = False
• FillmoreKayOConnor1988.Conjunction.ifNot.StrongerFirst = False

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidablePredConjunctionStrongerFirst : DecidablePred Conjunction.StrongerFirst

Equations

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

The paper's judgments

structure FillmoreKayOConnor1988.Row (D : Type) : Type

A sentence of the family with its conjunction, the polarity of its trigger, the points of its two foci and the paper's judgment.

• conj : Conjunction
• pol : Polarity
• a : D
• b : D
• judgment : Judgment

def FillmoreKayOConnor1988.instDecidableEqRow.decEq {D✝ : Type} [DecidableEq D✝] (x✝ x✝¹ : Row D✝) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqRow {D✝ : Type} [DecidableEq D✝] : DecidableEq (Row D✝)

Equations

• FillmoreKayOConnor1988.instDecidableEqRow = FillmoreKayOConnor1988.instDecidableEqRow.decEq

def FillmoreKayOConnor1988.instReprRow.repr {D✝ : Type} [Repr D✝] : Row D✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprRow {D✝ : Type} [Repr D✝] : Repr (Row D✝)

Equations

• FillmoreKayOConnor1988.instReprRow = { reprPrec := FillmoreKayOConnor1988.instReprRow.repr }

def FillmoreKayOConnor1988.Row.stronger {D : Type} (r : Row D) : D

The point of the clause the conjunction presents as the stronger.

Equations

• r.stronger = if r.conj.StrongerFirst then r.a else r.b

def FillmoreKayOConnor1988.Row.weaker {D : Type} (r : Row D) : D

The point of the clause the conjunction presents as the weaker.

Equations

• r.weaker = if r.conj.StrongerFirst then r.b else r.a

def FillmoreKayOConnor1988.Row.Predicted {D : Type} {S : Type u_1} (P : D → S → Prop) (r : Row D) : Prop

The conditions of §2.3.2 on the row, the conjunction fixing which clause must be the stronger.

Equations

• FillmoreKayOConnor1988.Row.Predicted P r = FillmoreKayOConnor1988.Felicitous P r.pol r.stronger r.weaker

def FillmoreKayOConnor1988.Row.FociOrdered {D : Type} [PartialOrder D] (r : Row D) : Prop

The conditions order the foci so that the stronger clause's point is the lower under negation and the higher under positive polarity.

Equations

• r.FociOrdered = match r.pol with | Polarity.negative => r.stronger < r.weaker | Polarity.positive => r.weaker < r.stronger

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableFociOrderedOfDecidableLT {D : Type} [PartialOrder D] [DecidableLT D] (r : Row D) : Decidable r.FociOrdered

Equations

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

theorem FillmoreKayOConnor1988.Row.predicted_iff {D : Type} {S : Type u_1} [PartialOrder D] {P : D → S → Prop} (h : IsScalarModel P) (r : Row D) : Predicted P r ↔ r.FociOrdered

def FillmoreKayOConnor1988.conjunctionTable : List (String × Conjunction)

Equations

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

def FillmoreKayOConnor1988.polarityTable : List (String × Polarity)

Equations

• FillmoreKayOConnor1988.polarityTable = [("negative", Polarity.negative), ("positive", Polarity.positive)]

def FillmoreKayOConnor1988.Row.ofDatum {D : Type} (foci? : Datum → Option (D × D)) (ex : Datum) : Option (Row D)

A row from an example, given a reading of its foci as points.

Equations

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

Military rank: (21), (106)–(107), (130)–(132)

inductive FillmoreKayOConnor1988.Rank : Type

The commissioned ranks the paper names, second lieutenant "the lowest commissioned rank" (§2.3.2).

• secondLieutenant : Rank
• colonel : Rank
• general : Rank

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqRank : DecidableEq Rank

Equations

• FillmoreKayOConnor1988.instDecidableEqRank x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprRank : Repr Rank

Equations

• FillmoreKayOConnor1988.instReprRank = { reprPrec := FillmoreKayOConnor1988.instReprRank.repr }

def FillmoreKayOConnor1988.instReprRank.repr : Rank → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instFintypeRank : Fintype Rank

Equations

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

def FillmoreKayOConnor1988.Rank.idx : Rank → ℕ

Equations

• FillmoreKayOConnor1988.Rank.secondLieutenant.idx = 0
• FillmoreKayOConnor1988.Rank.colonel.idx = 1
• FillmoreKayOConnor1988.Rank.general.idx = 2

@[instance_reducible]

instance FillmoreKayOConnor1988.instLinearOrderRank : LinearOrder Rank

Equations

• FillmoreKayOConnor1988.instLinearOrderRank = LinearOrder.lift' FillmoreKayOConnor1988.Rank.idx FillmoreKayOConnor1988.instLinearOrderRank._proof_1

@[reducible, inline]

abbrev FillmoreKayOConnor1988.MadeRank : Rank → LowerSet Rank → Prop

He made rank r holds in a career, the lower set of the ranks reached, when r is in it.

Equations

• FillmoreKayOConnor1988.MadeRank x1✝ x2✝ = (x1✝ ∈ x2✝)

theorem FillmoreKayOConnor1988.isBot_secondLieutenant : IsBot Rank.secondLieutenant

theorem FillmoreKayOConnor1988.anomaly_107 : ¬Felicitous MadeRank Polarity.negative Rank.secondLieutenant Rank.secondLieutenant

In (107), He wasn't even a commissioned officer, let alone a second lieutenant, the fragment names the lowest point.

def FillmoreKayOConnor1988.rankTable : List (String × Rank)

Equations

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

def FillmoreKayOConnor1988.rankFoci? (ex : Datum) : Option (Rank × Rank)

Equations

• FillmoreKayOConnor1988.rankFoci? ex = do let a ← ex.parse? "a" FillmoreKayOConnor1988.rankTable let b ← ex.parse? "b" FillmoreKayOConnor1988.rankTable pure (a, b)

def FillmoreKayOConnor1988.rankRows : List (Row Rank)

Equations

• FillmoreKayOConnor1988.rankRows = List.filterMap (FillmoreKayOConnor1988.Row.ofDatum FillmoreKayOConnor1988.rankFoci?) FillmoreKayOConnor1988.Examples.all

theorem FillmoreKayOConnor1988.rankRows_predicted (r : Row Rank) : r ∈ rankRows → (r.judgment = Judgment.acceptable ↔ Row.Predicted MadeRank r)

Among (21), (106)–(107) and (130)–(132), the acceptable sentences are exactly those meeting the conditions of §2.3.2 with the conjunction's ordering of the stronger clause.

Linguists and languages: Tables 1–4, (109)–(112)

inductive FillmoreKayOConnor1988.Linguist : Type

The professors of Indo-European linguistics in order of erudition: "Apotheosis knows every language that Brilliant knows, Brilliant knows every language that Competent knows, and Competent knows every language that Dimm knows".

• apotheosis : Linguist
• brilliant : Linguist
• competent : Linguist
• dimm : Linguist

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLinguist : DecidableEq Linguist

Equations

• FillmoreKayOConnor1988.instDecidableEqLinguist x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FillmoreKayOConnor1988.instReprLinguist.repr : Linguist → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLinguist : Repr Linguist

Equations

• FillmoreKayOConnor1988.instReprLinguist = { reprPrec := FillmoreKayOConnor1988.instReprLinguist.repr }

@[instance_reducible]

instance FillmoreKayOConnor1988.instFintypeLinguist : Fintype Linguist

Equations

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

def FillmoreKayOConnor1988.Linguist.idx : Linguist → ℕ

Equations

• FillmoreKayOConnor1988.Linguist.apotheosis.idx = 0
• FillmoreKayOConnor1988.Linguist.brilliant.idx = 1
• FillmoreKayOConnor1988.Linguist.competent.idx = 2
• FillmoreKayOConnor1988.Linguist.dimm.idx = 3

@[instance_reducible]

instance FillmoreKayOConnor1988.instLinearOrderLinguist : LinearOrder Linguist

Equations

• FillmoreKayOConnor1988.instLinearOrderLinguist = LinearOrder.lift' FillmoreKayOConnor1988.Linguist.idx FillmoreKayOConnor1988.instLinearOrderLinguist._proof_1

inductive FillmoreKayOConnor1988.Lang : Type

The languages are ordered by accessibility, so that "anyone who knows Hittite knows Greek, anyone who knows Greek knows French, and anyone who knows French knows English".

• english : Lang
• french : Lang
• greek : Lang
• hittite : Lang

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLang : DecidableEq Lang

Equations

• FillmoreKayOConnor1988.instDecidableEqLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLang : Repr Lang

Equations

• FillmoreKayOConnor1988.instReprLang = { reprPrec := FillmoreKayOConnor1988.instReprLang.repr }

def FillmoreKayOConnor1988.instReprLang.repr : Lang → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instFintypeLang : Fintype Lang

Equations

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

def FillmoreKayOConnor1988.Lang.idx : Lang → ℕ

Equations

• FillmoreKayOConnor1988.Lang.english.idx = 0
• FillmoreKayOConnor1988.Lang.french.idx = 1
• FillmoreKayOConnor1988.Lang.greek.idx = 2
• FillmoreKayOConnor1988.Lang.hittite.idx = 3

@[instance_reducible]

instance FillmoreKayOConnor1988.instLinearOrderLang : LinearOrder Lang

Equations

• FillmoreKayOConnor1988.instLinearOrderLang = LinearOrder.lift' FillmoreKayOConnor1988.Lang.idx FillmoreKayOConnor1988.instLinearOrderLang._proof_1

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLTProdLinguistLang : DecidableLT (Linguist × Lang)

Equations

• FillmoreKayOConnor1988.instDecidableLTProdLinguistLang x✝¹ x✝ = { decide := decide (x✝¹ ≤ x✝) && decide ¬x✝ ≤ x✝¹, reflects_decide := ⋯ }

@[reducible, inline]

abbrev FillmoreKayOConnor1988.CanRead : Linguist × Lang → LowerSet (Linguist × Lang) → Prop

Professor p.1 can read language p.2 in a state of affairs.

Equations

• FillmoreKayOConnor1988.CanRead x1✝ x2✝ = (x1✝ ∈ x2✝)

def FillmoreKayOConnor1988.table2c : LowerSet (Linguist × Lang)

In Table 2c, Apotheosis reads English and French, and Brilliant reads English.

Equations

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

theorem FillmoreKayOConnor1988.brilliant_english_greek : CanRead (Linguist.brilliant, Lang.english) table2c ∧ ¬CanRead (Linguist.brilliant, Lang.greek) table2c ∧ CanRead (Linguist.brilliant, Lang.greek) < CanRead (Linguist.brilliant, Lang.english)

In the Appendix's illustration, Brilliant can read English holds in Table 2c and Brilliant can read Greek does not, so the first does not entail the second, while the second entails the first because (Brilliant, English) is the lower point.

theorem FillmoreKayOConnor1988.corners (p : Linguist × Lang) : CanRead (Linguist.dimm, Lang.hittite) ≤ CanRead p ∧ (fun (x : LowerSet (Linguist × Lang)) => ¬CanRead (Linguist.apotheosis, Lang.english) x) ≤ fun (x : LowerSet (Linguist × Lang)) => ¬CanRead p x

At the corners of Table 1, Dimm can read Hittite entails that every linguist reads every language, and Apotheosis can't read English that none reads any.

theorem FillmoreKayOConnor1988.informativeness_109_112 : CanRead (Linguist.brilliant, Lang.hittite) < CanRead (Linguist.brilliant, Lang.french) ∧ ((fun (x : LowerSet (Linguist × Lang)) => ¬CanRead (Linguist.brilliant, Lang.french) x) < fun (x : LowerSet (Linguist × Lang)) => ¬CanRead (Linguist.brilliant, Lang.hittite) x) ∧ CanRead (Linguist.competent, Lang.hittite) < CanRead (Linguist.brilliant, Lang.french) ∧ (fun (x : LowerSet (Linguist × Lang)) => ¬CanRead (Linguist.brilliant, Lang.french) x) < fun (x : LowerSet (Linguist × Lang)) => ¬CanRead (Linguist.competent, Lang.french) x

In (109)–(112) each (a) sentence is more informative than its (b) sentence, Brilliant can read Hittite than Brilliant can read French, Brilliant can't read French than Brilliant can't read Hittite, Competent can read Hittite than Brilliant can read French, and Brilliant can't read French than Competent can't read French.

Complex scales: (121)–(122)

inductive FillmoreKayOConnor1988.Dim : Type

The four dimensions of (121), each with the two values its paired foci name, the lower value the one that makes the hiring the likelier: poor < rich, wash < wax, car < truck, $2 < $1.

• wealth : Dim
• task : Dim
• vehicle : Dim
• fee : Dim

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqDim : DecidableEq Dim

Equations

• FillmoreKayOConnor1988.instDecidableEqDim x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FillmoreKayOConnor1988.instReprDim.repr : Dim → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprDim : Repr Dim

Equations

• FillmoreKayOConnor1988.instReprDim = { reprPrec := FillmoreKayOConnor1988.instReprDim.repr }

@[instance_reducible]

instance FillmoreKayOConnor1988.instFintypeDim : Fintype Dim

Equations

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

@[reducible, inline]

abbrev FillmoreKayOConnor1988.Point : Type

A point of the four-dimensional argument space.

Equations

• FillmoreKayOConnor1988.Point = (FillmoreKayOConnor1988.Dim → Fin 2)

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLEPoint : DecidableLE Point

Equations

• FillmoreKayOConnor1988.instDecidableLEPoint x y = { decide := decide (∀ a ∈ Finset.univ, (fun (d : FillmoreKayOConnor1988.Dim) => x d ≤ y d) a), reflects_decide := ⋯ }

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLTPoint : DecidableLT Point

Equations

• FillmoreKayOConnor1988.instDecidableLTPoint x✝¹ x✝ = { decide := decide (x✝¹ ≤ x✝) && decide ¬x✝ ≤ x✝¹, reflects_decide := ⋯ }

@[reducible, inline]

abbrev FillmoreKayOConnor1988.CanGet : Point → LowerSet Point → Prop

You could get a wealth man to task your vehicle for fee in a state of affairs.

Equations

• FillmoreKayOConnor1988.CanGet x1✝ x2✝ = (x1✝ ∈ x2✝)

def FillmoreKayOConnor1988.Point.mk (w t v f : Fin 2) : Point

Equations

• FillmoreKayOConnor1988.Point.mk w t v f FillmoreKayOConnor1988.Dim.wealth = w
• FillmoreKayOConnor1988.Point.mk w t v f FillmoreKayOConnor1988.Dim.task = t
• FillmoreKayOConnor1988.Point.mk w t v f FillmoreKayOConnor1988.Dim.vehicle = v
• FillmoreKayOConnor1988.Point.mk w t v f FillmoreKayOConnor1988.Dim.fee = f

def FillmoreKayOConnor1988.wealthTable : List (String × Fin 2 × Fin 2)

Equations

• FillmoreKayOConnor1988.wealthTable = [("poor rich", 0, 1), ("rich poor", 1, 0)]

def FillmoreKayOConnor1988.taskTable : List (String × Fin 2 × Fin 2)

Equations

• FillmoreKayOConnor1988.taskTable = [("wash wax", 0, 1), ("wax wash", 1, 0)]

def FillmoreKayOConnor1988.vehicleTable : List (String × Fin 2 × Fin 2)

Equations

• FillmoreKayOConnor1988.vehicleTable = [("car truck", 0, 1), ("truck car", 1, 0)]

def FillmoreKayOConnor1988.feeTable : List (String × Fin 2 × Fin 2)

Equations

• FillmoreKayOConnor1988.feeTable = [("$2 $1", 0, 1), ("$1 $2", 1, 0)]

def FillmoreKayOConnor1988.focusFoci? (ex : Datum) : Option (Point × Point)

The foci of a row, one pair per dimension in the order A B.

Equations

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

def FillmoreKayOConnor1988.focusRows : List (Row Point)

Equations

• FillmoreKayOConnor1988.focusRows = List.filterMap (FillmoreKayOConnor1988.Row.ofDatum FillmoreKayOConnor1988.focusFoci?) FillmoreKayOConnor1988.Examples.all

theorem FillmoreKayOConnor1988.focusRows_predicted (r : Row Point) : r ∈ focusRows → (r.judgment = Judgment.acceptable ↔ Row.Predicted CanGet r)

In (121)–(122) the sentence with the likelier hiring in the full clause is acceptable and each exchange of one dimension's foci is not.

theorem FillmoreKayOConnor1988.featured_rows_parse (ex : Datum) : ex ∈ Examples.all → (ex.feature? "conjunction").isSome = true → (Row.ofDatum rankFoci? ex).isSome = true ∨ (Row.ofDatum focusFoci? ex).isSome = true

Every example that names a conjunction is read into one of the two models.