Documentation

Linglib.Studies.FillmoreKayOConnor1988

[FKOC88]: Let Alone #

"Regularity and Idiomaticity in Grammatical Constructions: The Case of Let Alone" (Language 64(3):501–538), the founding Construction Grammar paper: let alone is a formal idiom — a productive syntactic pattern F ⟨X A Y let alone B⟩ whose semantics requires a presupposed scalar model (Appendix, definitions A1–A5) and whose pragmatics resolves a conflict between Gricean Quantity (the informative full clause) and Relevance (the contextually given reduced clause). The idiom typology of §1 lives in ConstructionGrammar.Idiom; §2.1's conclusion that let alone is a formal idiom is derived from the construction's typed form (let_alone_formal_idiom).

The paper's scalar models are n-dimensional with n > 1 (definition A1; fn. 16: "a scalar model must contain at least two dimensions"). The military-rank model below is a deliberate one-dimensional simplification of the paper's colonel/general example, not a paper-licit scalar model; the linguists × languages model is the paper's own 2D example.

Main declarations #

FillmoreKayOConnor1988.IsScalarModel: definition A3, over points in their product order and propositions ordered by entailment; NegEntails is definition A4
FillmoreKayOConnor1988.letAloneConstruction, LetAloneConditions, ex21Conditions: the construction, its felicity conditions (p. 528), and their instantiation for ex. 21
FillmoreKayOConnor1988.let_alone_irreducible: let alone is not fully compositional
FillmoreKayOConnor1988.MadeRank, CanRead: the worked scalar models
Data.Examples.FillmoreKayOConnor1988: the paper's judgment data (generated module; Examples.all)

Scalar models (§2.3.2, Appendix) #

The argument space Dˣ is a product of scales carrying its product order: definition A2's "dᵢ is lower than dⱼ" (p. 536) — no coordinate higher, at least one strictly lower — is di < dj in that order. Propositions are ordered by entailment — P dj ≤ P di, pointwise over states — so definition A5's "stronger" (p. 537) is strict entailment P dj < P di. Definition A3 (p. 536) then classifies propositional functions: ⟨S, T, Dˣ, P⟩ is a scalar model iff, for distinct dᵢ, dⱼ, P(dⱼ) entails P(dᵢ) just in case dᵢ is lower than dⱼ.

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLeForallPropOfFintypeOfDecidablePred_linglib {S : Type u_2} {P Q : S → Prop} [Fintype S] [DecidablePred P] [DecidablePred Q] :

Decidable (P ≤ Q)

Equations

FillmoreKayOConnor1988.instDecidableLeForallPropOfFintypeOfDecidablePred_linglib = Fintype.decidableForallFintype

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLtForallPropOfFintypeOfDecidablePred_linglib {S : Type u_2} {P Q : S → Prop} [Fintype S] [DecidablePred P] [DecidablePred Q] :

Decidable (P < Q)

Equations

FillmoreKayOConnor1988.instDecidableLtForallPropOfFintypeOfDecidablePred_linglib = instDecidableAnd

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

Definition A3 (p. 536): for distinct points, entailment of the propositions reflects the reversed point order. The biconditional is demanding: a state space too sparse to separate the points produces artifact entailments between incomparable points and fails it (see ll_sparse_fails_A3).

Equations

FillmoreKayOConnor1988.IsScalarModel P = ∀ (di dj : Point), di ≠ dj → (P dj ≤ P di ↔ di < dj)

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableIsScalarModelOfDecidableEqOfDecidableLTOfFintypeOfDecidablePred {Point : Type u_1} {S : Type u_2} [Preorder Point] [DecidableEq Point] [DecidableLT Point] [Fintype Point] [Fintype S] (P : Point → S → Prop) [(d : Point) → DecidablePred (P d)] :

Decidable (IsScalarModel P)

Equations

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

def FillmoreKayOConnor1988.NegEntails {Point : Type u_1} {S : Type u_2} (P : Point → S → Prop) (di dj : Point) :

Definition A4 (p. 536): ¬P(dᵢ) entails ¬P(dⱼ) — the direction at work in the canonical negative let alone sentences: "he didn't make colonel; a fortiori, he didn't make general" (p. 523).

Equations

FillmoreKayOConnor1988.NegEntails P di dj = ∀ (s : S), ¬P di s → ¬P dj s

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableNegEntailsOfFintypeOfDecidablePred {Point : Type u_1} {S : Type u_2} [Fintype S] (P : Point → S → Prop) [(d : Point) → DecidablePred (P d)] (di dj : Point) :

Decidable (NegEntails P di dj)

Equations

FillmoreKayOConnor1988.instDecidableNegEntailsOfFintypeOfDecidablePred P di dj = FillmoreKayOConnor1988.instDecidableNegEntailsOfFintypeOfDecidablePred._aux_1 P di dj

The let alone construction (§2.1–2.4) #

def FillmoreKayOConnor1988.letAloneConstruction :

ConstructionGrammar.Construction Unit

The let alone construction: form F ⟨X A Y let alone B⟩ (ex. 20a, p. 512), where F is a negative polarity operator, X and Y are shared non-focused material, and the paired foci A and B are points in a presupposed scalar model. The typed form is the paired-foci core, eliding the shared X/Y material.

Equations

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

Instances For

theorem FillmoreKayOConnor1988.let_alone_irreducible :

ConstructionGrammar.isFullyCompositional letAloneConstruction = false

Let alone is not fully compositional: a formal idiom with paired focus, scalar entailment, and NPI licensing requirements that cannot be derived from the universal combination schemata (see isFullyCompositional).

theorem FillmoreKayOConnor1988.let_alone_formal_idiom :

letAloneConstruction.IsFormalIdiom

Let alone "must ... be given treatment as the kind of formal idiom or special construction we have been discussing" (§2.1): the paired focus slots A and B are open.

structure FillmoreKayOConnor1988.LetAloneConditions (Point : Type u_3) (S : Type u_4) :

Type (max u_3 u_4)

Felicity conditions on let alone sentences (p. 528): (1) the two clauses express propositions from the same scalar model; (2) the propositions are of the same polarity; (3) the proposition expressed by the initial, full clause is the stronger one.

The propositions include the polarity operator F, so condition (3) runs through definition A4 in the negative case: in "he didn't make colonel, let alone general" (ex. 21), ¬P(colonel) is stronger than ¬P(general) because colonel is the lower point. The paper itself flags the potential confusion between point-strength and clause-strength here (p. 532).

P : Point → S → Prop
The presupposed scalar model's propositional function
focusA : Point
Argument point for the A focus (in the initial, full clause)
focusB : Point
Argument point for the B focus (in the reduced clause)
polarity : Features.Polarity
Condition (2): shared polarity of the two clauses
fullClauseStronger : match self.polarity with | Features.Polarity.negative => NegEntails self.P self.focusA self.focusB ∧ ¬NegEntails self.P self.focusB self.focusA | Features.Polarity.positive => self.P self.focusA < self.P self.focusB
Condition (3): the full clause expresses the stronger proposition — via A4 under negation, via A5's strict entailment directly under positive polarity (the attested positive cases, exx. 71–72, p. 519)

Instances For

inductive FillmoreKayOConnor1988.LetAloneFamily :

The let alone family (p. 533): conjunctions presupposing a scalar model relating their conjuncts. "Let alone, together with much less and not to mention, presents the stronger statement first"; in fact and if not present it second.

letAlone : LetAloneFamily
"He didn't make colonel, let alone general."
muchLess : LetAloneFamily
notToMention : LetAloneFamily
neverMind : LetAloneFamily
"She didn't eat a BITE, never mind a WHOLE MEAL" (ex. 49).
ifNot : LetAloneFamily
"I believe he made colonel, if not general" (ex. 132).
inFact : LetAloneFamily
Presents the stronger point second (ex. 131).

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLetAloneFamily :

DecidableEq LetAloneFamily

Equations

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

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLetAloneFamily :

Repr LetAloneFamily

Equations

FillmoreKayOConnor1988.instReprLetAloneFamily = { reprPrec := FillmoreKayOConnor1988.instReprLetAloneFamily.repr }

def FillmoreKayOConnor1988.instReprLetAloneFamily.repr :

LetAloneFamily → ℕ → Std.Format

Equations

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

Instances For

def FillmoreKayOConnor1988.presentsStrongerFirst :

LetAloneFamily → Bool

Clause ordering within the family (p. 533). The paper's explicit stronger-first list is let alone, much less, not to mention; the value for never mind is an inference from ex. 49, not stated there.

Equations

Instances For

inductive FillmoreKayOConnor1988.LetAloneNPITrigger :

Environments licensing let alone (exx. 62–70, p. 518). The paper names five types — "simple negation, too complementation, comparison of inequality, only as determiner of the subject, and various minimal attainment qualifiers, these and more" — over nine examples; the last three cases are formalizer labels for the remaining illustrated environments.

simpleNegation : LetAloneNPITrigger
Ex. 62: "He didn't reach Denver, let alone Chicago."
tooComplementation : LetAloneNPITrigger
Ex. 63: "I'm too tired to get up, let alone go running with you."
comparisonOfInequality : LetAloneNPITrigger
Ex. 64.
onlyDeterminer : LetAloneNPITrigger
Ex. 65: "Only a linguist would BUY that book, let alone READ it."
minimalAttainment : LetAloneNPITrigger
Ex. 66: "I barely got up in time for lunch, let alone breakfast."
conditionalSurprise : LetAloneNPITrigger
Ex. 68.
failureVerb : LetAloneNPITrigger
Ex. 69: "failed to reach the sixth GRADE … get a B.A.".
anyoneWhod : LetAloneNPITrigger
Ex. 70: "Anyone who'd been to HIGH SCHOOL, let alone GRADUATE students in MATH, should be able to solve that problem."

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLetAloneNPITrigger :

DecidableEq LetAloneNPITrigger

Equations

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

def FillmoreKayOConnor1988.instReprLetAloneNPITrigger.repr :

LetAloneNPITrigger → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLetAloneNPITrigger :

Repr LetAloneNPITrigger

Equations

FillmoreKayOConnor1988.instReprLetAloneNPITrigger = { reprPrec := FillmoreKayOConnor1988.instReprLetAloneNPITrigger.repr }

def FillmoreKayOConnor1988.npiTriggerToContext :

LetAloneNPITrigger → Polarity.LicensingContext

Map the let alone licensing environments to the licensing contexts catalogued in Polarity.

Equations

Instances For

def FillmoreKayOConnor1988.coordinationConstruction :

ConstructionGrammar.Construction Unit

The garden-variety coordination construction let alone is measured against (§2.2.1): two like-category conjuncts joined by a coordinating conjunction. Present as the parent node of the inheritance link below.

Equations

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

Instances For

def FillmoreKayOConnor1988.letAloneInheritance :

ConstructionGrammar.InheritanceLink

Let alone against the coordination diagnostics of §2.2.1 (p. 514–517). Shared with coordinating conjunctions: joins like categories, right node raising, gapping. Overridden: no VP ellipsis (exx. 39–41), no IT-clefting of the full constituent (exx. 33–34), fragment second conjunct, scalar requirement, NPI status. The inheritance-link framing is retrospective — the 1988 paper predates Goldberg's link typology.

Equations

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

Instances For

def FillmoreKayOConnor1988.letAloneNetwork :

ConstructionGrammar.Constructicon Unit

The §2.2.1 comparison as a two-node network.

Equations

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

Instances For

theorem FillmoreKayOConnor1988.letAloneNetwork_wellFormed :

letAloneNetwork.WellFormed

The link resolves: no dangling parent.

Other constructions of §1 #

def FillmoreKayOConnor1988.comparativeCorrelative :

ConstructionGrammar.Construction Unit

The X-er the Y-er comparative correlative (exx. 1–2, introduced in §1.1.3 as the flagship formal idiom). The construction's "the" is "not, so far as we can tell, found generally elsewhere in the language" (p. 507; fn. 4 notes relatives like "all the more reason" and the Old English instrumental demonstrative source).

Equations

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

Instances For

def FillmoreKayOConnor1988.incredulityResponse :

ConstructionGrammar.Construction Unit

The Incredulity Response construction ("Him be a doctor?", ex. 14h in the §2 opening list, pp. 510–511; the type is introduced in §1.1.4): a non-nominative subject with a bare-stem predicate, "used to challenge or question a proposition just posed by an interlocutor" (p. 511).

Equations

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

Instances For

A one-dimensional rank model (ex. 21) #

Ex. 21 (p. 513): "I doubt he made COLONEL in World War II, let alone GENERAL." The paper names only second lieutenant ("the lowest commissioned rank"), colonel, and general; the intermediate ranks are world-knowledge interpolation. States are the down-sets of the rank chain, so the model separates every pair of ranks and satisfies full A3 — at the cost of being one-dimensional, which definition A1 (n > 1) disallows for genuine scalar models; see the module docstring.

inductive FillmoreKayOConnor1988.Rank :

Commissioned military ranks (ex. 21's scale; intermediate members interpolated).

secondLieutenant : Rank
lieutenant : Rank
captain : Rank
major : Rank
colonel : Rank
general : Rank

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqRank :

DecidableEq Rank

Equations

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

def FillmoreKayOConnor1988.instReprRank.repr :

Rank → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprRank :

Repr Rank

Equations

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

@[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 → ℕ

Position of a rank on the scale.

Equations

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instLinearOrderRank :

LinearOrder Rank

Equations

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

inductive FillmoreKayOConnor1988.AchievementState :

Career outcomes: the down-sets of the rank chain — either no commission, or every rank up to some ceiling.

achievedNone : AchievementState
achievedUpTo (ceiling : Rank) : AchievementState

Instances For

def FillmoreKayOConnor1988.instDecidableEqAchievementState.decEq (x✝ x✝¹ : AchievementState) :

Decidable (x✝ = x✝¹)

Equations

One or more equations did not get rendered due to their size.
FillmoreKayOConnor1988.instDecidableEqAchievementState.decEq FillmoreKayOConnor1988.AchievementState.achievedNone FillmoreKayOConnor1988.AchievementState.achievedNone = isTrue ⋯
FillmoreKayOConnor1988.instDecidableEqAchievementState.decEq FillmoreKayOConnor1988.AchievementState.achievedNone (FillmoreKayOConnor1988.AchievementState.achievedUpTo ceiling) = isFalse ⋯
FillmoreKayOConnor1988.instDecidableEqAchievementState.decEq (FillmoreKayOConnor1988.AchievementState.achievedUpTo ceiling) FillmoreKayOConnor1988.AchievementState.achievedNone = isFalse ⋯

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqAchievementState :

DecidableEq AchievementState

Equations

FillmoreKayOConnor1988.instDecidableEqAchievementState = FillmoreKayOConnor1988.instDecidableEqAchievementState.decEq

def FillmoreKayOConnor1988.instReprAchievementState.repr :

AchievementState → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprAchievementState :

Repr AchievementState

Equations

FillmoreKayOConnor1988.instReprAchievementState = { reprPrec := FillmoreKayOConnor1988.instReprAchievementState.repr }

@[instance_reducible]

instance FillmoreKayOConnor1988.instFintypeAchievementState :

Fintype AchievementState

Equations

FillmoreKayOConnor1988.instFintypeAchievementState = Fintype.ofEquiv (Unit ⊕ FillmoreKayOConnor1988.Rank) FillmoreKayOConnor1988.AchievementState.proxyTypeEquiv

def FillmoreKayOConnor1988.MadeRank (r : Rank) :

AchievementState → Prop

"He made rank r": the career reached at least r.

Equations

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidablePredAchievementStateMadeRank (r : Rank) :

DecidablePred (MadeRank r)

Equations

One or more equations did not get rendered due to their size.
FillmoreKayOConnor1988.instDecidablePredAchievementStateMadeRank r FillmoreKayOConnor1988.AchievementState.achievedNone = isFalse ⋯

theorem FillmoreKayOConnor1988.rank_model_satisfiesA3 :

IsScalarModel MadeRank

The rank model satisfies full definition A3: for distinct ranks, entailment holds exactly when the entailed point is lower. The down-set state space is what makes the biconditional (not just its forward half) go through.

theorem FillmoreKayOConnor1988.general_entails_colonel :

MadeRank Rank.general ≤ MadeRank Rank.colonel

"He made general" entails "he made colonel" (A3, forward).

theorem FillmoreKayOConnor1988.colonel_does_not_entail_general :

¬MadeRank Rank.colonel ≤ MadeRank Rank.general

"He made colonel" does not entail "he made general" (A3, converse direction for the higher point).

theorem FillmoreKayOConnor1988.general_stronger_than_colonel :

MadeRank Rank.general < MadeRank Rank.colonel

Making general is the stronger positive proposition (A5's strict entailment). NB the paper's warning (p. 532): in ex. 21 the clauses are negated, so the stronger clause is "didn't make colonel" — see ex21Conditions.

def FillmoreKayOConnor1988.ex21Conditions :

LetAloneConditions Rank AchievementState

The felicity conditions of p. 528, instantiated for ex. 21 "I doubt he made COLONEL, let alone GENERAL": negative polarity, A focus colonel, B focus general; the full clause ¬P(colonel) is stronger by definition A4 because colonel is the lower point.

Equations

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

Instances For

theorem FillmoreKayOConnor1988.secondLieutenant_is_lowest (r : Rank) :

¬r < Rank.secondLieutenant

Second lieutenant is the lowest point: no rank is lower. This is the paper's explanation (p. 526) of ex. 107's anomaly — with B the lowest point, the a-fortiori inference has nothing to conclude.

The linguists × languages model (§2.3.2, Tables 1–2) #

The paper's own 2D example (pp. 526–527; Appendix Tables 3–4, p. 535): four professors ordered by erudition, four languages ordered by accessibility, and the propositional function "X can read L".

inductive FillmoreKayOConnor1988.Linguist :

Linguists ordered by erudition, most erudite lowest (definition A2's worked example, p. 537): "Apotheosis reads English" is the easiest proposition to satisfy.

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

Instances For

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLinguist :

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 → ℕ

Position on the erudition scale.

Equations

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instLinearOrderLinguist :

LinearOrder Linguist

Equations

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

inductive FillmoreKayOConnor1988.Lang :

Languages ordered by accessibility, most accessible lowest.

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLang :

DecidableEq Lang

Equations

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

def FillmoreKayOConnor1988.instReprLang.repr :

Lang → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLang :

Repr Lang

Equations

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

@[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 → ℕ

Position on the accessibility scale.

Equations

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instLinearOrderLang :

LinearOrder Lang

Equations

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

inductive FillmoreKayOConnor1988.LLState :

States of who-reads-what. Every state assigns each professor an initial segment of the accessibility scale (threshold).

allFalse : LLState
Table 2a (p. 527): nobody reads anything.
topLeft : LLState
Table 2b: only Apotheosis reads English.
twoTrue : LLState
Table 2c: Apotheosis reads English and French, Brilliant English.
allTrue : LLState
Table 2d: everybody reads everything.
diagonal : LLState
A constructed staircase state (not in the paper), included to refute converse entailments.

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLLState :

DecidableEq LLState

Equations

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

def FillmoreKayOConnor1988.instReprLLState.repr :

LLState → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instReprLLState :

Equations

FillmoreKayOConnor1988.instReprLLState = { reprPrec := FillmoreKayOConnor1988.instReprLLState.repr }

@[instance_reducible]

instance FillmoreKayOConnor1988.instFintypeLLState :

Fintype LLState

Equations

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

def FillmoreKayOConnor1988.LLState.threshold :

LLState → Linguist → ℕ

How many languages, in accessibility order, each professor reads in a state.

Equations

Instances For

def FillmoreKayOConnor1988.CanRead (p : Linguist × Lang) (s : LLState) :

"Professor X can read language L" in a state: L falls within X's initial segment of the accessibility scale.

Equations

FillmoreKayOConnor1988.CanRead p s = (p.2.idx < s.threshold p.1)

Instances For

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidablePredLLStateCanRead (p : Linguist × Lang) :

DecidablePred (CanRead p)

Equations

FillmoreKayOConnor1988.instDecidablePredLLStateCanRead p x✝ = FillmoreKayOConnor1988.instDecidablePredLLStateCanRead._aux_1 p x✝

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLEProdLinguistLang :

DecidableLE (Linguist × Lang)

Equations

FillmoreKayOConnor1988.instDecidableLEProdLinguistLang x✝¹ x✝ = instDecidableAnd

@[instance_reducible]

instance FillmoreKayOConnor1988.instDecidableLTProdLinguistLang :

DecidableLT (Linguist × Lang)

Equations

FillmoreKayOConnor1988.instDecidableLTProdLinguistLang x✝¹ x✝ = instDecidableAnd

theorem FillmoreKayOConnor1988.ll_model_satisfiesA3Forward (di dj : Linguist × Lang) :

di < dj → CanRead dj ≤ CanRead di

The 2D model satisfies the forward half of A3 over the five states: lower points' propositions are entailed.

theorem FillmoreKayOConnor1988.ll_sparse_fails_A3 :

¬IsScalarModel CanRead

The five-state space is too sparse for full A3: incomparable points end up with artifact entailments (e.g. "Brilliant reads Hittite" entails "Competent reads French" over these states, though the points are incomparable), violating A3's only-if direction. A genuine model of the paper's Table 2 universe would need the full space of nested states.

theorem FillmoreKayOConnor1988.brilliant_hittite_entails_english :

CanRead (Linguist.brilliant, Lang.hittite) ≤ CanRead (Linguist.brilliant, Lang.english)

"Brilliant can read Hittite" entails "Brilliant can read English": Hittite is less accessible, so reading it is the stronger claim.

theorem FillmoreKayOConnor1988.brilliant_english_lower_than_brilliant_greek :

(Linguist.brilliant, Lang.english) < (Linguist.brilliant, Lang.greek)

The paper's worked example (p. 537): (Brilliant, English) is lower than (Brilliant, Greek).

theorem FillmoreKayOConnor1988.competent_french_incomparable_brilliant_hittite :

¬(Linguist.competent, Lang.french) < (Linguist.brilliant, Lang.hittite) ∧ ¬(Linguist.brilliant, Lang.hittite) < (Linguist.competent, Lang.french)

(Competent, French) and (Brilliant, Hittite) are incomparable (definition A2): Competent > Brilliant on erudition but French < Hittite on accessibility.

Judgment data #

The paper's judgment data — basic let alone (exx. 15–16), NPI licensing and the barely/almost/only contrast (exx. 62–66, 113–115), constituency probes (topicalization, VP ellipsis, wh-extraction, IT-clefting; exx. 31–34, 39–41), scalar anomalies (exx. 104, 106–107, 121–122), and the attested positive-polarity cases (exx. 71–72) — live in the generated module Data.Examples.FillmoreKayOConnor1988 (Examples.all, Examples.ex113, ...), sourced from Linglib/Data/Examples/FillmoreKayOConnor1988.json.

theorem FillmoreKayOConnor1988.positive_polarity_attested :

(Examples.ex71.judgment, Examples.ex72.judgment) = (Features.Judgment.acceptable, Features.Judgment.acceptable)

The positive-polarity examples (exx. 71–72) are judged acceptable — the attested cases LetAloneConditions.polarity := .positive covers, challenging a purely syntactic NPI account.

theorem FillmoreKayOConnor1988.barely_almost_only_contrast :

Examples.ex115.judgment = Features.Judgment.acceptable ∧ Examples.ex113.judgment = Features.Judgment.ungrammatical ∧ Examples.ex114.judgment = Features.Judgment.ungrammatical

The barely/almost/only minimal triple (exx. 113–115): barely licenses let alone; almost and non-subject only do not.