Beck, Oda and Sugisaki 2004: comparison in Japanese without degree abstraction

This file formalizes Beck, Oda and Sugisaki's analysis of Japanese yori-comparatives. A yori-constituent denotes an individual — a free relative, or a definite built from a relative clause — and fixes the standard c of a positive or contextual comparative in the main clause, in place of the than-clause degree set of the standard analysis. The authors attribute the difference to a Degree Abstraction Parameter: Japanese does not bind degree variables in the syntax. We state both repertoires of denotations and derive from them the paper's three empirical differences — variable acceptability, no subcomparatives of degree, no degree-based negative islands — and its scope argument.

Main definitions

• er: the comparative morpheme on degree sets, max D₂ > max D₁.
• pos: the positive form at a standard c; the contextual comparative is Degree.MaxIn (Set.Ioi c).
• theC: the Fregean definite over a contextual domain, the denotation of a yori-clause.
• erJ: the comparative that combines directly with the adjective meaning.

Main results

• pos_comparedTo, maxIn_Ioi_Iic_iff: a context setter supplying y turns the positive form and the contextual comparative into the comparison with y.
• isGreatest_card_of_isMaximal: an amount standard is the cardinality of the maximal plurality.
• pos_ne_subcomparative: an individual standard lies on the matrix dimension and does not express a subcomparative of degree.
• not_er_nobody, yori_negative_entails_unbought: the negated than-clause has no maximum on an unbounded scale, while the definite yori-clause is defined and entails a particular unbought individual.
• er_everyone_without_shared_book: the standard comparative lacks the definite's uniqueness presupposition.
• erJ_iff_pos, exists_wideScope_not_inSitu: erJ has the truth conditions of the positive form and, applied in situ, yields only the narrow reading under need.

Example numbers follow the journal article; the examples are typed in Data/Examples/BeckOdaSugisaki2004.json.

References

• [BOS04]
• [vS84], [Hei00]: the standard analysis and the scope argument from intensional verbs.
• [Rul95]: negative islands as maximality failure.
• [HK98]: the positive form and the Fregean definite.
• [Jac95]: free relatives as maximal individuals.
• [Ken97]: the comparative combining directly with the adjective.
• [Ish91], [SWD95]: the acceptability and subcomparative data.

The standard analysis

def BeckOdaSugisaki2004.er {D : Type u_2} [LinearOrder D] (D₁ D₂ : Set D) : Prop

The comparative morpheme on degree sets, where er D₁ D₂ holds iff max D₂ > max D₁ (8).

Equations

• BeckOdaSugisaki2004.er D₁ D₂ = ∃ (m₁ : D) (m₂ : D), IsGreatest D₁ m₁ ∧ IsGreatest D₂ m₂ ∧ m₁ < m₂

theorem BeckOdaSugisaki2004.er_Iic_Iic {D : Type u_2} [LinearOrder D] (d₁ d₂ : D) : er (Set.Iic d₁) (Set.Iic d₂) ↔ d₁ < d₂

With unique witnesses er compares the two maxima directly, the comparative and the subcomparative of (7′), (9′) and (10′).

The contextual analysis

def BeckOdaSugisaki2004.pos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (c : D) (x : Entity) : Prop

The positive form at a contextual standard, where pos μ c x holds iff x is d-A for some d > c (20).

Equations

• BeckOdaSugisaki2004.pos μ c x = ∃ d ≤ μ x, c < d

theorem BeckOdaSugisaki2004.pos_iff_lt {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (c : D) (x : Entity) : pos μ c x ↔ c < μ x

theorem BeckOdaSugisaki2004.pos_iff_mem_over {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (c : D) (x : Entity) : pos μ c x ↔ x ∈ μ ⁻¹' Set.Ioi c

The positive form is the preimage of the open ray above the standard.

theorem BeckOdaSugisaki2004.maxIn_Ioi_iff_of_isGreatest {D : Type u_2} [LinearOrder D] {S : Set D} {m : D} (h : IsGreatest S m) (c : D) : Degree.MaxIn (Set.Ioi c) S ↔ ∃ d ∈ S, c < d

The contextual comparative MaxIn (Set.Ioi c), max S > c (23), holds of an S with a greatest element iff some d ∈ S exceeds c (footnote 7).

theorem BeckOdaSugisaki2004.maxIn_Ioi_Iic_iff {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (c : D) (x : Entity) : Degree.MaxIn (Set.Ioi c) (Set.Iic (μ x)) ↔ pos μ c x

On an adjective's own degree set the contextual comparative and the positive form coincide ((24d), (21b)).

theorem BeckOdaSugisaki2004.pos_comparedTo {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (x y : Entity) : pos μ (μ y) x ↔ μ y < μ x

A context setter supplying y sets c := μ y, and the positive form becomes the comparison with y ((21), (25)).

Yori-clauses denote individuals

noncomputable def BeckOdaSugisaki2004.theC {Entity : Type u_1} (C : Set Entity) (P : Entity → Prop) : Option Entity

theC C P is the unique P-individual of the contextual domain C (54).

Equations

• BeckOdaSugisaki2004.theC C P = Reference.iota fun (x : Entity) => x ∈ C ∧ P x

theorem BeckOdaSugisaki2004.theC_eq_some_iff {Entity : Type u_1} (C : Set Entity) (P : Entity → Prop) (y : Entity) : theC C P = some y ↔ (y ∈ C ∧ P y) ∧ ∀ z ∈ C, P z → z = y

theorem BeckOdaSugisaki2004.isGreatest_card_of_isGreatest {Atom : Type u_3} {P : Finset Atom → Prop} {Y : Finset Atom} (h : IsGreatest {S : Finset Atom | P S} Y) : IsGreatest {n : ℕ | ∃ (S : Finset Atom), P S ∧ n ≤ S.card} Y.card

If Y is the maximal P-plurality, then the greatest n for which some P-plurality has at least n members is the cardinality of Y (41a).

Subcomparatives

theorem BeckOdaSugisaki2004.pos_ne_subcomparative : ∃ (μ : Fin 2 → ℕ) (ν : Fin 2 → ℕ), ν 1 < μ 0 ∧ ¬pos μ (μ 1) 0

An individual standard lies on the matrix dimension, so the reading of the shelf–door sentence with the door as standard differs from the subcomparative ((74), (79)).

Negative islands

theorem BeckOdaSugisaki2004.not_isGreatest_nobody {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [NoMaxOrder D] (bought : Entity → Prop) (μ : Entity → D) : ¬∃ (m : D), IsGreatest (Degree.scopeDegrees (Quantifier.GQ.no bought) (Set.Iic ∘ μ)) m

On a scale without a top the negated than-clause, the degrees d such that nobody bought a d-expensive book (11), has no greatest degree (12).

theorem BeckOdaSugisaki2004.not_er_nobody {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [NoMaxOrder D] (bought : Entity → Prop) (μ : Entity → D) (S : Set D) : ¬er (Degree.scopeDegrees (Quantifier.GQ.no bought) (Set.Iic ∘ μ)) S

er over a negated than-clause never holds, the negative island ((11), (87a)).

theorem BeckOdaSugisaki2004.yori_negative_entails_unbought {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (C : Set Entity) (bought : Entity → Prop) (μ : Entity → D) (x : Entity) (h : ∃ (y : Entity), (theC C fun (z : Entity) => ¬bought z) = some y ∧ pos μ (μ y) x) : ∃ y ∈ C, ¬bought y

A yori-clause built on the unbought individuals denotes the unique one of them, so the construction entails that some book in the domain went unbought ((86), (88c)).

theorem BeckOdaSugisaki2004.er_everyone_without_shared_book : ∃ (read : Fin 2 → Fin 3 → Prop) (μ : Fin 3 → ℕ), er (Degree.scopeDegrees (fun (S : Fin 3 → Prop) => ∀ (b : Fin 2), Quantifier.GQ.some (read b) S) (Set.Iic ∘ μ)) (Set.Iic (μ 2)) ∧ ¬∃ (x : Fin 3), ∀ (b : Fin 2), read b x

The than-clause of a universally quantified comparative, the degrees d such that every boy read a d-long book (95a), is the degree set of the quantifier every boy read some book; the comparative can hold when no book was read by every boy, so it lacks the uniqueness presupposition of the yori-clause ((94), (95)).

The main clause and scope

def BeckOdaSugisaki2004.erJ {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (c : D) (P : D → Entity → Prop) (x : Entity) : Prop

The comparative on adjective meanings, where erJ c P x holds iff the greatest degree to which x is P exceeds c (133).

Equations

• BeckOdaSugisaki2004.erJ c P x = Degree.MaxIn (Set.Ioi c) {d : D | P d x}

theorem BeckOdaSugisaki2004.erJ_iff_pos {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ : Entity → D) (c : D) (x : Entity) : erJ c (fun (d : D) (x : Entity) => d ≤ μ x) x ↔ pos μ c x

For a monotone adjective, erJ and the positive form have the same truth conditions (footnote 15).

def BeckOdaSugisaki2004.wideScope {D : Type u_2} [LinearOrder D] {W : Type u_3} (acc : Set W) (μ : W → D) (s : D) : Prop

The wide-scope reading of need to be exactly s long, the comparative over need, says that the greatest degree reached in every acceptable world is the target s (136b).

Equations

• BeckOdaSugisaki2004.wideScope acc μ s = Degree.HighScope (Degree.MaxIn {s}) (Quantifier.GQ.every fun (x : W) => x ∈ acc) (Set.Iic ∘ μ)

def BeckOdaSugisaki2004.inSitu {D : Type u_2} [LinearOrder D] {W : Type u_3} (acc : Set W) (μ : W → D) (s : D) : Prop

The in-situ reading, which erJ with a differential yields, says that in every acceptable world the greatest degree is the target s.

Equations

• BeckOdaSugisaki2004.inSitu acc μ s = Degree.LowScope (Degree.MaxIn {s}) (Quantifier.GQ.every fun (x : W) => x ∈ acc) (Set.Iic ∘ μ)

theorem BeckOdaSugisaki2004.inSitu_iff {D : Type u_2} [LinearOrder D] {W : Type u_3} (acc : Set W) (μ : W → D) (s : D) : inSitu acc μ s ↔ ∀ w ∈ acc, μ w = s

theorem BeckOdaSugisaki2004.wideScope_of_inSitu {D : Type u_2} [LinearOrder D] {W : Type u_3} {acc : Set W} {μ : W → D} {s : D} (hne : acc.Nonempty) (h : inSitu acc μ s) : wideScope acc μ s

theorem BeckOdaSugisaki2004.exists_wideScope_not_inSitu : ∃ (acc : Set (Fin 2)) (μ : Fin 2 → ℕ), wideScope acc μ (10 + 5) ∧ ¬inSitu acc μ (10 + 5)

In a model where the acceptable versions of a 10-page draft run to 15 or 16 pages, the wide-scope reading of "needs to be exactly 5 pages longer" holds and the in-situ reading fails ((136), (138)).