Granularity and Just: Degree Morphology [TD20]

Grounds the approximative readings of just with degree constructions in the granularity semantics of Degree.Granularity: with equatives the negative component of just is vacuous (just_vacuous_iff, "just as tall as" ≈ "exactly"), while with comparatives it forces failure at coarser grains (just_rules_out, "just taller than" ≈ "barely").

Main declarations

• equality_grounded, proximity_grounded: the two readings as instances of the granularity lemmas
• GranularityDatum, allGranularityData: the §3 equative/comparative data
• all_noncancellable: the granularity contribution is at-issue (§3.3)

theorem ThomasDeo2020.equality_grounded {D : Type u_1} {G : Type u_2} [LinearOrder D] (p : G → D → Prop) (finest : G) (h : ∀ (g : G), Degree.Granularity.atLeastAsStrong p finest g) (μ_x : D) : Degree.Granularity.approxJust p finest μ_x ↔ p finest μ_x

The equality reading for equatives is grounded: when the finest grain is the strongest (largest lo → fine entails coarse), just's negative component is vacuous, so "just as tall as" reduces to the equative at finest grain. Instantiates just_vacuous_iff.

theorem ThomasDeo2020.proximity_grounded {D : Type u_1} {G : Type u_2} [LinearOrder D] (p : G → D → Prop) (finest g : G) (h : ¬Degree.Granularity.atLeastAsStrong p finest g) (μ_x : D) (hjust : Degree.Granularity.approxJust p finest μ_x) : ¬p g μ_x

The proximity reading for comparatives is grounded: when the finest grain is NOT the strongest at some coarser grain g, just rules out truth at g. Instantiates just_rules_out.

§3 data: just with equatives and comparatives

Each datum records the construction type and the cancellability of the granularity inference.

inductive ThomasDeo2020.Cancellability : Type

Whether just's inference can be cancelled with "but...".

• cancellable : Cancellability
• nonCancellable : Cancellability

def ThomasDeo2020.instReprCancellability.repr : Cancellability → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ThomasDeo2020.instReprCancellability : Repr Cancellability

Equations

• ThomasDeo2020.instReprCancellability = { reprPrec := ThomasDeo2020.instReprCancellability.repr }

@[implicit_reducible]

instance ThomasDeo2020.instDecidableEqCancellability : DecidableEq Cancellability

Equations

• ThomasDeo2020.instDecidableEqCancellability x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure ThomasDeo2020.GranularityDatum : Type

A granularity-specific datum: example + construction + cancellability.

• sentence : String
• construction : Degree.AdjectivalConstruction
• cancellability : Cancellability
• paraphrase : String
• exampleNum : ℕ

@[implicit_reducible]

instance ThomasDeo2020.instReprGranularityDatum : Repr GranularityDatum

Equations

• ThomasDeo2020.instReprGranularityDatum = { reprPrec := ThomasDeo2020.instReprGranularityDatum.repr }

def ThomasDeo2020.instReprGranularityDatum.repr : GranularityDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance ThomasDeo2020.instDecidableEqGranularityDatum : DecidableEq GranularityDatum

Equations

• ThomasDeo2020.instDecidableEqGranularityDatum = ThomasDeo2020.instDecidableEqGranularityDatum.decEq

def ThomasDeo2020.instDecidableEqGranularityDatum.decEq (x✝ x✝¹ : GranularityDatum) : Decidable (x✝ = x✝¹)

Equations

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

def ThomasDeo2020.eq_amaryllis : GranularityDatum

(14) "The amaryllis are just as tall as the hollyhocks" ≈ "exactly as tall as".

Equations

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

def ThomasDeo2020.eq_anna_maria : GranularityDatum

(15) "Anna is just as old as Maria" ≈ "exactly as old as".

Equations

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

def ThomasDeo2020.comp_fafen_siri : GranularityDatum

(21) "Fafen is just older than Siri" ≈ "barely older than".

Equations

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

def ThomasDeo2020.comp_fafen_cancel : GranularityDatum

(23) "#Fafen is just older than Siri, but by a lot" — the proximity inference is non-cancellable. Contrast with (24): "Fafen is only older than Siri, but by a lot" (OK).

Equations

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

def ThomasDeo2020.comp_album : GranularityDatum

(25) "This album is just more expensive than that one" ≈ "barely more expensive".

Equations

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

def ThomasDeo2020.allGranularityData : List GranularityDatum

Equations

• ThomasDeo2020.allGranularityData = [ThomasDeo2020.eq_amaryllis, ThomasDeo2020.eq_anna_maria, ThomasDeo2020.comp_fafen_siri, ThomasDeo2020.comp_fafen_cancel, ThomasDeo2020.comp_album]

theorem ThomasDeo2020.all_noncancellable (d : GranularityDatum) : d ∈ allGranularityData → d.cancellability = Cancellability.nonCancellable

The granularity contribution of just is at-issue (§3.3), not a cancellable implicature: every datum's inference is non-cancellable.