Thomas and Deo (2020): The Interaction of just with Modified Scalar Predicates

Thomas and Deo analyse the approximative use of just with equatives and comparatives, just as tall as and just older than. A degree is interpreted at a level of precision, the open interval whose radius is the grain; an equative places the subject's degree above the infimum of the standard's level and a comparative above its supremum. Equatives make stronger claims at finer grains and comparatives at coarser ones. Just asserts the prejacent at the finest grain and denies it at every coarser grain where it would be stronger, so it adds nothing to an equative and gives a comparative an upper bound that cannot be cancelled.

Main definitions

• ThomasDeo2020.level: the level of radius ε around a degree, (42)–(43).
• ThomasDeo2020.equative, ThomasDeo2020.comparative: the constructions at a grain, (45) and (49).
• ThomasDeo2020.just: approximative just, (44).

Main results

• ThomasDeo2020.isGranularity_level, ThomasDeo2020.not_isPartition_range_level: a level is a granularity function, (40), that does not partition the scale.
• ThomasDeo2020.level_eq_iUnion_cell: a level is the union of the cells around its degree over all alignments of the grain, footnote 9.
• ThomasDeo2020.equative_mono, ThomasDeo2020.comparative_anti: (47) and (51).
• ThomasDeo2020.just_equative: with an equative just adds nothing, (48).
• ThomasDeo2020.just_comparative_iff, ThomasDeo2020.just.not_comparative: just older than holds at the finest grain and at no coarser one, (24).
• ThomasDeo2020.just_equative_of_comparative: just as tall as, if not taller, (16).
• ThomasDeo2020.not_just_comparative_iff: the two ways of denying just older, (31).
• ThomasDeo2020.just_comparative_Ici_iff: the negative component is exhaustification over the chain of grains, section 5.
• ThomasDeo2020.not_equative_of_comparative: the contradiction of (30).

Implementation notes

Degrees form a linearly ordered additive group. A construction relates the grain, the standard and the subject's maximal degree, which stands in for the existential over degrees of (45) and (49); the infimum and supremum of the level are computed as in (46b) and (50b), isGLB_level and isLUB_level. The endpoint clauses of (43) are not formalized: they leave the endpoint out of its own level, against (40a), which the paper says levels satisfy. The finest grain of (44) and the contextual grains are parameters; how magnitude, permitted error and roundness fix the finest grain (section 4) and the role of expectations (section 3.4) are not formalized. The examples are the rows of Data.Examples.ThomasDeo2020.

References

• [TD20]
• [SS11]
• [KMcN05]
• [CB14]
• [BC08]
• [Las99]
• [Kri07a]

Granularity levels, (40)–(43)

def ThomasDeo2020.level {D : Type u_1} [AddCommGroup D] [LinearOrder D] (ε d : D) : Set D

The level of radius ε around d, (43) at a degree that is not an endpoint of the scale.

Equations

• ThomasDeo2020.level ε d = Set.Ioo (d - ε) (d + ε)

theorem ThomasDeo2020.mem_level {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε d x : D} [IsOrderedAddMonoid D] : x ∈ level ε d ↔ |x - d| < ε

theorem ThomasDeo2020.mem_level_self {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε d : D} [IsOrderedAddMonoid D] (hε : 0 < ε) : d ∈ level ε d

theorem ThomasDeo2020.isGranularity_level {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε : D} [IsOrderedAddMonoid D] (hε : 0 < ε) : Degree.IsGranularity (level ε) (2 • ε)

The level of radius ε is a granularity function of width 2 • ε; the paper notes that the properties in (40) hold for levels.

theorem ThomasDeo2020.not_isPartition_range_level {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε : D} [IsOrderedAddMonoid D] [DenselyOrdered D] (hε : 0 < ε) : ¬Setoid.IsPartition (Set.range (level ε))

Levels do not partition the scale, as the paper notes in introducing (43).

theorem ThomasDeo2020.isGLB_level {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε d : D} [IsOrderedAddMonoid D] [DenselyOrdered D] (hε : 0 < ε) : IsGLB (level ε d) (d - ε)

On a dense scale the infimum of the level is d - ε, the bound of the equative as computed in (46b).

theorem ThomasDeo2020.isLUB_level {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε d : D} [IsOrderedAddMonoid D] [DenselyOrdered D] (hε : 0 < ε) : IsLUB (level ε d) (d + ε)

On a dense scale the supremum of the level is d + ε, the bound of the comparative as computed in (50b).

theorem ThomasDeo2020.level_eq_iUnion_cell {α : Type u_2} [Field α] [LinearOrder α] [IsStrictOrderedRing α] [FloorRing α] {ε : α} (hε : 0 < ε) (d : α) : level ε d = ⋃ (t : α), {y : α | y - t ∈ (Degree.grain ε).cell (d - t)}

The level of radius ε around d is the union, over all alignments t of the grain of width ε, of the cells containing d, as footnote 9 states.

Constructions at a grain (sections 4.1 and 4.2)

def ThomasDeo2020.equative {D : Type u_1} [AddCommGroup D] [LinearOrder D] (ε dc μx : D) : Prop

The equative at a grain holds when the subject's degree exceeds the infimum of the standard's level, (45).

Equations

• ThomasDeo2020.equative ε dc μx = (dc - ε < μx)

def ThomasDeo2020.comparative {D : Type u_1} [AddCommGroup D] [LinearOrder D] (ε dc μx : D) : Prop

The comparative at a grain holds when the subject's degree exceeds the supremum of the standard's level, (49).

Equations

• ThomasDeo2020.comparative ε dc μx = (dc + ε < μx)

theorem ThomasDeo2020.equative_iff {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε dc μx : D} : equative ε dc μx ↔ dc - ε < μx

theorem ThomasDeo2020.comparative_iff {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε dc μx : D} : comparative ε dc μx ↔ dc + ε < μx

def ThomasDeo2020.AtLeastAsStrong {D : Type u_1} (p : D → D → Prop) (ε₁ ε₂ : D) : Prop

A construction at one grain is at least as strong as at another when it entails it at every degree, the ranking of footnote 10.

Equations

• ThomasDeo2020.AtLeastAsStrong p ε₁ ε₂ = ∀ (μx : D), p ε₁ μx → p ε₂ μx

def ThomasDeo2020.just {D : Type u_1} (p : D → D → Prop) (G : Set D) (εf μx : D) : Prop

Approximative just, (44), asserts that the prejacent holds at the finest grain and at no grain of the contextual set at which it would make a stronger claim.

Equations

• ThomasDeo2020.just p G εf μx = (p εf μx ∧ ∀ ε ∈ G, p ε μx → ThomasDeo2020.AtLeastAsStrong p εf ε)

theorem ThomasDeo2020.equative_mono {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε₁ ε₂ dc : D} [IsOrderedAddMonoid D] (h : ε₁ ≤ ε₂) : AtLeastAsStrong (fun (x : D) => equative x dc) ε₁ ε₂

An equative at a finer grain is at least as strong, (47).

theorem ThomasDeo2020.comparative_anti {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε₁ ε₂ dc : D} [IsOrderedAddMonoid D] (h : ε₁ ≤ ε₂) : AtLeastAsStrong (fun (x : D) => comparative x dc) ε₂ ε₁

A comparative at a coarser grain is at least as strong, (51).

theorem ThomasDeo2020.not_equative_of_comparative {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε : D} [IsOrderedAddMonoid D] {μF dS : D} (h : comparative ε dS μF) : ¬equative ε μF dS

At one grain a comparative and its reversed equative cannot both hold, (30), since the difference in degree that the comparative requires is what the equative excludes.

Approximative just (44)

theorem ThomasDeo2020.just_equative {D : Type u_1} [AddCommGroup D] [LinearOrder D] {εf dc μx : D} {G : Set D} [IsOrderedAddMonoid D] (hG : ∀ ε ∈ G, εf ≤ ε) : just (fun (x : D) => equative x dc) G εf μx ↔ equative εf dc μx

With an equative the negative component is vacuous, so just as tall as is the equative at the finest grain, (48).

theorem ThomasDeo2020.just_equative_of_comparative {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε εf dc μx : D} {G : Set D} [IsOrderedAddMonoid D] (hG : ∀ ε ∈ G, εf ≤ ε) (hf : 0 ≤ εf) (hε : 0 ≤ ε) (h : comparative ε dc μx) : just (fun (x : D) => equative x dc) G εf μx

An equative with just enforces no upper bound, (16), since the subject may exceed the standard by any grain.

theorem ThomasDeo2020.just.not_comparative {D : Type u_1} [AddCommGroup D] [LinearOrder D] {ε εf dc μx : D} {G : Set D} [IsOrderedAddMonoid D] (h : just (fun (x : D) => comparative x dc) G εf μx) (hε : ε ∈ G) (hlt : εf < ε) : ¬comparative ε dc μx

With a comparative the negative component excludes every coarser grain, so the upper bound cannot be cancelled, (24).

theorem ThomasDeo2020.just_comparative_iff {D : Type u_1} [AddCommGroup D] [LinearOrder D] {εf dc μx : D} {G : Set D} [IsOrderedAddMonoid D] (hG : ∀ ε ∈ G, εf ≤ ε) : just (fun (x : D) => comparative x dc) G εf μx ↔ dc + εf < μx ∧ ∀ ε ∈ G, εf < ε → μx ≤ dc + ε

Just older than holds when the comparative holds at the finest grain and at no coarser one.

theorem ThomasDeo2020.not_just_comparative_iff {D : Type u_1} [AddCommGroup D] [LinearOrder D] {εf dc μx : D} {G : Set D} [IsOrderedAddMonoid D] (hG : ∀ ε ∈ G, εf ≤ ε) : ¬just (fun (x : D) => comparative x dc) G εf μx ↔ μx ≤ dc + εf ∨ ∃ ε ∈ G, εf < ε ∧ dc + ε < μx

Denying just older denies the comparative at the finest grain or asserts it at a coarser one, that the subject is significantly older, (31).

theorem ThomasDeo2020.just_comparative_Ici_iff {D : Type u_1} [AddCommGroup D] [LinearOrder D] {εf dc μx : D} [IsOrderedAddMonoid D] : just (fun (x : D) => comparative x dc) (Set.Ici εf) εf μx ↔ Exhaustification.exhAgainst (fun (x1 x2 : D) => x1 < x2) (fun (x : D) => comparative x dc μx) εf

Over the grains no finer than the finest, the negative component of just with a comparative is exhaustification against the strictly coarser grains, the stronger alternatives of the chain (section 5).

theorem ThomasDeo2020.just_comparative_iff_succ {D : Type u_1} [AddCommGroup D] [LinearOrder D] {εf dc μx : D} [IsOrderedAddMonoid D] {ε' : D} (his : εf < ε') (hleast : ∀ (ε : D), εf < ε → ε' ≤ ε) : just (fun (x : D) => comparative x dc) (Set.Ici εf) εf μx ↔ dc + εf < μx ∧ μx ≤ dc + ε'

With a next grain above the finest, just older than places the subject within that grain above the standard: Fafen's age is Siri's plus the finest grain, section 4.2.