Degree Constructions and Actuality Inferences (@cite{nadathur-2023}, Chapter 5)

@cite{meier-2003} @cite{nadathur-2023}

Formalizes the causal analysis of enough and too constructions:

• "The coffee is hot enough to drink" → someone drank it (with PFV)
• "The coffee is too hot to drink" → no one drank it (with PFV)

Key Insight

Enough and too generate actuality inferences via the same mechanism as ability modals: causal sufficiency of a degree-threshold condition for the complement, modulated by grammatical aspect.

• "Adj enough to VP": degree ≥ θ is causally sufficient for VP
• "too Adj to VP": degree ≥ θ is causally sufficient for ¬VP

With perfective aspect, the degree condition is asserted to hold, triggering the actuality inference. With imperfective, only the causal relationship is asserted.

Connection to CausalFrame

DegreeScenario is a CausalFrame where the trigger is the degree variable (degree ≥ threshold). This means:

• enoughWithAspect IS CausalFrame.actualityWithAspect with polarity = positive
• tooWithAspect uses CausalFrame.complementBlockedAt with polarity = negative
• The actuality theorems are INSTANCES of the generic ones from CausalVerb.lean

structure Nadathur2023.DegreeCausation.DegreeScenario : Type

A causal scenario for degree constructions (enough to VP, too Adj to VP).

The trigger is the degree variable: whether the entity's degree meets the threshold (degree ≥ θ for "enough", degree ≥ θ for "too" where θ is the threshold of excess).

The complement is the VP outcome.

The causal dynamics encodes the link between degree satisfaction and the complement. For "enough", the link is positive (degree met → complement develops). For "too", the link is negative (degree met → complement does NOT develop, modeled as absence of a law).

• dynamics : Core.StructuralEquationModel.CausalDynamics

  Causal dynamics linking degree to complement

• degreeMet : Core.StructuralEquationModel.Variable

  The degree variable: "degree meets threshold"

• complement : Core.StructuralEquationModel.Variable

  The complement variable (VP outcome)

• background : Semantics.Attitudes.Intensional.World → Core.StructuralEquationModel.Situation

  Maps each world to its background situation. Encodes whether the degree condition was actually met.

def Nadathur2023.DegreeCausation.enoughAt (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World) : Bool

The degree condition is causally sufficient for the complement at w.

"The coffee is hot enough to drink" presupposes that the degree of heat being sufficient is causally linked to the drinking event.

Equations

• Nadathur2023.DegreeCausation.enoughAt sc w = Core.StructuralEquationModel.causallySufficient sc.dynamics (sc.background w) sc.degreeMet sc.complement

def Nadathur2023.DegreeCausation.enoughActualized (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World) : Bool

The complement is actualized at w: degree was met AND complement developed via normal causal propagation.

Equations

• Nadathur2023.DegreeCausation.enoughActualized sc w = Core.StructuralEquationModel.factuallyDeveloped sc.dynamics (sc.background w) sc.degreeMet sc.complement

def Nadathur2023.DegreeCausation.enoughWithAspect (sc : DegreeScenario) (asp : Semantics.Tense.Aspect.Core.ViewpointAspectB) (w : Semantics.Attitudes.Intensional.World) : Bool

Enough with aspectual modulation.

• Perfective: degree met AND complement actualized
• Imperfective: degree met (causal link exists) but no actualization required

Equations

• One or more equations did not get rendered due to their size.
• Nadathur2023.DegreeCausation.enoughWithAspect sc Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective w = Nadathur2023.DegreeCausation.enoughAt sc w

def Nadathur2023.DegreeCausation.tooAt (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World) : Bool

The degree condition blocks the complement: degree met, but complement does NOT develop. This is the "too" pattern.

"The coffee is too hot to drink": the degree of heat being excessive is causally sufficient for the complement NOT occurring.

Equations

• Nadathur2023.DegreeCausation.tooAt sc w = !(Core.StructuralEquationModel.normalDevelopment sc.dynamics ((sc.background w).extend sc.degreeMet true)).hasValue sc.complement true

def Nadathur2023.DegreeCausation.tooActualized (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World) : Bool

The complement is blocked at w: degree was met AND complement did NOT develop.

Equations

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

def Nadathur2023.DegreeCausation.tooWithAspect (sc : DegreeScenario) (asp : Semantics.Tense.Aspect.Core.ViewpointAspectB) (w : Semantics.Attitudes.Intensional.World) : Bool

Too with aspectual modulation.

• Perfective: degree met AND complement blocked (= didn't happen)
• Imperfective: degree is excessive (causal link to blocking)

Equations

• One or more equations did not get rendered due to their size.
• Nadathur2023.DegreeCausation.tooWithAspect sc Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective w = Nadathur2023.DegreeCausation.tooAt sc w

theorem Nadathur2023.DegreeCausation.perfective_enough_entails_complement (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World) (h : enoughWithAspect sc Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = true) : enoughActualized sc w = true

Perfective enough entails complement: if "was Adj enough to VP" holds with perfective aspect, the complement is actualized.

Proof: immediate from the definition — perfective conjoins causal sufficiency with actualization.

theorem Nadathur2023.DegreeCausation.perfective_too_blocks_complement (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World) (h : tooWithAspect sc Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = true) : tooActualized sc w = true

Perfective too entails complement blocked: if "was too Adj to VP" holds with perfective aspect, the complement did NOT occur.

theorem Nadathur2023.DegreeCausation.imperfective_enough_no_entailment : ∃ (sc : DegreeScenario) (w : Semantics.Attitudes.Intensional.World), enoughWithAspect sc Semantics.Tense.Aspect.Core.ViewpointAspectB.imperfective w = true ∧ enoughActualized sc w = false

Imperfective enough is compatible with complement not actualized.

theorem Nadathur2023.DegreeCausation.enough_too_opposite : ∃ (scE : DegreeScenario) (scT : DegreeScenario) (w : Semantics.Attitudes.Intensional.World), scE.degreeMet = scT.degreeMet ∧ enoughWithAspect scE Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = true ∧ enoughActualized scE w = true ∧ tooWithAspect scT Semantics.Tense.Aspect.Core.ViewpointAspectB.perfective w = true ∧ tooActualized scT w = true

Enough and too give opposite actuality inferences in the same scenario.

With the same dynamics and degree variable:

• "enough": degree sufficient → complement develops
• "too": degree sufficient → complement does NOT develop (Different dynamics encode the different causal relationships.)

def Nadathur2023.DegreeCausation.DegreeScenario.toFrame (sc : DegreeScenario) : CausalVerb.CausalFrame Semantics.Attitudes.Intensional.World

A DegreeScenario for "enough" is a CausalFrame World with aspectual actualization.

Equations

• sc.toFrame = { dynamics := sc.dynamics, trigger := sc.degreeMet, complement := sc.complement, background := sc.background, actualization := CausalVerb.ActualizationMode.aspectual }

theorem Nadathur2023.DegreeCausation.enough_matches_frame (sc : DegreeScenario) (asp : Semantics.Tense.Aspect.Core.ViewpointAspectB) (w : Semantics.Attitudes.Intensional.World) : enoughWithAspect sc asp w = sc.toFrame.actualityWithAspect asp w

Grounding: enoughWithAspect matches the generic CausalFrame.actualityWithAspect for degree scenarios.

This proves that "enough" is structurally identical to "be able": both are aspect-governed causal frames.

theorem Nadathur2023.DegreeCausation.enough_same_pattern_as_ability (sc : DegreeScenario) : sc.toFrame.actualization = CausalVerb.ActualizationMode.aspectual

Structural unity: ability modals and "enough" are the same frame pattern, differing only in what the trigger represents.

This is the key claim of @cite{nadathur-2023}: ability modals and degree constructions are unified by the causal frame.