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.IdiomTypology.

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.ScalarModel: argument points, entails, strongerThan (A5), negEntails (A4), satisfiesA3
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.rankScalarModel, linguistLangModel: worked scalar models
FillmoreKayOConnor1988.allExamples: the paper's judgment data

Scalar models (§2.3.2, Appendix) #

The formal backbone of the paper: an n-dimensional argument space with a monotonicity constraint on propositional functions. Definition A3 (p. 536): ⟨S, T, Dˣ, P⟩ is a scalar model iff, for distinct dᵢ, dⱼ in Dˣ, P(dⱼ) entails P(dᵢ) just in case dᵢ is lower than dⱼ.

structure FillmoreKayOConnor1988.ArgumentPoint (α : Type u_1) :

Type u_1

An argument point in the n-dimensional argument space Dˣ. In the paper's 2D example, (Brilliant, English) is an argument point in the linguists × languages space.

coordinates : List α
Coordinates, one per dimension

Instances For

def FillmoreKayOConnor1988.instDecidableEqArgumentPoint.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : ArgumentPoint α✝) :

Decidable (x✝ = x✝¹)

Equations

FillmoreKayOConnor1988.instDecidableEqArgumentPoint.decEq { coordinates := a } { coordinates := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableEqArgumentPoint {α✝ : Type u_1} [DecidableEq α✝] :

DecidableEq (ArgumentPoint α✝)

Equations

FillmoreKayOConnor1988.instDecidableEqArgumentPoint = FillmoreKayOConnor1988.instDecidableEqArgumentPoint.decEq

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprArgumentPoint {α✝ : Type u_1} [Repr α✝] :

Repr (ArgumentPoint α✝)

Equations

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

def FillmoreKayOConnor1988.instReprArgumentPoint.repr {α✝ : Type u_1} [Repr α✝] :

ArgumentPoint α✝ → ℕ → Std.Format

Equations

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

Instances For

def FillmoreKayOConnor1988.ArgumentPoint.isLower {α : Type u_1} (le : α → α → Bool) (di dj : ArgumentPoint α) :

Bool

dᵢ is LOWER than dⱼ (definition A2, p. 536): no coordinate of dᵢ has a higher value than the corresponding coordinate of dⱼ, and at least one coordinate is strictly lower.

Equations

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

Instances For

structure FillmoreKayOConnor1988.ScalarModel (S : Type u_1) (α : Type u_2) :

Type (max u_1 u_2)

A scalar model candidate: argument points, a propositional function, and a per-dimension ordering. Definition A3's monotonicity constraint is checked by satisfiesA3 rather than carried as a field, so that deliberately defective models can be discussed.

points : List (ArgumentPoint α)
Argument points (elements of Dˣ)
propFn : ArgumentPoint α → S → Bool
Propositional function: argument point → proposition over states
dimLe : α → α → Bool
Ordering on individual dimension values

Instances For

def FillmoreKayOConnor1988.ScalarModel.entails {S : Type u_1} {α : Type u_2} (sm : ScalarModel S α) (dj di : ArgumentPoint α) :

Scalar entailment: P(dⱼ) entails P(dᵢ) iff every state verifying P(dⱼ) verifies P(dᵢ).

Equations

sm.entails dj di = ∀ (s : S), sm.propFn dj s = true → sm.propFn di s = true

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableEntailsOfFintype {S : Type u_1} {α : Type u_2} [Fintype S] (sm : ScalarModel S α) (dj di : ArgumentPoint α) :

Decidable (sm.entails dj di)

Equations

FillmoreKayOConnor1988.instDecidableEntailsOfFintype sm dj di = FillmoreKayOConnor1988.instDecidableEntailsOfFintype._aux_1 sm dj di

def FillmoreKayOConnor1988.ScalarModel.strongerThan {S : Type u_1} {α : Type u_2} (sm : ScalarModel S α) (dj di : ArgumentPoint α) :

Informativeness/strength (definition A5, p. 537): p is MORE INFORMATIVE (STRONGER) than q relative to a scalar model iff p entails q and q does not entail p.

Equations

sm.strongerThan dj di = (sm.entails dj di ∧ ¬sm.entails di dj)

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableStrongerThanOfFintype {S : Type u_1} {α : Type u_2} [Fintype S] (sm : ScalarModel S α) (dj di : ArgumentPoint α) :

Decidable (sm.strongerThan dj di)

Equations

FillmoreKayOConnor1988.instDecidableStrongerThanOfFintype sm dj di = FillmoreKayOConnor1988.instDecidableStrongerThanOfFintype._aux_1 sm dj di

def FillmoreKayOConnor1988.ScalarModel.negEntails {S : Type u_1} {α : Type u_2} (sm : ScalarModel S α) (di dj : ArgumentPoint α) :

Negative scalar entailment (definition A4, p. 536): ¬P(dᵢ) entails ¬P(dⱼ) just in case dᵢ is lower than dⱼ. This is 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

sm.negEntails di dj = ∀ (s : S), sm.propFn di s = false → sm.propFn dj s = false

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableNegEntailsOfFintype {S : Type u_1} {α : Type u_2} [Fintype S] (sm : ScalarModel S α) (di dj : ArgumentPoint α) :

Decidable (sm.negEntails di dj)

Equations

FillmoreKayOConnor1988.instDecidableNegEntailsOfFintype sm di dj = FillmoreKayOConnor1988.instDecidableNegEntailsOfFintype._aux_1 sm di dj

def FillmoreKayOConnor1988.ScalarModel.negStrongerThan {S : Type u_1} {α : Type u_2} (sm : ScalarModel S α) (di dj : ArgumentPoint α) :

A5 strength for negated propositions: ¬P(dᵢ) is stronger than ¬P(dⱼ) iff it entails and is not entailed by it.

Equations

sm.negStrongerThan di dj = (sm.negEntails di dj ∧ ¬sm.negEntails dj di)

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableNegStrongerThanOfFintype {S : Type u_1} {α : Type u_2} [Fintype S] (sm : ScalarModel S α) (di dj : ArgumentPoint α) :

Decidable (sm.negStrongerThan di dj)

Equations

FillmoreKayOConnor1988.instDecidableNegStrongerThanOfFintype sm di dj = FillmoreKayOConnor1988.instDecidableNegStrongerThanOfFintype._aux_1 sm di dj

def FillmoreKayOConnor1988.ScalarModel.satisfiesA3Forward {S : Type u_1} {α : Type u_2} (sm : ScalarModel S α) (states : List S) :

Bool

Forward half of definition A3 over a finite state list: whenever dᵢ is lower than dⱼ, P(dⱼ) entails P(dᵢ).

Equations

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

Instances For

def FillmoreKayOConnor1988.ScalarModel.satisfiesA3 {S : Type u_1} {α : Type u_2} [DecidableEq α] (sm : ScalarModel S α) (states : List S) :

Bool

Full definition A3 over a finite state list: for distinct dᵢ, dⱼ, P(dⱼ) entails P(dᵢ) just in case dᵢ is lower than dⱼ. The biconditional is demanding: a state list too sparse to separate the points produces artifact entailments between incomparable points and fails this check (see ll_sparse_fails_A3).

Equations

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

Instances For

The let alone construction (§2.1–2.4) #

def FillmoreKayOConnor1988.letAloneConstruction :

ConstructionGrammar.Construction

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 ([Dun25]'s slot projection), 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).

structure FillmoreKayOConnor1988.LetAloneConditions (S : Type u_1) (α : Type u_2) :

Type (max u_1 u_2)

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).

scalarModel : ScalarModel S α
The presupposed scalar model
focusA : ArgumentPoint α
Argument point for the A focus (in the initial, full clause)
focusB : ArgumentPoint α
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 => self.scalarModel.negStrongerThan self.focusA self.focusB | Features.Polarity.positive => self.scalarModel.strongerThan self.focusA self.focusB
Condition (3): the full clause expresses the stronger proposition — via A4 under negation, via A5 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
muchLess : LetAloneFamily
notToMention : LetAloneFamily
neverMind : LetAloneFamily
ifNot : LetAloneFamily
inFact : LetAloneFamily

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLetAloneFamily :

DecidableEq LetAloneFamily

Equations

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

@[implicit_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
tooComplementation : LetAloneNPITrigger
comparisonOfInequality : LetAloneNPITrigger
onlyDeterminer : LetAloneNPITrigger
minimalAttainment : LetAloneNPITrigger
conditionalSurprise : LetAloneNPITrigger
failureVerb : LetAloneNPITrigger
anyoneWhod : LetAloneNPITrigger

Instances For

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprLetAloneNPITrigger :

Repr LetAloneNPITrigger

Equations

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

def FillmoreKayOConnor1988.npiTriggerToContext :

LetAloneNPITrigger → Features.LicensingContext

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

Equations

Instances For

def FillmoreKayOConnor1988.coordinationConstruction :

ConstructionGrammar.Construction

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

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

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

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableEqRank :

DecidableEq Rank

Equations

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

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

Instances For

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

def FillmoreKayOConnor1988.rankLe (a b : Rank) :

Bool

Rank ordering.

Equations

FillmoreKayOConnor1988.rankLe a b = decide (a.idx ≤ b.idx)

Instances For

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

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprAchievementState :

Repr AchievementState

Equations

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instFintypeAchievementState :

Fintype AchievementState

Equations

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

def FillmoreKayOConnor1988.madeRank (r : Rank) :

AchievementState → Bool

"He made rank r" holds iff the career reached at least r.

Equations

Instances For

def FillmoreKayOConnor1988.rankStates :

List AchievementState

All career outcomes.

Equations

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

Instances For

def FillmoreKayOConnor1988.rankScalarModel :

ScalarModel AchievementState Rank

The military rank scalar model.

Equations

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

Instances For

theorem FillmoreKayOConnor1988.rank_model_satisfiesA3 :

rankScalarModel.satisfiesA3 rankStates = true

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 :

rankScalarModel.entails { coordinates := [Rank.general] } { coordinates := [Rank.colonel] }

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

theorem FillmoreKayOConnor1988.colonel_does_not_entail_general :

¬rankScalarModel.entails { coordinates := [Rank.colonel] } { coordinates := [Rank.general] }

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

theorem FillmoreKayOConnor1988.general_stronger_than_colonel :

rankScalarModel.strongerThan { coordinates := [Rank.general] } { coordinates := [Rank.colonel] }

Making general is the stronger positive proposition (A5). 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 AchievementState Rank

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 (pt : ArgumentPoint Rank) :

pt ∈ rankScalarModel.points → ¬ArgumentPoint.isLower rankLe pt { coordinates := [Rank.secondLieutenant] } = true

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 → least).

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

Instances For

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprLinguist :

Equations

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instFintypeLinguist :

Fintype Linguist

Equations

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

inductive FillmoreKayOConnor1988.Lang :

Languages ordered by accessibility (most → least).

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

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLang :

DecidableEq Lang

Equations

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

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

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instFintypeLang :

Fintype Lang

Equations

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

inductive FillmoreKayOConnor1988.LingLangVal :

Dimension value: a linguist or a language. The argument space is Linguist × Lang, encoded as 2-element coordinate lists.

ling : Linguist → LingLangVal
lang : Lang → LingLangVal

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instDecidableEqLingLangVal :

DecidableEq LingLangVal

Equations

FillmoreKayOConnor1988.instDecidableEqLingLangVal = FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq

def FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq (x✝ x✝¹ : LingLangVal) :

Decidable (x✝ = x✝¹)

Equations

FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq (FillmoreKayOConnor1988.LingLangVal.ling a) (FillmoreKayOConnor1988.LingLangVal.ling b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq (FillmoreKayOConnor1988.LingLangVal.ling a) (FillmoreKayOConnor1988.LingLangVal.lang a_1) = isFalse ⋯
FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq (FillmoreKayOConnor1988.LingLangVal.lang a) (FillmoreKayOConnor1988.LingLangVal.ling a_1) = isFalse ⋯
FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq (FillmoreKayOConnor1988.LingLangVal.lang a) (FillmoreKayOConnor1988.LingLangVal.lang b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

Instances For

def FillmoreKayOConnor1988.instReprLingLangVal.repr :

LingLangVal → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprLingLangVal :

Repr LingLangVal

Equations

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

def FillmoreKayOConnor1988.lingLangLe :

LingLangVal → LingLangVal → Bool

Dimension ordering. A LOWER point yields a WEAKER proposition (definition A2; worked example p. 537: "(B, E) is lower than (B, G)"). More erudite linguists and more accessible languages are lower: "Apotheosis reads English" is the easiest proposition to satisfy. Cross-dimension comparisons are false (dimensions are independent).

Equations

Instances For

inductive FillmoreKayOConnor1988.LLState :

States of who-reads-what. The first four are Table 2's states a–d (p. 527); diagonal is a constructed staircase state (not in the paper), included to refute converse entailments.

allFalse : LLState
topLeft : LLState
twoTrue : LLState
allTrue : LLState
diagonal : LLState

Instances For

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprLLState :

Equations

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

@[implicit_reducible]

instance FillmoreKayOConnor1988.instFintypeLLState :

Fintype LLState

Equations

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

def FillmoreKayOConnor1988.canRead :

Linguist → Lang → LLState → Bool

"Professor X can read language L" in each state.

Equations

Instances For

def FillmoreKayOConnor1988.llPoint (l : Linguist) (lang : Lang) :

ArgumentPoint LingLangVal

Convenience constructor for 2D argument points.

Equations

FillmoreKayOConnor1988.llPoint l lang = { coordinates := [FillmoreKayOConnor1988.LingLangVal.ling l, FillmoreKayOConnor1988.LingLangVal.lang lang] }

Instances For

def FillmoreKayOConnor1988.linguistLangModel :

ScalarModel LLState LingLangVal

The linguists × languages scalar model.

Equations

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

Instances For

def FillmoreKayOConnor1988.llStates :

All five states.

Equations

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

Instances For

theorem FillmoreKayOConnor1988.ll_model_satisfiesA3Forward :

linguistLangModel.satisfiesA3Forward llStates = true

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

theorem FillmoreKayOConnor1988.ll_sparse_fails_A3 :

linguistLangModel.satisfiesA3 llStates = false

The five-state list 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 :

linguistLangModel.entails (llPoint Linguist.brilliant Lang.hittite) (llPoint 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 :

ArgumentPoint.isLower lingLangLe (llPoint Linguist.brilliant Lang.english) (llPoint Linguist.brilliant Lang.greek) = true

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

theorem FillmoreKayOConnor1988.competent_french_incomparable_brilliant_hittite :

ArgumentPoint.isLower lingLangLe (llPoint Linguist.competent Lang.french) (llPoint Linguist.brilliant Lang.hittite) = false ∧ ArgumentPoint.isLower lingLangLe (llPoint Linguist.brilliant Lang.hittite) (llPoint Linguist.competent Lang.french) = false

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

Judgment data #

Grammaticality judgments and contrasts from the paper, by example number. Verified against the published text; judgments reproduce the paper's markings (* ungrammatical, # anomalous, ? marginal).

structure FillmoreKayOConnor1988.ExampleDatum :

A single attested or judged example.

exNumber : String
Example number in the paper
sentence : String
The sentence
judgment : Features.Acceptability
Acceptability judgment
phenomenon : String
What phenomenon this illustrates

Instances For

def FillmoreKayOConnor1988.instReprExampleDatum.repr :

ExampleDatum → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instReprExampleDatum :

Repr ExampleDatum

Equations

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

def FillmoreKayOConnor1988.instBEqExampleDatum.beq :

ExampleDatum → ExampleDatum → Bool

Equations

One or more equations did not get rendered due to their size.
FillmoreKayOConnor1988.instBEqExampleDatum.beq x✝¹ x✝ = false

Instances For

@[implicit_reducible]

instance FillmoreKayOConnor1988.instBEqExampleDatum :

BEq ExampleDatum

Equations

FillmoreKayOConnor1988.instBEqExampleDatum = { beq := FillmoreKayOConnor1988.instBEqExampleDatum.beq }

Basic let alone (§2.1, exx. 15–16, p. 512) #

def FillmoreKayOConnor1988.ex15b :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex16b :

Equations

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

Instances For

NPI licensing (§2.2.4, exx. 62–66, p. 518) #

def FillmoreKayOConnor1988.ex62 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex63 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex66 :

Equations

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

Instances For

Barely vs. almost/only (§2.3.3, exx. 113–115, p. 529) #

Barely licenses let alone; almost and non-subject only do not — "barely is syntactically a negative polarity trigger while almost and nonsubject only are not".

def FillmoreKayOConnor1988.ex113 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex114 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex115 :

Equations

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

Instances For

def FillmoreKayOConnor1988.npiContrasts :

List ExampleDatum

NPI licensing contrasts: barely licenses, almost and only do not.

Equations

FillmoreKayOConnor1988.npiContrasts = [FillmoreKayOConnor1988.ex113, FillmoreKayOConnor1988.ex114, FillmoreKayOConnor1988.ex115]

Instances For

Topicalization asymmetry (§2.2.1, exx. 31a–d, p. 515) #

def FillmoreKayOConnor1988.ex31a :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex31b :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex31c :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex31d :

Equations

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

Instances For

def FillmoreKayOConnor1988.topicalizationContrasts :

List ExampleDatum

Topicalization asymmetry: and allows full topicalization, let alone only allows extraposed second conjunct.

Equations

FillmoreKayOConnor1988.topicalizationContrasts = [FillmoreKayOConnor1988.ex31a, FillmoreKayOConnor1988.ex31b, FillmoreKayOConnor1988.ex31d]

Instances For

VP ellipsis (§2.2.1, exx. 39–41, p. 516) #

def FillmoreKayOConnor1988.ex39 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex40 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex41 :

Equations

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

Instances For

def FillmoreKayOConnor1988.vpEllipsisContrasts :

List ExampleDatum

VP ellipsis contrast: and/but allow it, let alone does not.

Equations

FillmoreKayOConnor1988.vpEllipsisContrasts = [FillmoreKayOConnor1988.ex39, FillmoreKayOConnor1988.ex40, FillmoreKayOConnor1988.ex41]

Instances For

Wh-extraction (§2.2.1, exx. 32a–b, p. 515) #

def FillmoreKayOConnor1988.ex32a :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex32b :

Equations

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

Instances For

Scalar anomaly (§2.3.2, exx. 104, 121–122, pp. 525, 530–531) #

def FillmoreKayOConnor1988.ex104 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex121 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex122a :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex122b :

Equations

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

Instances For

def FillmoreKayOConnor1988.scalarAnomalyContrasts :

List ExampleDatum

Scalar anomaly contrasts: well-formed scalar ordering vs. swapped foci.

Equations

FillmoreKayOConnor1988.scalarAnomalyContrasts = [FillmoreKayOConnor1988.ex121, FillmoreKayOConnor1988.ex122a, FillmoreKayOConnor1988.ex122b]

Instances For

IT-clefting (§2.2.1, exx. 33–34, pp. 515–516) #

def FillmoreKayOConnor1988.ex33 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex34 :

Equations

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

Instances For

Lowest-point anomaly (§2.3.2, exx. 106–107, p. 526) #

With B the lowest scale point, negating a non-lowest point yields no a-fortiori conclusion about it (see secondLieutenant_is_lowest).

def FillmoreKayOConnor1988.ex106 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex107 :

Equations

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

Instances For

Positive polarity (§2.2.4, exx. 71–72, p. 519) #

Rare but attested; these challenge a purely syntactic NPI account and are the cases LetAloneConditions.polarity := .positive covers.

def FillmoreKayOConnor1988.ex71 :

Equations

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

Instances For

def FillmoreKayOConnor1988.ex72 :

Equations

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

Instances For

def FillmoreKayOConnor1988.positivePolarityExamples :

List ExampleDatum

Positive polarity let alone examples challenge pure NPI analysis.

Equations

FillmoreKayOConnor1988.positivePolarityExamples = [FillmoreKayOConnor1988.ex71, FillmoreKayOConnor1988.ex72]

Instances For

def FillmoreKayOConnor1988.allExamples :

List ExampleDatum

All judgment data from the paper.

Equations

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

Instances For

def FillmoreKayOConnor1988.grammaticalExamples :

List ExampleDatum

All grammatical examples.

Equations

FillmoreKayOConnor1988.grammaticalExamples = List.filter (fun (x : FillmoreKayOConnor1988.ExampleDatum) => x.judgment == Features.Acceptability.ok) FillmoreKayOConnor1988.allExamples

Instances For

def FillmoreKayOConnor1988.ungrammaticalExamples :

List ExampleDatum

All ungrammatical examples.

Equations

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

Instances For

theorem FillmoreKayOConnor1988.has_all_judgment_types :

(allExamples.any fun (x : ExampleDatum) => x.judgment == Features.Acceptability.ok) = true ∧ (allExamples.any fun (x : ExampleDatum) => x.judgment == Features.Acceptability.unacceptable) = true ∧ (allExamples.any fun (x : ExampleDatum) => x.judgment == Features.Acceptability.marginal) = true ∧ (allExamples.any fun (x : ExampleDatum) => x.judgment == Features.Acceptability.anomalous) = true

The data cover all four judgment types.