Büring 2007: Cross-Polar Nomalies

[Bur07]

Daniel Büring. Cross-Polar Nomalies. SALT 17 (2007).

Core Puzzle

Cross-polar anomalies — comparisons pairing A⁺ with its direct antonym A⁻ — are ungrammatical: *"John is shorter than Mary is tall." But cross-polar nomalies — comparisons pairing A⁻ with a non-antonymous A⁺ from a different spatial dimension — are perfectly acceptable: "The ladder was shorter than the house was high."

Analysis

LITTLE is a degree negation operator ([Hei06]): short = LITTLE long, less = LITTLE -er. Formally, LITTLE complements a degree predicate: ⟦LITTLE⟧ = λi.λd. i(d) = 0, mapping positive extents to negative extents ([Ken99]).

Cross-polar nomalies work because MORE LITTLE-A in the main clause can be reinterpreted as LITTLE-er A. This reinterpretation is blocked for direct antonyms by comparative deletion (MaxElide) and for inverse configurations by the requirement that LITTLE license ellipsis only in its own clause.

Three-way pattern:

• Cross-polar anomaly: *A⁺-er than A⁻ / *A⁻-er than A⁺ (direct antonyms) — BAD
• Cross-polar nomaly: A⁻-er than A⁺ (different dimensions) — OK
• Inverse nomaly: *A⁺-er than A⁻ (different dimensions) — BAD

Two Competing Analyses (§3 vs §5)

• Analysis 1 (§3–4, preferred): LITTLE sits with -er in the main clause. "shorter than high" = LITTLE-er long than HOW the house is high. The degree negation scopes with the comparative morpheme.

• Analysis 2 (§5): A second LITTLE appears in the than-clause, turning high into LITTLE-high (= low). The main-clause LITTLE is then elided under identity with the than-clause LITTLE (comparative subdeletion).

Both predict the same truth conditions for basic cases. §6 uses modal scope as a diagnostic: universal/existential modals in the than-clause disambiguate the two, favoring Analysis 1.

Formal Connections

• LITTLE as extent complement: littlePred maps Set.Iic to Set.Ioi, connecting to [Ken99]'s extent algebra in Degree.
• Cross-polar anomaly = algebraic impossibility: same-dimension cross-polar comparison requires crossExtentInclusion, which Degree.not_crossExtentInclusion proves is impossible on any linear order.
• Cross-polar nomaly = subcomparative: different-dimension comparison is subcomparative from [SW02a].
• Klein limitation bridge: [vS84]'s Klein limitation 3 ("Ede is more tall than broad") is exactly a subcomparative.

LITTLE: degree negation [Hei06]

Absorbed from the retired Degree/Little.lean (Büring is its only consumer): ⟦LITTLE⟧ = λP.λd. ¬ P d; short = LITTLE tall, less = LITTLE -er.

def Buring2007.littlePred {D : Type u_1} (P : D → Prop) : D → Prop

LITTLE on degree predicates: complementation.

Equations

• Buring2007.littlePred P d = ¬P d

theorem Buring2007.littlePred_Iic_eq_Ioi {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (x : Entity) (d : D) : littlePred (fun (x_1 : D) => x_1 ∈ Set.Iic (μ x)) d ↔ d ∈ Set.Ioi (μ x)

LITTLE maps the positive extent to the negative extent: LITTLE({d | d ≤ μ(x)}) = {d | μ(x) < d}. The formal content of "short = LITTLE tall" — the degree predicate for 'short' is the complement of the degree predicate for 'tall', exactly the relation between positive and negative extents from [Ken99].

theorem Buring2007.little_involution {D : Type u_1} (P : D → Prop) (d : D) : littlePred (littlePred P) d ↔ P d

LITTLE is an involution: double degree negation cancels.

theorem Buring2007.little_reverses_comparison {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive ↔ Degree.comparativeSem μ b a Core.Order.ScalePolarity.negative

LITTLE reverses the comparison direction: "A is LITTLE-er Adj than B" ↔ "B is Adj-er than A". Delegates to taller_shorter_antonymy.

def Buring2007.positiveInterval {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) : NonemptyInterval D

Schwarzschild-style positive interval [⊥, μ x] — the bundled (NonemptyInterval) face of Set.Iic (μ x).

Equations

• Buring2007.positiveInterval μ x = { fst := ⊥, snd := μ x, fst_le_snd := ⋯ }

def Buring2007.negativeInterval {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) : NonemptyInterval D

Negative interval [μ x, ⊤] (§4: ⟦short⟧ = ⟦LITTLE tall⟧ inverts the positive interval) — the bundled face of Set.Ioi (μ x).

Equations

• Buring2007.negativeInterval μ x = { fst := μ x, snd := ⊤, fst_le_snd := ⋯ }

LITTLE: Degree Negation on Extents

theorem Buring2007.little_positive_to_negative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) : (negativeInterval μ x).toProd.1 = (positiveInterval μ x).toProd.2

LITTLE maps positive intervals to negative intervals ([Bur07] §4, def. 22): the positive interval [⊥, μ(x)] becomes the negative interval [μ(x), ⊤]. This is the interval-level counterpart of littlePred_Iic_eq_Ioi (which operates on extent sets).

The bridge connects the interval framework (Schwarzschild) to the extent framework (Kennedy) via LITTLE.

Cross-Polar Anomaly: Algebraic Impossibility

theorem Buring2007.crossPolar_anomaly_impossible {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : ¬Degree.crossExtentInclusion μ a b

Cross-polar anomaly = attempting to compare a positive extent with a negative extent on the same dimension.

"?*John is shorter than Mary is tall" requires Iic(μ Mary) ⊆ Ioi(μ John), but Degree.not_crossExtentInclusion from [Ken99]'s extent algebra proves this is impossible on any linear order: the boundary degree μ(a) belongs to the positive extent but not the negative one, so the inclusion always fails.

Note: [Bur07]'s explanation is syntactic (MaxElide §3.2), not algebraic. The algebraic impossibility is a stronger claim: even if the LF were syntactically available, the semantics would be vacuous. Büring's account is compatible — MaxElide blocks the LF before semantics applies.

Cross-Polar Pattern (Data)

inductive Buring2007.CrossPolarType : Type

Classification of cross-polar configurations (p. 3).

• anomaly : CrossPolarType
• nomaly : CrossPolarType
• inverseNomaly : CrossPolarType

@[instance_reducible]

instance Buring2007.instDecidableEqCrossPolarType : DecidableEq CrossPolarType

Equations

• Buring2007.instDecidableEqCrossPolarType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Buring2007.instReprCrossPolarType.repr : CrossPolarType → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Buring2007.instReprCrossPolarType : Repr CrossPolarType

Equations

• Buring2007.instReprCrossPolarType = { reprPrec := Buring2007.instReprCrossPolarType.repr }

structure Buring2007.CrossPolarDatum : Type

• sentence : String
• classification : CrossPolarType
• grammatical : Bool

def Buring2007.instReprCrossPolarDatum.repr : CrossPolarDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Buring2007.instReprCrossPolarDatum : Repr CrossPolarDatum

Equations

• Buring2007.instReprCrossPolarDatum = { reprPrec := Buring2007.instReprCrossPolarDatum.repr }

def Buring2007.crossPolarData : List CrossPolarDatum

Equations

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

Cross-Polar Nomalies = Subcomparatives

theorem Buring2007.subcomparative_same_dimension {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (a b : Entity) : Degree.subcomparative μ μ a b ↔ Degree.comparativeSem μ a b Core.Order.ScalePolarity.positive

When both dimensions use the same measure function, the subcomparative collapses to the standard comparative: "a is shorter than b" = "b is taller than a".

Concrete Example

@[instance_reducible]

instance Buring2007.instDecidableEqThing : DecidableEq Buring2007.Thing✝

Equations

• Buring2007.instDecidableEqThing x✝ y✝ = if h : Buring2007.Thing.ctorIdx✝ x✝ = Buring2007.Thing.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Buring2007.instReprThing : Repr Buring2007.Thing✝

Equations

• Buring2007.instReprThing = { reprPrec := Buring2007.instReprThing.repr }

def Buring2007.instReprThing.repr : Buring2007.Thing✝ → ℕ → Std.Format

Equations

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

Why Anomalies Are Blocked

structure Buring2007.AnomalyBlockingDatum : Type

[Bur07]'s syntactic explanation for why direct-antonym cross-polar constructions are anomalous (§3.2): when A⁻ and A⁺ ARE direct antonyms (same dimension), comparative deletion (ellipsis of the whole A in the than-clause) produces a competing form. MaxElide (Takahashi and Fox 2005) prefers this deletion, blocking the cross-polar LF.

For nomalies, deletion is unavailable because the adjectives differ (long ≠ high), so no competition arises (§3.3).

Inverse nomalies (*A⁺-er than A⁻, different dimensions) are blocked because LITTLE in the main clause cannot license ellipsis in the than-clause (§3.4): the LF "the house is MORE high [than HOW the ladder is LITTLE-long]" cannot be reinterpreted as "LITTLE-er high" because LITTLE and MORE are in separate clauses.

• sentence : String
• whyBlocked : String
• competingForm : String

def Buring2007.instReprAnomalyBlockingDatum.repr : AnomalyBlockingDatum → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Buring2007.instReprAnomalyBlockingDatum : Repr AnomalyBlockingDatum

Equations

• Buring2007.instReprAnomalyBlockingDatum = { reprPrec := Buring2007.instReprAnomalyBlockingDatum.repr }

def Buring2007.anomalyBlocking : List AnomalyBlockingDatum

Equations

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

Bridge to Von Stechow's Klein Limitation

theorem Buring2007.klein_limitation_is_subcomparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ₁ μ₂ : Entity → D) (a : Entity) : Degree.subcomparative μ₁ μ₂ a a ↔ μ₁ a > μ₂ a

[vS84]'s Klein limitation 3: "Ede is more tall than broad" is a cross-dimensional comparison that Klein's degree-free framework cannot express.

[Bur07]'s cross-polar nomalies are the same phenomenon: "shorter(length) than high(height)" compares different dimensions on a shared spatial extent scale. Both require degree ontology (specifically, subcomparative from [SW02a]).

Definitionally: comparing two dimensions of the same entity is subcomparative μ₁ μ₂ a a, which unfolds to μ₁ a > μ₂ a.

LITTLE–□ scope: the de Morgan asymmetry (§6)

The two analyses place LITTLE on opposite sides of the than-clause modal, so the than-clause degree property is either LITTLE(□P) or □(LITTLE P). Over accessible worlds acc with world-indexed degree μw, a degree d is in LITTLE(□P) iff it exceeds some world's degree (it escapes the minimum), and in □(LITTLE P) iff it exceeds every world's degree (it escapes the maximum). □∘LITTLE entails LITTLE∘□ — the nontrivial direction of de Morgan for infinite meets — but not conversely, which is why the modal diagnostic below discriminates the two analyses.

def Buring2007.littleOverBox {W : Type u_1} {D : Type u_2} [LT D] (acc : Set W) (μw : W → D) (d : D) : Prop

LITTLE(□P): d exceeds the degree of some accessible world.

Equations

• Buring2007.littleOverBox acc μw d = ∃ w ∈ acc, μw w < d

def Buring2007.boxOverLittle {W : Type u_1} {D : Type u_2} [LT D] (acc : Set W) (μw : W → D) (d : D) : Prop

□(LITTLE P): d exceeds the degree of every accessible world.

Equations

• Buring2007.boxOverLittle acc μw d = ∀ w ∈ acc, μw w < d

theorem Buring2007.boxOverLittle_implies_littleOverBox {W : Type u_1} {D : Type u_2} [LT D] {acc : Set W} (μw : W → D) (d : D) (hne : acc.Nonempty) : boxOverLittle acc μw d → littleOverBox acc μw d

□(LITTLE P) entails LITTLE(□P) when some world is accessible: the nontrivial de Morgan direction.

theorem Buring2007.littleOverBox_not_boxOverLittle : ∃ (acc : Set Bool) (μw : Bool → ℚ) (d : ℚ), littleOverBox acc μw d ∧ ¬boxOverLittle acc μw d

The converse fails: over two worlds with degrees 5 and 10, the degree 7 escapes the minimum but not the maximum.

theorem Buring2007.littleBox_collapse_when_uniform {W : Type u_1} {D : Type u_2} [LT D] {acc : Set W} (μw : W → D) (d : D) (hne : acc.Nonempty) (hunif : ∀ w₁ ∈ acc, ∀ w₂ ∈ acc, μw w₁ = μw w₂) : littleOverBox acc μw d ↔ boxOverLittle acc μw d

When all accessible worlds agree on the degree, the two analyses collapse — modal scope is undetectable ([Hei01]'s monotone collapse at the modal level).

Modal Scope Diagnostic (§6)

@[instance_reducible]

instance Buring2007.instDecidableEqCastlePart : DecidableEq Buring2007.CastlePart✝

Equations

• Buring2007.instDecidableEqCastlePart x✝ y✝ = if h : Buring2007.CastlePart.ctorIdx✝ x✝ = Buring2007.CastlePart.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Buring2007.instReprCastlePart : Repr Buring2007.CastlePart✝

Equations

• Buring2007.instReprCastlePart = { reprPrec := Buring2007.instReprCastlePart.repr }

def Buring2007.instReprCastlePart.repr : Buring2007.CastlePart✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Buring2007.instDecidableEqPermittedWorld : DecidableEq Buring2007.PermittedWorld✝

Equations

• Buring2007.instDecidableEqPermittedWorld x✝ y✝ = if h : Buring2007.PermittedWorld.ctorIdx✝ x✝ = Buring2007.PermittedWorld.ctorIdx✝ y✝ then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Buring2007.instReprPermittedWorld : Repr Buring2007.PermittedWorld✝

Equations

• Buring2007.instReprPermittedWorld = { reprPrec := Buring2007.instReprPermittedWorld.repr }

def Buring2007.instReprPermittedWorld.repr : Buring2007.PermittedWorld✝ → ℕ → Std.Format

Equations

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

def Buring2007.analysis1_minRequiredWidth : ℚ

Analysis 1 (preferred): LITTLE scopes with -er in main clause. The than-clause denotes {d | ∀w ∈ Deon(@). d ≤ WIDTH_w(moat)}, whose max is the minimum required width (= 30). The comparative asserts: min-required-width > bridge-length.

Truth conditions: the bridge is shorter than the moat's minimum required width. This is correct — the bridge (15ft) can't span a moat that must be at least 30ft wide.

Equations

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

theorem Buring2007.analysis1_correct : analysis1_minRequiredWidth > Buring2007.bridgeLength✝

def Buring2007.analysis2_maxPermittedNarrowness (maxWidth : ℚ) : ℚ

Analysis 2: LITTLE scopes in the than-clause (with the adjective). HAS-TO scopes over LITTLE-wide (= narrow). The than-clause denotes {d | ∀w ∈ Deon(@). NARROWNESS_w(moat) ≥ d}, whose max is the min narrowness across permitted worlds — i.e., the narrowness in the world where the moat is widest (= 40ft → narrowness is minimal).

On a bounded scale [0, maxWidth], narrowness = maxWidth - width. Min narrowness = maxWidth - max(width) = maxWidth - 40. For any reasonable maxWidth, this is smaller than bridge shortness.

Truth conditions: we could (but don't have to) build a moat narrow enough that the bridge would span it. This does NOT match the intuition of (29), which asserts the bridge is too short, period.

Equations

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

theorem Buring2007.analysis2_wrong_at_50 : ¬analysis2_maxPermittedNarrowness 50 > Buring2007.bridgeLength✝

Analysis 2 predicts narrowness of (maxWidth - 40). For any reasonable maxWidth (e.g. 50), this is 10 — less than the bridge length of 15. So Analysis 2 would predict the sentence is FALSE (the bridge IS long enough for the widest-possible moat-narrowness). This is the wrong prediction.

theorem Buring2007.analyses_diverge : analysis1_minRequiredWidth > Buring2007.bridgeLength✝ ∧ ¬analysis2_maxPermittedNarrowness 50 > Buring2007.bridgeLength✝

The two analyses diverge: Analysis 1 predicts TRUE (bridge too short), Analysis 2 predicts FALSE (bridge long enough). Native speakers judge the sentence true, confirming Analysis 1.

Existential Modal Variant (§6.2)

structure Buring2007.ModalNomalyDatum : Type

[Bur07] §6.2 (p. 14, ex. 38): existential modals produce the same disambiguation.

"The moat is narrower than drawbridges are allowed to be long."

Analysis 1: moat width < max permitted bridge length. Paraphrase: "we can get a bridge that spans the moat."

Analysis 2: moat narrowness < max permitted bridge shortness. Paraphrase: weaker — about permitted shortness, not length.

• sentence : String
• modalForce : String
• analysis1Reading : String
• analysis2Reading : String
• nativeSpeakerMatch : Bool

@[instance_reducible]

instance Buring2007.instReprModalNomalyDatum : Repr ModalNomalyDatum

Equations

• Buring2007.instReprModalNomalyDatum = { reprPrec := Buring2007.instReprModalNomalyDatum.repr }

def Buring2007.instReprModalNomalyDatum.repr : ModalNomalyDatum → ℕ → Std.Format

Equations

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

def Buring2007.modalDiagnosticData : List ModalNomalyDatum

Equations

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