@cite{fillmore-kay-oconnor-1988}: Let Alone

Formalization of "Regularity and Idiomaticity in Grammatical Constructions: The Case of Let Alone" (Language 64(3):501–538).

This foundational Construction Grammar paper argues that let alone is a formal idiom: a productive syntactic pattern with non-compositional semantics and specific pragmatic constraints. The key contributions:

1. Idiom typology: encoding vs decoding, grammatical vs extragrammatical, substantive vs formal (§1.1–1.2)
2. Scalar model: n-dimensional argument space with a monotonicity constraint on propositional functions (Appendix, Definition A3)
3. Let alone construction: form F ⟨X A Y let alone B⟩ requires A and B to be points on a presupposed scale, with F'⟨X A Y⟩ entailing F'⟨X B Y⟩
4. Pragmatic function: resolves conflict between Gricean Quantity (informativeness — the A clause) and Relevance (the B clause)

Section 1: Idiom Typology (§1.1–1.2)

Fillmore et al.'s classification cross-cuts two dimensions:

• Encoding vs decoding
• Grammatical vs extragrammatical
• Substantive (lexically filled) vs formal (open slots)

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.IdiomInterpretability : Type

Encoding vs decoding idioms (§1.1.1, @cite{makkai-1972}).

A decoding idiom cannot be interpreted without prior learning ("kick the bucket"). An encoding idiom can be understood but its conventional status must be learned ("answer the door").

• decoding : IdiomInterpretability
• encoding : IdiomInterpretability

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomInterpretability.repr : IdiomInterpretability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomInterpretability : Repr IdiomInterpretability

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomInterpretability = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomInterpretability.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqIdiomInterpretability : DecidableEq IdiomInterpretability

Equations

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

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.IdiomGrammaticality : Type

Grammatical vs extragrammatical idioms (§1.1.2).

Grammatical idioms have words filling proper grammatical slots ("kick the bucket"). Extragrammatical idioms have anomalous structure ("first off", "by and large", "so far so good").

• grammatical : IdiomGrammaticality
• extragrammatical : IdiomGrammaticality

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomGrammaticality.repr : IdiomGrammaticality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomGrammaticality : Repr IdiomGrammaticality

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomGrammaticality = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomGrammaticality.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqIdiomGrammaticality : DecidableEq IdiomGrammaticality

Equations

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

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.IdiomFormality : Type

Substantive vs formal idioms (§1.1.3).

Substantive (lexically filled) idioms have fixed lexical content. Formal idioms are syntactic patterns dedicated to semantic/pragmatic purposes not knowable from form alone.

• substantive : IdiomFormality
• formal : IdiomFormality

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomFormality.repr : IdiomFormality → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomFormality : Repr IdiomFormality

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomFormality = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomFormality.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqIdiomFormality : DecidableEq IdiomFormality

Equations

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

structure ConstructionGrammar.Studies.FillmoreKayOConnor1988.IdiomType : Type

Combined idiom classification.

• interpretability : IdiomInterpretability
• grammaticality : IdiomGrammaticality
• formality : IdiomFormality

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomType.repr : IdiomType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomType : Repr IdiomType

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomType = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprIdiomType.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instBEqIdiomType : BEq IdiomType

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instBEqIdiomType = { beq := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instBEqIdiomType.beq }

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instBEqIdiomType.beq : IdiomType → IdiomType → Bool

Equations

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

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.FamiliarityPattern : Type

Familiar-pieces typology (§1.2): how familiar are the pieces and their mode of combination?

• unfamiliarPiecesUnfamiliarlyArranged : FamiliarityPattern
• familiarPiecesUnfamiliarlyArranged : FamiliarityPattern
• familiarPiecesFamiliarlyArranged : FamiliarityPattern

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprFamiliarityPattern.repr : FamiliarityPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprFamiliarityPattern : Repr FamiliarityPattern

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprFamiliarityPattern = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprFamiliarityPattern.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqFamiliarityPattern : DecidableEq FamiliarityPattern

Equations

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

Section 2: Scalar Models (§2.3.2, Appendix)

The formal backbone of the paper: an n-dimensional scalar model with a monotonicity constraint on propositional functions.

Definition A3: (S, T, D^x, P) is a SCALAR MODEL iff, for distinct d_i, d_j in D^x, P(d_j) entails P(d_i) just in case d_i is LOWER than d_j.

Where "lower" means: d_i is lower than d_j iff no coordinate of d_i has a higher value than the corresponding coordinate of d_j, and at least one coordinate of d_i has a lower value (Definition A2).

structure ConstructionGrammar.Studies.FillmoreKayOConnor1988.ArgumentPoint (α : Type u_1) : Type u_1

An argument point in the n-dimensional argument space D^x. In the paper's example: (Apotheosis, English) is an argument point in the 2D space of linguists × languages.

• coordinates : List α

  Coordinates, one per dimension

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqArgumentPoint {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (ArgumentPoint α✝)

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqArgumentPoint = ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqArgumentPoint.decEq

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

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprArgumentPoint.repr {α✝ : Type u_1} [Repr α✝] : ArgumentPoint α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprArgumentPoint {α✝ : Type u_1} [Repr α✝] : Repr (ArgumentPoint α✝)

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprArgumentPoint = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprArgumentPoint.repr }

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

A scalar model (Definition A3 from the Appendix).

Given argument space D^x and propositional function P, the scalar model constrains P so that lower argument points yield weaker (entailed) propositions.

We use Bool for decidable propositions over states S.

• points : List (ArgumentPoint α)

  Argument points (elements of D^x)

• propFn : ArgumentPoint α → S → Bool

  Propositional function: argument point → proposition over states

• dimLe : α → α → Bool

  Ordering on individual dimension values

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

An argument point d_i is LOWER than d_j (Definition A2): no coordinate of d_i exceeds the corresponding coordinate of d_j, and at least one coordinate of d_i is strictly lower.

Equations

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

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

Scalar entailment: P(d_j) entails P(d_i) iff {s | P(d_j)(s)} ⊆ {s | P(d_i)(s)}.

In a valid scalar model, this holds exactly when d_i is lower than d_j.

Equations

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

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

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

Equations

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

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

Definition A3 validity: a scalar model satisfies the monotonicity constraint iff for all distinct argument points d_i, d_j in D^x, P(d_j) entails P(d_i) exactly when d_i is lower than d_j.

We check the forward direction (lower → entails) for all point pairs. This is the computable check used by native_decide.

Equations

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

Section 3: The Let Alone Construction (§2.1–2.4)

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.letAloneConstruction : Construction

The let alone construction as a Construction.

Form: F ⟨X A Y let alone B⟩

• F = negative polarity operator (negation, doubt, barely, etc.)
• X, Y = shared non-focused material
• A = first focused element (in the stronger, full clause)
• B = second focused element (in the weaker, reduced clause)
• A and B must be points on a presupposed scale

Equations

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

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

Semantic conditions on let alone sentences (p.528).

For a let alone sentence to be well-formed:

1. The full clause and reduced clause are propositions from the same scalar model
2. The two propositions are of the same polarity
3. The full clause proposition is stronger (more informative) than the reduced clause

• scalarModel : ScalarModel S α

  The presupposed scalar model

• focusA : ArgumentPoint α

  Argument point for the A focus (in the stronger clause)

• focusB : ArgumentPoint α

  Argument point for the B focus (in the weaker clause)

• aStrongerThanB : self.scalarModel.strongerThan self.focusA self.focusB

  A is stronger than B in the scalar model

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily : Type

The let alone family: related conjunctions with similar scalar semantics (p.533). All presuppose a scalar model relating their two conjuncts. They differ in clause ordering (stronger-first vs weaker-first).

• letAlone : LetAloneFamily
• muchLess : LetAloneFamily
• notToMention : LetAloneFamily
• neverMind : LetAloneFamily
• ifNot : LetAloneFamily
• inFact : LetAloneFamily

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneFamily : Repr LetAloneFamily

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneFamily = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneFamily.repr }

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneFamily.repr : LetAloneFamily → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLetAloneFamily : DecidableEq LetAloneFamily

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst : LetAloneFamily → Bool

Clause ordering: let alone presents the stronger proposition first, while if not and in fact present the weaker first (p.533).

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily.letAlone = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily.muchLess = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily.notToMention = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily.neverMind = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily.ifNot = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.presentsStrongerFirst ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneFamily.inFact = false

Section 4: NPI status (§2.2.4)

Let alone is a negative polarity item, but with nuances:

• It occurs in standard NPI environments (negation, doubt, barely, etc.)
• Some speakers accept it in positive contexts (p.519, exx.71-72)
• The NPI requirement may be pragmatic rather than purely syntactic

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.LetAloneNPITrigger : Type

NPI trigger types that license let alone (§2.2.4, exx.62-70).

• simpleNegation : LetAloneNPITrigger
• tooComplementation : LetAloneNPITrigger
• comparisonOfInequality : LetAloneNPITrigger
• onlyDeterminer : LetAloneNPITrigger
• minimalAttainment : LetAloneNPITrigger
• conditionalSurprise : LetAloneNPITrigger
• failureVerb : LetAloneNPITrigger
• anyoneWhod : LetAloneNPITrigger

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneNPITrigger.repr : LetAloneNPITrigger → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneNPITrigger : Repr LetAloneNPITrigger

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneNPITrigger = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLetAloneNPITrigger.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLetAloneNPITrigger : DecidableEq LetAloneNPITrigger

Equations

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

Section 5: Construction definitions for the constructicon

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.comparativeCorrelative : Construction

The X-er the Y-er comparative correlative (§1.2.1, exx.1-2).

A formal idiom with unfamiliar pieces unfamiliarly arranged. The definite article "the" is unique to this construction (p.507) — a fixed element — and the two-part structure has no parallel elsewhere in English. The open comparative phrases make it partially open (mix of fixed "the" and open comparatives).

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.incredulityResponse : Construction

The Incredulity Response construction (§1.1.4, ex.14h).

"Him be a doctor?" — non-nominative subject + bare stem verb, expressing incredulity. A formal idiom: the pattern (NP[acc] VP[bare]) is productive and dedicated to a rhetorical/evaluative pragmatic function not derivable from its component meanings.

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.letAloneInheritance : InheritanceLink

Inheritance: let alone inherits from coordinating conjunction but overrides several properties.

Equations

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

Section 6: 1D Scalar Model — Military Ranks (§2.1, ex.21)

The running example: ⟨second lieutenant,..., colonel, general⟩.

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank : Type

Military ranks from the paper's running example.

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

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

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprRank : Repr Rank

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqRank : DecidableEq Rank

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instFintypeRank : Fintype Rank

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe : Rank → Rank → Bool

Rank ordering (lower index = lower rank).

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.secondLieutenant x✝ = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.lieutenant x✝ = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.captain x✝ = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.major ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.colonel = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.major ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.general = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.major ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.major = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.major x✝ = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.colonel x✝ = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankLe ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.general x✝ = false

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.AchievementState : Type

States: whether a person achieved each rank.

• achievedNone : AchievementState
• achievedUpToLt : AchievementState
• achievedUpToCol : AchievementState
• achievedUpToGen : AchievementState

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprAchievementState.repr : AchievementState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprAchievementState : Repr AchievementState

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprAchievementState = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprAchievementState.repr }

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqAchievementState : DecidableEq AchievementState

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instFintypeAchievementState : Fintype AchievementState

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank : Rank → AchievementState → Bool

"He made rank R" is true in a state iff the state includes R.

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.secondLieutenant x✝ = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.lieutenant x✝ = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.captain x✝ = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.major x✝ = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.colonel x✝ = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.madeRank ConstructionGrammar.Studies.FillmoreKayOConnor1988.Rank.general x✝ = false

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.rankScalarModel : ScalarModel AchievementState Rank

The military rank scalar model.

Equations

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

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.rank_model_valid : rankScalarModel.satisfiesA3 [AchievementState.achievedNone, AchievementState.achievedUpToLt, AchievementState.achievedUpToCol, AchievementState.achievedUpToGen] = true

The rank scalar model satisfies Definition A3: for every pair of points where d_i is lower than d_j, P(d_j) entails P(d_i).

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.rank_model_is_1d : (rankScalarModel.points.all fun (p : ArgumentPoint Rank) => p.coordinates.length == 1) = true

The rank scalar model is one-dimensional: every argument point has exactly one coordinate. The paper argues (fn.16, p.535) that some examples require ≥2 dimensions.

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.general_entails_colonel : rankScalarModel.entails { coordinates := [Rank.general] } { coordinates := [Rank.colonel] }

Scalar entailment: "He made general" entails "He made colonel". This is the core semantic condition on let alone (p.523, 528): the stronger (A) proposition entails the weaker (B) proposition.

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.colonel_entails_lieutenant : rankScalarModel.entails { coordinates := [Rank.colonel] } { coordinates := [Rank.lieutenant] }

Scalar entailment: "He made colonel" entails "He made lieutenant".

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.colonel_does_not_entail_general : ¬rankScalarModel.entails { coordinates := [Rank.colonel] } { coordinates := [Rank.general] }

The reverse does NOT hold: "He made colonel" does not entail "He made general". This is why "He didn't make colonel, let alone general" is felicitous — general is STRONGER (p.528).

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.general_stronger_than_colonel : rankScalarModel.strongerThan { coordinates := [Rank.general] } { coordinates := [Rank.colonel] }

Making general is STRONGER than making colonel: the extension of "made general" is a proper subset of "made colonel" (Definition A5).

theorem ConstructionGrammar.Studies.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 other rank is lower. This explains the anomaly in ex.107: "let alone a second lieutenant" is anomalous because you cannot scalar-entail the negation of the lowest point from the negation of a non-lowest point (p.526).

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.ex21_scalar_condition_neg (s : AchievementState) : madeRank Rank.general s = true → madeRank Rank.colonel s = true

The rank scalar model validates FKO's ex.21: "He didn't make colonel, let alone general."

Under negation, the scalar direction reverses: "not make colonel" entails "not make general" (if you can't do the easier thing, you can't do the harder thing).

Section 7: 2D Scalar Model — Linguists × Languages (§2.3.2, Tables 1–4)

The paper's most carefully developed example: four professors (Apotheosis, Brilliant, Competent, Dimm) and four languages (English, French, Greek, Hittite), ordered by erudition and accessibility respectively.

The propositional function P: "professor X can read language L" is monotone: if X is more erudite and L is more accessible, P is more likely to be true.

This 2D model is the basis for the Appendix definitions (A1–A5).

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.Linguist : Type

Linguists ordered by erudition (most → least).

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

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

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLinguist : Repr Linguist

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLinguist : DecidableEq Linguist

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instFintypeLinguist : Fintype Linguist

Equations

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

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.Lang : Type

Languages ordered by accessibility (most → least).

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLang : Repr Lang

Equations

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

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

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLang : DecidableEq Lang

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instFintypeLang : Fintype Lang

Equations

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

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.LingLangVal : Type

Dimension value: either a linguist or a language. The argument space D^x = Linguist × Lang, encoded as 2-element coordinate lists of LingLangVal.

• ling : Linguist → LingLangVal
• lang : Lang → LingLangVal

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLingLangVal.repr : LingLangVal → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLingLangVal : Repr LingLangVal

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLingLangVal = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLingLangVal.repr }

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq (x✝ x✝¹ : LingLangVal) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLingLangVal : DecidableEq LingLangVal

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLingLangVal = ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLingLangVal.decEq

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.lingLangLe : LingLangVal → LingLangVal → Bool

Dimension ordering (≤) for the linguist/language scalar model.

From Definition A2 (p.536) and the worked example on p.537: d_i is LOWER than d_j when d_i has coordinatewise ≤ values with at least one strict. A LOWER argument point yields a WEAKER proposition (true in more states).

• Linguist: Apotheosis ≤ Brilliant ≤ Competent ≤ Dimm (more erudite = LOWER = weaker — "Apotheosis reads L" is easiest to satisfy)
• Language: English ≤ French ≤ Greek ≤ Hittite (more accessible = LOWER = weaker — "X reads English" is easiest to satisfy)

The paper confirms (p.537): "(B, E) is lower than (B, G)" — Brilliant with English is lower than Brilliant with Greek. Cross-type comparisons return false (dimensions are independent).

Equations

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

inductive ConstructionGrammar.Studies.FillmoreKayOConnor1988.LLState : Type

States of affairs for the linguist/language model. Each state specifies which (linguist, language) pairs satisfy "X can read L". We use a few representative states from Table 2 in the paper (p.527).

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLLState : Repr LLState

Equations

• ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLLState = { reprPrec := ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLLState.repr }

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.instReprLLState.repr : LLState → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instDecidableEqLLState : DecidableEq LLState

Equations

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

@[implicit_reducible]

instance ConstructionGrammar.Studies.FillmoreKayOConnor1988.instFintypeLLState : Fintype LLState

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.canRead : Linguist → Lang → LLState → Bool

"Professor X can read language L" in each state. The diagonal state is the paper's primary example: knowledge forms a staircase from the 1-corner (Apotheosis, English) outward.

Equations

• One or more equations did not get rendered due to their size.
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.canRead x✝¹ x✝ ConstructionGrammar.Studies.FillmoreKayOConnor1988.LLState.allFalse = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.canRead x✝¹ x✝ ConstructionGrammar.Studies.FillmoreKayOConnor1988.LLState.allTrue = true
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.canRead x✝¹ x✝ ConstructionGrammar.Studies.FillmoreKayOConnor1988.LLState.topLeft = false
• ConstructionGrammar.Studies.FillmoreKayOConnor1988.canRead x✝¹ x✝ ConstructionGrammar.Studies.FillmoreKayOConnor1988.LLState.twoTrue = false

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.llPoint (l : Linguist) (lang : Lang) : ArgumentPoint LingLangVal

Convenience constructor for 2D argument points.

Equations

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

def ConstructionGrammar.Studies.FillmoreKayOConnor1988.linguistLangModel : ScalarModel LLState LingLangVal

The linguist/language scalar model from §2.3.2 (Tables 1–4, p.526–527).

Equations

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

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.ll_model_is_2d : (linguistLangModel.points.all fun (p : ArgumentPoint LingLangVal) => p.coordinates.length == 2) = true

The linguist/language model is two-dimensional.

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.ll_model_valid : linguistLangModel.satisfiesA3 [LLState.allFalse, LLState.topLeft, LLState.twoTrue, LLState.allTrue, LLState.diagonal] = true

The 2D model satisfies Definition A3.

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.brilliant_hittite_entails_english : linguistLangModel.entails (llPoint Linguist.brilliant Lang.hittite) (llPoint Linguist.brilliant Lang.english)

In the 2D model, "Brilliant can read Hittite" entails "Brilliant can read English" — Hittite is less accessible, so knowing it is stronger (p.528, exx.109–112).

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.brilliant_hittite_stronger_than_competent_french : linguistLangModel.strongerThan (llPoint Linguist.brilliant Lang.hittite) (llPoint Linguist.competent Lang.french)

"Brilliant can read Hittite" is stronger than "Competent can read French" (Definition A5). Note: these points are INCOMPARABLE in the partial order (Brilliant < Competent on linguist, Hittite > French on language), but the entailment holds empirically — the scalar model constrains more than just comparable pairs.

theorem ConstructionGrammar.Studies.FillmoreKayOConnor1988.brilliant_english_lower_than_brilliant_greek : ArgumentPoint.isLower lingLangLe (llPoint Linguist.brilliant Lang.english) (llPoint Linguist.brilliant Lang.greek) = true

(Brilliant, English) is lower than (Brilliant, Greek): the paper's own worked example (p.537). Same linguist, but English is more accessible (lower) than Greek.

theorem ConstructionGrammar.Studies.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: Competent > Brilliant on linguist but French < Hittite on language. Neither is uniformly ≤ the other (Definition A2).