Büring 2007: cross-polar nomalies

Comparatives pairing a positive adjective with a negative one are anomalous — John is shorter than Mary is tall — and yet the ladder was shorter than the house was high is perfectly acceptable. This file formalizes the account of the contrast. A negative adjective is the degree negation of its positive counterpart, and a comparative whose degree phrase carries that negation inverts both intervals it compares, so shorter than … high can be read as less long than … high. Read that way it compares two positive extents; read literally it compares a positive extent with a negative one, which no scale makes true, while the reinterpretation is a subcomparative.

The reinterpretation needs the negation and the comparative morpheme in one clause, and it is preempted where the than-clause adjective is the matrix one modulo the negation, since comparative deletion then supplies a synonymous competitor. Those two conditions cut the cross-polar space into the paper's three cases, and they block for different reasons: the anomaly has the reinterpretation available and loses to its competitor, the inverse nomaly has no competitor and still fails.

A modal in the than-clause separates this account from the variant that puts the degree negation with the than-clause adjective. The negation outside the modal and the negation inside it turn the same comparison into the box and the diamond of one proposition, so the first is the stronger reading under a universal modal and the weaker one under an existential; they coincide only when the accessible worlds agree on the standard's degree.

Main definitions

• compareWith — the comparative morpheme, relative to the modifier in its degree phrase
• Comparative, Comparative.Acceptable — a cross-polar comparative and the conditions on it
• negationOutside, negationInside — the two analyses of a modal than-clause

Main results

• compareWith_little — the degree negation inverts both intervals compared
• not_crossPolar, not_crossPolar' — neither order of a literal cross-polar comparison is true
• metamorphosis_iff_subcomparative — the reinterpretation is a subcomparative
• nomaly_acceptable, blocked_for_different_reasons — the three-way pattern and its two sources
• reading_of_deletion — the deletion competitor is synonymous exactly on one dimension
• negationOutside_box, negationInside_box — the two analyses as box and diamond
• outside_entails_inside_box, inside_not_entails_outside — the entailment is strict
• analyses_agree_of_uniform — a degree-uniform modal base hides the difference

References

• [Bur07]
• [Hei06]
• [Ken99]
• [Ken01]
• [Rul95]
• [SW02a]
• [TF05]

The comparative and the degree negation

def Buring2007.compareWith {D : Type u_1} (m : Set D → Set D) (thanClause matrix : Set D) : Prop

The comparative morpheme compareWith m i j holds when the than-clause interval i is properly included in the matrix interval j, both read through the degree-phrase modifier m, the identity for MUCH and complementation for LITTLE.

Equations

• Buring2007.compareWith m thanClause matrix = (m thanClause ⊂ m matrix)

theorem Buring2007.compareWith_little {D : Type u_1} (i j : Set D) : compareWith compl i j ↔ j ⊂ i

LITTLE turns a more-comparative into a less-comparative by inverting both intervals compared: less is LITTLE -er ([Hei06]).

theorem Buring2007.not_crossPolar {D : Type u_1} [LinearOrder D] (a b : D) : ¬compareWith id (Set.Iic a) (Set.Ioi b)

A positive extent is never properly included in a negative one, so the literal reading of Mary is taller than John is short is true on no scale ([Ken01]).

theorem Buring2007.not_crossPolar' {D : Type u_1} [LinearOrder D] [NoMaxOrder D] (a b : D) : ¬compareWith id (Set.Ioi a) (Set.Iic b)

The other order fails too whenever the scale has no greatest degree: John is shorter than Mary is tall read literally would need every degree above John's height to lie below Mary's.

theorem Buring2007.metamorphosis_iff_subcomparative {D : Type u_1} [LinearOrder D] {Entity : Type u_2} (μ₁ μ₂ : Entity → D) (a b : Entity) : compareWith compl (Set.Iic (μ₁ a)) (Set.Iic (μ₂ b)) ↔ μ₂ b < μ₁ a

Under the reinterpretation, with the negation in the degree phrase, both intervals compared are positive extents, and the comparison is the subcomparative of [SW02a], the ladder's length against the house's height.

The three cross-polar configurations

inductive Buring2007.Dimension : Type

The paper's examples measure spatial dimensions, the one scale carrying measurements in more than one dimension, which is why cross-polar nomalies are confined to it.

• length : Dimension
• height : Dimension
• width : Dimension
• depth : Dimension

@[instance_reducible]

instance Buring2007.instDecidableEqDimension : DecidableEq Dimension

Equations

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

@[instance_reducible]

instance Buring2007.instReprDimension : Repr Dimension

Equations

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

def Buring2007.instReprDimension.repr : Dimension → ℕ → Std.Format

Equations

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

structure Buring2007.Adjective : Type

An adjective pairs a dimension with a polarity, measuring it positively (long) or negatively (short).

• dimension : Dimension
• polarity : Polarity

@[instance_reducible]

instance Buring2007.instDecidableEqAdjective : DecidableEq Adjective

Equations

• Buring2007.instDecidableEqAdjective = Buring2007.instDecidableEqAdjective.decEq

def Buring2007.instDecidableEqAdjective.decEq (x✝ x✝¹ : Adjective) : Decidable (x✝ = x✝¹)

Equations

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

def Buring2007.instReprAdjective.repr : Adjective → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Buring2007.instReprAdjective : Repr Adjective

Equations

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

structure Buring2007.Comparative : Type

A comparative pairing a matrix adjective with a than-clause adjective.

• matrix : Adjective
• thanClause : Adjective

def Buring2007.instDecidableEqComparative.decEq (x✝ x✝¹ : Comparative) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Buring2007.instDecidableEqComparative : DecidableEq Comparative

Equations

• Buring2007.instDecidableEqComparative = Buring2007.instDecidableEqComparative.decEq

def Buring2007.instReprComparative.repr : Comparative → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Buring2007.instReprComparative : Repr Comparative

Equations

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

def Buring2007.Comparative.CrossPolar (c : Comparative) : Prop

A comparative is cross-polar when its two adjectives are of opposite polarity.

Equations

• c.CrossPolar = (c.matrix.polarity ≠ c.thanClause.polarity)

def Buring2007.Comparative.Metamorphosis (c : Comparative) : Prop

The reinterpretation is available only where the degree negation and the comparative morpheme share a clause, that is where the negative adjective is the matrix one: a than-clause negation cannot be recombined with the matrix comparative.

Equations

• c.Metamorphosis = (c.matrix.polarity = Polarity.negative)

def Buring2007.Comparative.Deletion (c : Comparative) : Prop

Comparative deletion is licensed where the than-clause adjective phrase is the matrix one modulo the degree morphology, that is where the two adjectives measure the same dimension.

Equations

• c.Deletion = (c.matrix.dimension = c.thanClause.dimension)

def Buring2007.Comparative.Acceptable (c : Comparative) : Prop

A cross-polar comparative survives when the reinterpretation is available and no comparative deletion competes with it ([TF05]'s MaxElide prefers the larger ellipsis).

Equations

• c.Acceptable = (c.Metamorphosis ∧ ¬c.Deletion)

@[instance_reducible]

instance Buring2007.Comparative.instDecidableCrossPolar (c : Comparative) : Decidable c.CrossPolar

Equations

• c.instDecidableCrossPolar = { decide := !decide (c.matrix.polarity = c.thanClause.polarity), reflects_decide := ⋯ }

@[instance_reducible]

instance Buring2007.Comparative.instDecidableMetamorphosis (c : Comparative) : Decidable c.Metamorphosis

Equations

• c.instDecidableMetamorphosis = Buring2007.Comparative.instDecidableMetamorphosis._aux_1 c

@[instance_reducible]

instance Buring2007.Comparative.instDecidableDeletion (c : Comparative) : Decidable c.Deletion

Equations

• c.instDecidableDeletion = Buring2007.Comparative.instDecidableDeletion._aux_1 c

@[instance_reducible]

instance Buring2007.Comparative.instDecidableAcceptable (c : Comparative) : Decidable c.Acceptable

Equations

• c.instDecidableAcceptable = { decide := decide c.Metamorphosis && decide ¬c.Deletion, reflects_decide := ⋯ }

def Buring2007.Comparative.reading {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (m : Dimension → Entity → D) (c : Comparative) (subject standard : Entity) : Prop

The reading a cross-polar comparative gets under the reinterpretation, on a model interpreting each dimension as a measure function.

Equations

• Buring2007.Comparative.reading m c subject standard = (m c.matrix.dimension subject < m c.thanClause.dimension standard)

def Buring2007.anomaly : Comparative

In John is shorter than Mary is tall the negative adjective is the matrix one and both measure height.

Equations

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

def Buring2007.reverseAnomaly : Comparative

In Mary is taller than John is short the negation sits in the than-clause.

Equations

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

def Buring2007.nomaly : Comparative

In The ladder was shorter than the house was high the negative adjective is the matrix one and the two dimensions differ.

Equations

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

def Buring2007.inverseNomaly : Comparative

In The house is higher than the ladder is short the dimensions differ, but the negation is in the than-clause.

Equations

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

theorem Buring2007.configurations_crossPolar : anomaly.CrossPolar ∧ reverseAnomaly.CrossPolar ∧ nomaly.CrossPolar ∧ inverseNomaly.CrossPolar

All four configurations are cross-polar, so the acceptability condition applies to each.

theorem Buring2007.nomaly_acceptable : nomaly.Acceptable

The nomaly is reinterpretable and has no deletion competitor.

theorem Buring2007.others_unacceptable : ¬anomaly.Acceptable ∧ ¬reverseAnomaly.Acceptable ∧ ¬inverseNomaly.Acceptable

The anomaly, its reverse and the inverse nomaly are all blocked.

theorem Buring2007.blocked_for_different_reasons : anomaly.Metamorphosis ∧ anomaly.Deletion ∧ ¬inverseNomaly.Metamorphosis ∧ ¬inverseNomaly.Deletion

Neither condition derives the pattern alone: the anomaly is reinterpretable and blocked only by its competitor, the inverse nomaly has no competitor and is blocked only by the position of the negation.

theorem Buring2007.reading_of_deletion {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (m : Dimension → Entity → D) (c : Comparative) (h : c.Deletion) (subject standard : Entity) : Comparative.reading m c subject standard ↔ m c.matrix.dimension subject < m c.matrix.dimension standard

Comparative deletion competes only where it is synonymous: on one dimension the reinterpreted reading is exactly the plain comparative the deletion form expresses, which is why the anomaly loses to it while the nomaly — whose deletion form makes a different claim — does not.

theorem Buring2007.reading_not_synonymous : ∃ (m : Dimension → Bool → ℕ) (subject : Bool) (standard : Bool), Comparative.reading m nomaly subject standard ∧ ¬m Dimension.length subject < m Dimension.length standard

With two dimensions the deletion form is not a paraphrase, so it does not compete: a 12-foot ladder is shorter than a 15-foot-high house without being shorter than the house is long.

A modal in the than-clause

def Buring2007.negationOutside {W : Type u_1} {D : Type u_2} [LinearOrder D] (Q : (W → Prop) → Prop) (μ : W → D) (c : D) : Prop

With the degree negation outside the modal, the than-clause denotes the degrees the standard reaches under the modal, and the less-comparative asserts that the subject's positive extent is included in it.

Equations

• Buring2007.negationOutside Q μ c = (Set.Iic c ⊆ {d : D | Q fun (v : W) => d ≤ μ v})

def Buring2007.negationInside {W : Type u_1} {D : Type u_2} [LinearOrder D] (Q : (W → Prop) → Prop) (μ : W → D) (c : D) : Prop

With the degree negation inside the modal, the than-clause denotes the degrees exceeding the standard under the modal, and the more-comparative asserts that they are among the degrees exceeding the subject.

Equations

• Buring2007.negationInside Q μ c = ({d : D | Q fun (v : W) => μ v < d} ⊆ Set.Ioi c)

theorem Buring2007.negationOutside_iff {W : Type u_1} {D : Type u_2} [LinearOrder D] {Q : (W → Prop) → Prop} {μ : W → D} {c : D} (hQ : Monotone Q) : negationOutside Q μ c ↔ Q fun (v : W) => c ≤ μ v

The outside reading holds exactly when the modal claims the standard reaches the subject's degree.

theorem Buring2007.negationInside_iff {W : Type u_1} {D : Type u_2} [LinearOrder D] {Q : (W → Prop) → Prop} {μ : W → D} {c : D} (hQ : Monotone Q) : negationInside Q μ c ↔ ¬Q fun (v : W) => μ v < c

The inside reading holds exactly when the modal fails to claim the standard falls below the subject's degree.

theorem Buring2007.monotone_box {W : Type u_1} (R : SetRel W W) (w : W) : Monotone fun (p : W → Prop) => ModalLogic.Box R p w

theorem Buring2007.monotone_diamond {W : Type u_1} (R : SetRel W W) (w : W) : Monotone fun (p : W → Prop) => ModalLogic.Diamond R p w

theorem Buring2007.negationOutside_box {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} : negationOutside (fun (p : W → Prop) => ModalLogic.Box R p w) μ c ↔ ModalLogic.Box R (fun (v : W) => c ≤ μ v) w

Under a universal than-clause modal the outside reading is that the standard reaches the subject's degree in every accessible world — the minimum required width of the moat exceeds the drawbridge's length.

theorem Buring2007.negationInside_box {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} : negationInside (fun (p : W → Prop) => ModalLogic.Box R p w) μ c ↔ ModalLogic.Diamond R (fun (v : W) => c ≤ μ v) w

The inside reading of the same sentence is that the standard reaches it in some accessible world — the maximum permitted width does.

theorem Buring2007.negationOutside_diamond {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} : negationOutside (fun (p : W → Prop) => ModalLogic.Diamond R p w) μ c ↔ ModalLogic.Diamond R (fun (v : W) => c ≤ μ v) w

With an existential modal the two readings exchange: the outside reading becomes the weaker one, about the maximum permitted length of a drawbridge.

theorem Buring2007.negationInside_diamond {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} : negationInside (fun (p : W → Prop) => ModalLogic.Diamond R p w) μ c ↔ ModalLogic.Box R (fun (v : W) => c ≤ μ v) w

And the inside reading becomes the stronger one, about the minimum permitted length.

theorem Buring2007.outside_entails_inside_box {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} [ModalLogic.IsSerial R] : negationOutside (fun (p : W → Prop) => ModalLogic.Box R p w) μ c → negationInside (fun (p : W → Prop) => ModalLogic.Box R p w) μ c

Under a universal modal the outside reading entails the inside one.

theorem Buring2007.inside_entails_outside_diamond {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} [ModalLogic.IsSerial R] : negationInside (fun (p : W → Prop) => ModalLogic.Diamond R p w) μ c → negationOutside (fun (p : W → Prop) => ModalLogic.Diamond R p w) μ c

Under an existential modal the entailment runs the other way.

theorem Buring2007.inside_not_entails_outside : ∃ (μ : Bool → ℕ) (c : ℕ), negationInside (fun (p : Bool → Prop) => ModalLogic.Box Set.univ p true) μ c ∧ ¬negationOutside (fun (p : Bool → Prop) => ModalLogic.Box Set.univ p true) μ c

The entailment is strict: where a regulation permits moats of 30 and of 40 feet, a 35-foot drawbridge is shorter than a permitted moat is wide without being shorter than every one.

theorem Buring2007.analyses_agree_of_uniform {W : Type u_1} {D : Type u_2} [LinearOrder D] {μ : W → D} {c : D} {R : SetRel W W} {w : W} [ModalLogic.IsSerial R] (h : ∀ (v u : W), (w, v) ∈ R → (w, u) ∈ R → μ v = μ u) : negationOutside (fun (p : W → Prop) => ModalLogic.Box R p w) μ c ↔ negationInside (fun (p : W → Prop) => ModalLogic.Box R p w) μ c

The two readings coincide when the accessible worlds agree on the standard's degree, which is why a than-clause without a modal cannot tell the analyses apart.