Jin & Koenig (2021): A Cross-Linguistic Study of Expletive Negation

@cite{jin-koenig-2021}

Linguistic Typology, 25(1), 39–78.

A typological study of expletive negation (EN) — semantically vacuous negation triggered by the lexical meaning of an embedding predicate or operator. Based on a survey of 722 languages (EN attested in 74, across 37 genera) and detailed comparison of five languages: English, French, Januubi, Mandarin, and Zarma-Sonrai.

Core Contribution: Why EN Triggers Are Cross-Linguistically Similar

The paper's central insight: EN occurs when a trigger's meaning activates both a proposition p and its dual ¬p (in different modal or temporal domains). This dual activation, via spreading activation in language production (@cite{dell-1986}), sometimes causes the negator for ¬p to surface in the complement clause.

Four Licensing Conditions (§5.5, ex. 13)

EN triggers obey one of four semantic licensing conditions:

1. Propositional attitude / speech report triggers (§6.1): Meaning entails Operator₁(p) and Operator₂(¬p) — p and ¬p hold in different sets of worlds (attitude vs. desire, belief vs. standards).

2. Temporal operator triggers (§6.2): Meaning entails p at time t and ¬p at time t' — two time intervals.

3. Logical operator triggers (§6.3): Meaning includes ¬ directly (impossible, without, unless).

4. Comparative triggers (§6.4): Meaning entails Q(Y,D) and ¬Q(Z,D') — predications over distinct entities/degrees.

Table 5 Trigger Taxonomy

Class	Subclasses
"FEAR"	FEAR, AVOID
"REGRET"	REGRET, COMPLAIN, ADVISE AGAINST
"DENY"	DENY, HIDE, DESPAIR
"FORGET"	FORGET, DELAY, REFUSE, STOP/PREVENT, ALMOST
TEMPORALS	BEFORE, CANNOT WAIT, SINCE, RARELY
"IMPOSSIBLE"	IMPOSSIBLE, DIFFICULT
"WITHOUT"	WITHOUT
"UNLESS"	UNLESS, IT ONLY DEPENDS ON SOMEONE THAT
COMPARATIVES	MORE THAN, LESS THAN, DIFFERENT THAN, TOO…TO

structure JinKoenig2021.ENSurveyResult : Type

Cross-linguistic EN survey results.

• totalSurveyed : ℕ

  Total languages surveyed

• languagesWithEN : ℕ

  Languages where EN was attested

• generaWithEN : ℕ

  Genera where EN was attested

• beforeTriggerCount : ℕ

  Languages with EN in BEFORE-clauses specifically

• fearTriggerCount : ℕ

  Languages with EN in FEAR-clauses specifically

def JinKoenig2021.instReprENSurveyResult.repr : ENSurveyResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JinKoenig2021.instReprENSurveyResult : Repr ENSurveyResult

Equations

• JinKoenig2021.instReprENSurveyResult = { reprPrec := JinKoenig2021.instReprENSurveyResult.repr }

def JinKoenig2021.enSurvey : ENSurveyResult

The overall EN survey from @cite{jin-koenig-2021}.

Equations

• JinKoenig2021.enSurvey = { totalSurveyed := 722, languagesWithEN := 74, generaWithEN := 37, beforeTriggerCount := 50, fearTriggerCount := 39 }

def JinKoenig2021.survey : ENSurveyResult

The overall survey: 722 languages, EN in 74 (37 genera).

Equations

• JinKoenig2021.survey = JinKoenig2021.enSurvey

theorem JinKoenig2021.en_attested_minority : enSurvey.languagesWithEN < enSurvey.totalSurveyed

EN is attested in a substantial minority of surveyed languages.

theorem JinKoenig2021.en_across_many_genera : enSurvey.generaWithEN ≥ 30

EN is found across many genera (not an areal phenomenon).

theorem JinKoenig2021.en_before_most_common : enSurvey.beforeTriggerCount > enSurvey.fearTriggerCount

BEFORE is the most common EN trigger.

theorem JinKoenig2021.en_before_trigger_majority : enSurvey.beforeTriggerCount * 2 > enSurvey.languagesWithEN

BEFORE triggers occur in the majority of EN-attesting languages.

inductive JinKoenig2021.ContinentalArea : Type

Continental areas from @cite{jin-koenig-2021} Table 2.

• africa : ContinentalArea
• australiaNewGuinea : ContinentalArea
• eurasia : ContinentalArea
• northAmerica : ContinentalArea
• southAmerica : ContinentalArea
• pidginsCreoles : ContinentalArea

@[implicit_reducible]

instance JinKoenig2021.instDecidableEqContinentalArea : DecidableEq ContinentalArea

Equations

• JinKoenig2021.instDecidableEqContinentalArea x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JinKoenig2021.instReprContinentalArea.repr : ContinentalArea → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JinKoenig2021.instReprContinentalArea : Repr ContinentalArea

Equations

• JinKoenig2021.instReprContinentalArea = { reprPrec := JinKoenig2021.instReprContinentalArea.repr }

structure JinKoenig2021.ENAreaData : Type

Per-area EN survey data (Table 2).

• area : ContinentalArea
• languagesLookedAt : ℕ
• languagesWithEN : ℕ
• generaCovered : Option ℕ
• generaWithEN : Option ℕ

@[implicit_reducible]

instance JinKoenig2021.instReprENAreaData : Repr ENAreaData

Equations

• JinKoenig2021.instReprENAreaData = { reprPrec := JinKoenig2021.instReprENAreaData.repr }

def JinKoenig2021.instReprENAreaData.repr : ENAreaData → ℕ → Std.Format

Equations

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

def JinKoenig2021.enByArea : List ENAreaData

Table 2: Distribution of languages with and without EN by continental area (@cite{jin-koenig-2021}).

Equations

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

theorem JinKoenig2021.enByArea_sums_to_74 : (List.map (fun (x : ENAreaData) => x.languagesWithEN) enByArea).sum = 74

The per-area EN counts sum to 74. (The per-area language-looked-at counts sum to 728, not 722 — the paper's total is 722, suggesting 6 Pidgin/Creole languages are also counted in geographic areas.)

theorem JinKoenig2021.en_absent_south_america : ((List.filter (fun (x : ENAreaData) => x.area == ContinentalArea.southAmerica) enByArea).all fun (x : ENAreaData) => x.languagesWithEN == 0) = true

EN is not attested in South America in this sample.

theorem JinKoenig2021.eurasia_most_en : ((List.filter (fun (x : ENAreaData) => x.area == ContinentalArea.eurasia) enByArea).all fun (x : ENAreaData) => decide (x.languagesWithEN > 50)) = true

Eurasia has the highest concentration of EN-attesting languages.

Per-language EN attestation

Table 3 lists all 74 languages where EN was attested, grouped by continental area and genus. Each entry records the EN trigger concepts attested in that language (using the concept labels from the paper, in small capitals).

structure JinKoenig2021.ENLanguageEntry : Type

A language with attested EN and its trigger concepts (Table 3).

• name : String

  Language name

• iso : String

  ISO 639-3 code

• genus : String

  Genus (following the paper's classification)

• area : ContinentalArea

  Continental area

• triggers : List String

  EN trigger concepts attested (concept labels from Table 3)

def JinKoenig2021.instReprENLanguageEntry.repr : ENLanguageEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JinKoenig2021.instReprENLanguageEntry : Repr ENLanguageEntry

Equations

• JinKoenig2021.instReprENLanguageEntry = { reprPrec := JinKoenig2021.instReprENLanguageEntry.repr }

def JinKoenig2021.enLanguages : List ENLanguageEntry

Table 3: All 74 languages where EN was attested, with their trigger concepts (@cite{jin-koenig-2021}, pp. 45–48).

Equations

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

theorem JinKoenig2021.enLanguages_count : enLanguages.length = 74

Table 3 has exactly 74 languages.

theorem JinKoenig2021.enLanguages_africa : (List.filter (fun (x : ENLanguageEntry) => x.area == ContinentalArea.africa) enLanguages).length = 11

Per-area counts match Table 2.

theorem JinKoenig2021.enLanguages_australiaNewGuinea : (List.filter (fun (x : ENLanguageEntry) => x.area == ContinentalArea.australiaNewGuinea) enLanguages).length = 2

theorem JinKoenig2021.enLanguages_eurasia : (List.filter (fun (x : ENLanguageEntry) => x.area == ContinentalArea.eurasia) enLanguages).length = 56

theorem JinKoenig2021.enLanguages_northAmerica : (List.filter (fun (x : ENLanguageEntry) => x.area == ContinentalArea.northAmerica) enLanguages).length = 1

theorem JinKoenig2021.enLanguages_pidginsCreoles : (List.filter (fun (x : ENLanguageEntry) => x.area == ContinentalArea.pidginsCreoles) enLanguages).length = 4

theorem JinKoenig2021.enLanguages_no_southAmerica : (List.filter (fun (x : ENLanguageEntry) => x.area == ContinentalArea.southAmerica) enLanguages).length = 0

No South American languages have EN in this sample.

theorem JinKoenig2021.enLanguages_all_have_triggers : (enLanguages.all fun (e : ENLanguageEntry) => !e.triggers.isEmpty) = true

Every language has at least one trigger concept.

theorem JinKoenig2021.enLanguages_many_genera : (List.map (fun (x : ENLanguageEntry) => x.genus) enLanguages).eraseDups.length ≥ 37

The number of distinct genera represented (counting unique genus strings).

theorem JinKoenig2021.enLanguages_before_at_least : (List.filter (fun (e : ENLanguageEntry) => JinKoenig2021.hasBeforeOrUntil✝ e.triggers) enLanguages).length ≥ 42

At least 42 languages in Table 3 have BEFORE/UNTIL as an EN trigger.

theorem JinKoenig2021.enLanguages_fear_at_least : (List.filter (fun (e : ENLanguageEntry) => JinKoenig2021.hasFearOrAfraid✝ e.triggers) enLanguages).length ≥ 38

At least 38 languages in Table 3 have FEAR/AFRAID as an EN trigger.

theorem JinKoenig2021.before_more_widespread_than_fear : (List.filter (fun (e : ENLanguageEntry) => JinKoenig2021.hasBeforeOrUntil✝ e.triggers) enLanguages).length > (List.filter (fun (e : ENLanguageEntry) => JinKoenig2021.hasFearOrAfraid✝ e.triggers) enLanguages).length

BEFORE/UNTIL is more widely attested than FEAR/AFRAID in Table 3.

structure JinKoenig2021.TriggerCount : Type

Per-trigger occurrence counts (Table 4). The number of languages (out of the 74 with any EN) where each trigger concept was attested.

• trigger : String
• count : ℕ

def JinKoenig2021.instReprTriggerCount.repr : TriggerCount → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JinKoenig2021.instReprTriggerCount : Repr TriggerCount

Equations

• JinKoenig2021.instReprTriggerCount = { reprPrec := JinKoenig2021.instReprTriggerCount.repr }

def JinKoenig2021.triggerCounts : List TriggerCount

Equations

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

theorem JinKoenig2021.before_and_fear_most_widespread : triggerCounts.head? = some { trigger := "BEFORE/UNTIL", count := 50 }

BEFORE and FEAR are the two most widespread EN triggers.

inductive JinKoenig2021.LicensingCondition : Type

The four main classes of EN-licensing conditions (§5.5, ex. 13).

• propositionalAttitude : LicensingCondition

  Meaning entails Operator₁(p) and Operator₂(¬p) in different sets of worlds (attitude content vs. desire/standards/beliefs).

• temporalOperator : LicensingCondition

  Meaning entails p at time t and ¬p at time t'.

• logicalOperator : LicensingCondition

  Meaning includes ¬ directly (impossible, without, unless).

• comparative : LicensingCondition

  Meaning entails Q(Y,D) and ¬Q(Z,D') over distinct entities.

@[implicit_reducible]

instance JinKoenig2021.instDecidableEqLicensingCondition : DecidableEq LicensingCondition

Equations

• JinKoenig2021.instDecidableEqLicensingCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JinKoenig2021.instReprLicensingCondition : Repr LicensingCondition

Equations

• JinKoenig2021.instReprLicensingCondition = { reprPrec := JinKoenig2021.instReprLicensingCondition.repr }

def JinKoenig2021.instReprLicensingCondition.repr : LicensingCondition → ℕ → Std.Format

Equations

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

inductive JinKoenig2021.TriggerSubclass : Type

Subclasses of EN triggers within each licensing condition (Table 5).

• fear : TriggerSubclass
• regret : TriggerSubclass
• deny : TriggerSubclass
• forget : TriggerSubclass
• before : TriggerSubclass
• cannotWait : TriggerSubclass
• since : TriggerSubclass
• rarely : TriggerSubclass
• impossible : TriggerSubclass
• without : TriggerSubclass
• unless : TriggerSubclass
• moreThan : TriggerSubclass
• differentThan : TriggerSubclass
• tooTo : TriggerSubclass

@[implicit_reducible]

instance JinKoenig2021.instDecidableEqTriggerSubclass : DecidableEq TriggerSubclass

Equations

• JinKoenig2021.instDecidableEqTriggerSubclass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance JinKoenig2021.instReprTriggerSubclass : Repr TriggerSubclass

Equations

• JinKoenig2021.instReprTriggerSubclass = { reprPrec := JinKoenig2021.instReprTriggerSubclass.repr }

def JinKoenig2021.instReprTriggerSubclass.repr : TriggerSubclass → ℕ → Std.Format

Equations

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

def JinKoenig2021.TriggerSubclass.licensingCondition : TriggerSubclass → LicensingCondition

Each subclass belongs to exactly one licensing condition.

Equations

• JinKoenig2021.TriggerSubclass.fear.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude
• JinKoenig2021.TriggerSubclass.regret.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude
• JinKoenig2021.TriggerSubclass.deny.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude
• JinKoenig2021.TriggerSubclass.forget.licensingCondition = JinKoenig2021.LicensingCondition.propositionalAttitude
• JinKoenig2021.TriggerSubclass.before.licensingCondition = JinKoenig2021.LicensingCondition.temporalOperator
• JinKoenig2021.TriggerSubclass.cannotWait.licensingCondition = JinKoenig2021.LicensingCondition.temporalOperator
• JinKoenig2021.TriggerSubclass.since.licensingCondition = JinKoenig2021.LicensingCondition.temporalOperator
• JinKoenig2021.TriggerSubclass.rarely.licensingCondition = JinKoenig2021.LicensingCondition.temporalOperator
• JinKoenig2021.TriggerSubclass.impossible.licensingCondition = JinKoenig2021.LicensingCondition.logicalOperator
• JinKoenig2021.TriggerSubclass.without.licensingCondition = JinKoenig2021.LicensingCondition.logicalOperator
• JinKoenig2021.TriggerSubclass.unless.licensingCondition = JinKoenig2021.LicensingCondition.logicalOperator
• JinKoenig2021.TriggerSubclass.moreThan.licensingCondition = JinKoenig2021.LicensingCondition.comparative
• JinKoenig2021.TriggerSubclass.differentThan.licensingCondition = JinKoenig2021.LicensingCondition.comparative
• JinKoenig2021.TriggerSubclass.tooTo.licensingCondition = JinKoenig2021.LicensingCondition.comparative

The dual-inference property

The central observation: EN triggers activate both p and ¬p, but in different domains (different sets of worlds, different time intervals, different degrees). Table 6 catalogs the positive and negative inferences for each trigger subclass.

For propositional attitude triggers, the two domains are:

• Positive inference: p in worlds consistent with X's attitude
• Negative inference: ¬p in worlds consistent with X's desires/standards/beliefs

For temporal triggers:

• Positive inference: p at time t
• Negative inference: ¬p at reference time r (or at a different time t')

For logical triggers, ¬ is part of the operator's meaning (no separate domain).

For comparatives, the dual involves predications over distinct entities/degrees.

structure JinKoenig2021.DualInferenceProfile : Type

The positive and negative inferences of a trigger subclass (Table 6). These are natural-language descriptions of the modal/temporal domains in which p and ¬p hold, respectively.

• subclass : TriggerSubclass
• positiveInference : String

  Domain where p holds (positive inference)

• negativeInference : String

  Domain where ¬p holds (negative inference)

@[implicit_reducible]

instance JinKoenig2021.instReprDualInferenceProfile : Repr DualInferenceProfile

Equations

• JinKoenig2021.instReprDualInferenceProfile = { reprPrec := JinKoenig2021.instReprDualInferenceProfile.repr }

def JinKoenig2021.instReprDualInferenceProfile.repr : DualInferenceProfile → ℕ → Std.Format

Equations

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

def JinKoenig2021.table6 : List DualInferenceProfile

Table 6 data: positive and negative inferences for each trigger concept (@cite{jin-koenig-2021}, pp. 70–71). All 28 rows of the paper's Table 6 are encoded. Within each class, concepts often have different inference profiles (e.g., AVOID adds "and in w₀" to FEAR's positive inference; DESPAIR has three sources of inference).

Equations

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

theorem JinKoenig2021.table6_complete : table6.length = 28

All 28 rows of the paper's Table 6 (pp. 70–71) are encoded. Some subclasses have multiple entries with distinct inference profiles (e.g., FEAR vs AVOID, IMPOSSIBLE vs DIFFICULT).

Connecting EN licensing to preferential attitude semantics

The FEAR trigger class (§6.1.1) licenses EN because the meaning of fear-type verbs activates both p (content of attitude — what X fears) and ¬p (content of desire — what X wants). This dual activation corresponds precisely to negative valence in the preferential attitude semantics of @cite{villalta-2008}:

• Positive valence (hope, wish): X wants p → only p is activated
• Negative valence (fear, dread): X fears p but wants ¬p → both activated

The key theorem: negative-valence predicates satisfy the propositional attitude licensing condition for EN.

def JinKoenig2021.negativeValenceEntailsDual (v : Features.AttitudeValence) : Bool

Negative-valence predicates have dual inference: the meaning activates both p (feared proposition) and ¬p (desired alternative). This is DERIVED from the valence field of the preferential predicate, not stipulated.

Equations

• JinKoenig2021.negativeValenceEntailsDual v = (v == Features.AttitudeValence.negative)

theorem JinKoenig2021.fear_has_dual_inference {W : Type u_1} {E : Type u_2} (μ : Semantics.Attitudes.Preferential.PreferenceFunction W E) (θ : Semantics.Attitudes.Preferential.ThresholdFunction W) : negativeValenceEntailsDual (Semantics.Attitudes.Preferential.fear μ θ).valence = true

Fear has negative valence → satisfies the dual-inference condition.

theorem JinKoenig2021.dread_has_dual_inference {W : Type u_1} {E : Type u_2} (μ : Semantics.Attitudes.Preferential.PreferenceFunction W E) (θ : Semantics.Attitudes.Preferential.ThresholdFunction W) : negativeValenceEntailsDual (Semantics.Attitudes.Preferential.dread μ θ).valence = true

Dread has negative valence → satisfies the dual-inference condition.

theorem JinKoenig2021.worry_has_dual_inference {W : Type u_1} {E : Type u_2} (μ : Semantics.Attitudes.Preferential.PreferenceFunction W E) (θ : Semantics.Attitudes.Preferential.ThresholdFunction W) (isUncertain : E → Semantics.Attitudes.Preferential.AlternativeList W → Bool) : negativeValenceEntailsDual (Semantics.Attitudes.Preferential.worry μ θ isUncertain).valence = true

Worry has negative valence → satisfies the dual-inference condition. (Non-C-distributive, but still negative valence.)

theorem JinKoenig2021.hope_no_dual_inference {W : Type u_1} {E : Type u_2} (μ : Semantics.Attitudes.Preferential.PreferenceFunction W E) (θ : Semantics.Attitudes.Preferential.ThresholdFunction W) : negativeValenceEntailsDual (Semantics.Attitudes.Preferential.hope μ θ).valence = false

Hope has positive valence → does NOT satisfy the dual-inference condition → NOT an EN trigger. While 'hope' has been reported as a possible EN trigger in Japanese/Korean (@cite{jin-koenig-2021}, §2, exx. 5–6), JK2021 exclude these based on their definition (2): the complement negation reflects epistemic uncertainty, not EN.

theorem JinKoenig2021.class2_licenses_EN : negativeValenceEntailsDual Features.AttitudeValence.negative = true ∧ negativeValenceEntailsDual Features.AttitudeValence.positive = false

NVP Class 2 (C-distributive + negative valence) = the class that licenses EN in complement clauses. This connects the preferential attitude classification to the EN trigger taxonomy.

DENY triggers and neg-raising

The DENY class (§6.1.3) licenses EN because DENY entails or implies BELIEVE(X, ¬p). In neg-raising terms: when the matrix clause is negated or questioned, both p and ¬p are activated (the doxastic square has both Bel(p) and Bel(¬p) as corners).

The connection: neg-raising predicates activate both p and ¬p precisely because ¬Bel(p) pragmatically strengthens to Bel(¬p). When DOUBT is negated or questioned, this dual activation occurs, licensing EN.

This is consistent with the empirical observation that DOUBT and DENY triggers in French often require the matrix clause to be negated or questioned for EN to occur (§6.1.3).

theorem JinKoenig2021.deny_EN_via_negRaising : Semantics.Attitudes.NegRaising.negRaisingAvailable Features.Veridicality.nonVeridical = true ∧ TriggerSubclass.deny.licensingCondition = LicensingCondition.propositionalAttitude

DENY triggers license EN through the doxastic square:

1. Non-veridical doxastic predicates (believe, doubt) support neg-raising: ¬Bel(p) strengthens to Bel(¬p) (NegRaising.lean)
2. Under negation/questioning, this pragmatic strengthening activates both Bel(p) and Bel(¬p) simultaneously — the dual inference required for EN (§6.1.3)
3. DENY maps to the propositional attitude licensing condition

The paper says explicitly: "triggers such as QUESTION or DOUBT do not strictly entail BELIEVE(X, ¬p); they only strongly imply BELIEVE(X, ¬p)" — this IS neg-raising (O→E strengthening).

Five-language comparison

Table 5 shows that the trigger classes are strikingly similar across five languages from four distinct families:

• English (Germanic/Indo-European)
• French (Italic/Indo-European)
• Januubi (Semitic/Afro-Asiatic)
• Mandarin (Sinitic/Sino-Tibetan)
• Zarma-Sonrai (Songhay/Nilo-Saharan)

Each entry records whether a language has lexical items for a given trigger subclass.

structure JinKoenig2021.TriggerAttestation : Type

A cross-linguistic trigger attestation datum (Table 5). Each Bool records whether any subclass member triggers EN in that language. .differentThan is omitted (not a separate Table 5 row; analyzed only in §6.4 and Table 6).

• subclass : TriggerSubclass
• english : Bool

  Does the language have EN-triggering lexical items for this class?

• french : Bool
• januubi : Bool
• mandarin : Bool
• zarmaSonrai : Bool

@[implicit_reducible]

instance JinKoenig2021.instReprTriggerAttestation : Repr TriggerAttestation

Equations

• JinKoenig2021.instReprTriggerAttestation = { reprPrec := JinKoenig2021.instReprTriggerAttestation.repr }

def JinKoenig2021.instReprTriggerAttestation.repr : TriggerAttestation → ℕ → Std.Format

Equations

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

def JinKoenig2021.triggerAttestations : List TriggerAttestation

Equations

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

theorem JinKoenig2021.core_triggers_universal : ((List.filter (fun (d : TriggerAttestation) => [TriggerSubclass.fear, TriggerSubclass.regret, TriggerSubclass.deny, TriggerSubclass.forget, TriggerSubclass.before, TriggerSubclass.cannotWait, TriggerSubclass.since, TriggerSubclass.rarely, TriggerSubclass.impossible, TriggerSubclass.unless].contains d.subclass) triggerAttestations).all fun (d : TriggerAttestation) => d.english && d.french && d.januubi && d.mandarin && d.zarmaSonrai) = true

Ten trigger subclasses are attested in all five languages (Table 5). The three non-universal subclasses are WITHOUT (Mandarin and Zarma-Sonrai express it as "q not p", §7), MORE THAN (Januubi only allows NPs as complements of comparatives, §6.4), and TOO...TO (Januubi, Mandarin, and Zarma-Sonrai use "too...so that...not" collocations, §6.4).

theorem JinKoenig2021.non_universal_triggers_explained : ((List.filter (fun (d : TriggerAttestation) => [TriggerSubclass.without, TriggerSubclass.moreThan, TriggerSubclass.tooTo].contains d.subclass) triggerAttestations).all fun (d : TriggerAttestation) => !(d.english && d.french && d.januubi && d.mandarin && d.zarmaSonrai)) = true

WITHOUT, MORE THAN, and TOO...TO are attested in only a subset of languages due to language-internal structural factors (§6.4, §7).

theorem JinKoenig2021.attitude_triggers_grouped : ([TriggerSubclass.fear, TriggerSubclass.regret, TriggerSubclass.deny, TriggerSubclass.forget].all fun (x : TriggerSubclass) => x.licensingCondition == LicensingCondition.propositionalAttitude) = true

All attitude/speech report triggers map to the propositional attitude licensing condition.

theorem JinKoenig2021.temporal_triggers_grouped : ([TriggerSubclass.before, TriggerSubclass.cannotWait, TriggerSubclass.since, TriggerSubclass.rarely].all fun (x : TriggerSubclass) => x.licensingCondition == LicensingCondition.temporalOperator) = true

All temporal triggers map to the temporal operator licensing condition.

theorem JinKoenig2021.logical_triggers_grouped : ([TriggerSubclass.impossible, TriggerSubclass.without, TriggerSubclass.unless].all fun (x : TriggerSubclass) => x.licensingCondition == LicensingCondition.logicalOperator) = true

All logical triggers map to the logical operator licensing condition.

theorem JinKoenig2021.comparative_triggers_grouped : ([TriggerSubclass.moreThan, TriggerSubclass.differentThan, TriggerSubclass.tooTo].all fun (x : TriggerSubclass) => x.licensingCondition == LicensingCondition.comparative) = true

All comparative triggers map to the comparative licensing condition.

The type of domain determines the licensing condition

The paper's four licensing conditions correspond to four types of domain in which p and ¬p hold. This is not stated explicitly in the paper but follows from the structure of Table 6: propositional attitude triggers always involve different sets of worlds, temporal triggers involve different time intervals, logical operators include ¬ structurally, and comparatives involve different degrees.

inductive JinKoenig2021.InferenceDomainType : Type

The type of domain in which a trigger's inferences hold.

• modal : InferenceDomainType
• temporal : InferenceDomainType
• structural : InferenceDomainType
• degree : InferenceDomainType

@[implicit_reducible]

instance JinKoenig2021.instDecidableEqInferenceDomainType : DecidableEq InferenceDomainType

Equations

• JinKoenig2021.instDecidableEqInferenceDomainType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def JinKoenig2021.instReprInferenceDomainType.repr : InferenceDomainType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance JinKoenig2021.instReprInferenceDomainType : Repr InferenceDomainType

Equations

• JinKoenig2021.instReprInferenceDomainType = { reprPrec := JinKoenig2021.instReprInferenceDomainType.repr }

def JinKoenig2021.TriggerSubclass.inferenceDomainType : TriggerSubclass → InferenceDomainType

Each trigger subclass has a characteristic domain type.

Equations

• JinKoenig2021.TriggerSubclass.fear.inferenceDomainType = JinKoenig2021.InferenceDomainType.modal
• JinKoenig2021.TriggerSubclass.regret.inferenceDomainType = JinKoenig2021.InferenceDomainType.modal
• JinKoenig2021.TriggerSubclass.deny.inferenceDomainType = JinKoenig2021.InferenceDomainType.modal
• JinKoenig2021.TriggerSubclass.forget.inferenceDomainType = JinKoenig2021.InferenceDomainType.modal
• JinKoenig2021.TriggerSubclass.before.inferenceDomainType = JinKoenig2021.InferenceDomainType.temporal
• JinKoenig2021.TriggerSubclass.cannotWait.inferenceDomainType = JinKoenig2021.InferenceDomainType.temporal
• JinKoenig2021.TriggerSubclass.since.inferenceDomainType = JinKoenig2021.InferenceDomainType.temporal
• JinKoenig2021.TriggerSubclass.rarely.inferenceDomainType = JinKoenig2021.InferenceDomainType.temporal
• JinKoenig2021.TriggerSubclass.impossible.inferenceDomainType = JinKoenig2021.InferenceDomainType.structural
• JinKoenig2021.TriggerSubclass.without.inferenceDomainType = JinKoenig2021.InferenceDomainType.structural
• JinKoenig2021.TriggerSubclass.unless.inferenceDomainType = JinKoenig2021.InferenceDomainType.structural
• JinKoenig2021.TriggerSubclass.moreThan.inferenceDomainType = JinKoenig2021.InferenceDomainType.degree
• JinKoenig2021.TriggerSubclass.differentThan.inferenceDomainType = JinKoenig2021.InferenceDomainType.degree
• JinKoenig2021.TriggerSubclass.tooTo.inferenceDomainType = JinKoenig2021.InferenceDomainType.degree

theorem JinKoenig2021.domainType_determines_condition (s : TriggerSubclass) : s.licensingCondition = match s.inferenceDomainType with | InferenceDomainType.modal => LicensingCondition.propositionalAttitude | InferenceDomainType.temporal => LicensingCondition.temporalOperator | InferenceDomainType.structural => LicensingCondition.logicalOperator | InferenceDomainType.degree => LicensingCondition.comparative

The inference domain type determines the licensing condition. This is a structural invariant: any trigger whose inferences involve different worlds maps to propositionalAttitude, etc.

BEFORE satisfies the temporal operator licensing condition

Anscombe's BEFORE semantics: A BEFORE B ↔ ∃t ∈ timeTrace(A), ∀t' ∈ timeTrace(B), t < t'

This entails:

• Positive inference: p is true at time t (∃t ∈ timeTrace(A))
• Negative inference: ¬p at reference time r (the complement time)

The temporal dual-inference property follows directly from the definition: BEFORE entails that the main clause event (p) occurs at a time strictly preceding all complement-clause times, hence p holds at t but not at any complement time t'.

The paper identifies BEFORE as the single most widespread EN trigger (50 languages), consistent with its transparent dual-inference structure.

theorem JinKoenig2021.before_positive_inference {Time : Type u_1} [LinearOrder Time] (A B : Semantics.Tense.TemporalConnectives.SentDenotation Time) (h : Semantics.Tense.TemporalConnectives.Anscombe.before A B) : ∃ (t : Time), t ∈ Semantics.Tense.TemporalConnectives.timeTrace A

BEFORE entails a temporal witness for p (the main clause event occurs at some time). This is the positive inference.

theorem JinKoenig2021.before_temporal_separation {Time : Type u_1} [LinearOrder Time] (A B : Semantics.Tense.TemporalConnectives.SentDenotation Time) (h : Semantics.Tense.TemporalConnectives.Anscombe.before A B) : ∃ t ∈ Semantics.Tense.TemporalConnectives.timeTrace A, ∀ t' ∈ Semantics.Tense.TemporalConnectives.timeTrace B, t < t'

BEFORE entails temporal separation: the main-clause time strictly precedes all complement-clause times. When B is nonempty, p (at t) and ¬p (at any t' ∈ B) coexist — the dual inference.

theorem JinKoenig2021.before_licensing : TriggerSubclass.before.licensingCondition = LicensingCondition.temporalOperator

BEFORE licenses EN because it maps to the temporal operator licensing condition (§6.2, ex. 13b).

theorem JinKoenig2021.until_en_from_before_negation {Time : Type u_1} [LinearOrder Time] (A B : Semantics.Tense.TemporalConnectives.SentDenotation Time) : Semantics.Tense.TemporalConnectives.Karttunen.notUntil A B ↔ ¬Semantics.Tense.TemporalConnectives.Anscombe.before A B

Punctual UNTIL = ¬BEFORE (Karttunen): the negation of BEFORE surfaces as the complement-clause negator, which is exactly EN.

IMPOSSIBLE satisfies the logical operator licensing condition

IMPOSSIBLE p = □¬p (necessity of negation): p is false in all accessible worlds. The meaning of IMPOSSIBLE includes ¬ directly — the negation is part of the operator's meaning, not contributed by a separate negator.

Kratzer's necessity f g (¬p) w computes: all best accessible worlds satisfy ¬p. The ¬ in the complement is structural, not expletive — but from the language production perspective, the activation of ¬p alongside p (in worlds outside the modal base) triggers EN.

@[reducible, inline]

abbrev JinKoenig2021.World : Type

Equations

• JinKoenig2021.World = Fin 4

theorem JinKoenig2021.impossible_licensing : TriggerSubclass.impossible.licensingCondition = LicensingCondition.logicalOperator

IMPOSSIBLE maps to the logical operator licensing condition.

theorem JinKoenig2021.not_impossible_activates_p (f : Core.Logic.Intensional.ModalBase World) (g : Core.Logic.Intensional.OrderingSource World) (p : World → Prop) (w : World) : ¬Semantics.Modality.Kratzer.necessity f g (fun (w' : World) => ¬p w') w → Semantics.Modality.Kratzer.possibility f g p w

WITHOUT satisfies the logical operator licensing condition

"q WITHOUT p" entails q ∧ ¬p. The negation of p is a necessary part of the meaning of WITHOUT — it is structural, not expletive (§6.3.2).

The paper notes that "in the examples we found, there is an entailment that ¬p is true at reference time t (e.g., the speaker not knowing it) and that reference time includes the event time for q (e.g., the time where she left)."

Cross-linguistically, WITHOUT triggers EN in English, French, and Januubi but NOT in Mandarin or Zarma-Sonrai (which express WITHOUT analytically as "q not p", making the negation non-expletive).

def JinKoenig2021.withoutSem {W : Type u_1} (q p : W → Bool) : W → Bool

WITHOUT q p = q ∧ ¬p: the meaning structurally includes ¬.

Equations

• JinKoenig2021.withoutSem q p w = (q w && !p w)

theorem JinKoenig2021.without_entails_not_p {W : Type u_1} (q p : W → Bool) (w : W) (h : withoutSem q p w = true) : p w = false

WITHOUT structurally includes negation: if "q without p" holds, then p is false.

theorem JinKoenig2021.without_entails_q {W : Type u_1} (q p : W → Bool) (w : W) (h : withoutSem q p w = true) : q w = true

WITHOUT structurally includes the main clause: if "q without p" holds, then q is true.

theorem JinKoenig2021.without_licensing : TriggerSubclass.without.licensingCondition = LicensingCondition.logicalOperator

WITHOUT maps to the logical operator licensing condition.

UNLESS satisfies the logical operator licensing condition

UNLESS q p = if ¬p then q = materialImp (¬p) q.

The meaning of UNLESS structurally includes ¬: the conditional's antecedent is the negation of p. This makes ¬p part of the operator's meaning, satisfying the logical operator licensing condition (§6.3.3).

More precisely: "q UNLESS p" entails that ¬p is true in all suppositive worlds (worlds where q holds).

def JinKoenig2021.unlessSem {W : Type u_1} (q p : Set W) : Set W

UNLESS q p is definable as material implication with negated antecedent: if ¬p then q. The negation is structural.

Equations

• JinKoenig2021.unlessSem q p = Semantics.Conditionals.materialImp pᶜ q

theorem JinKoenig2021.unless_modus_ponens {W : Type u_1} (q p : Set W) (w : W) (hcond : unlessSem q p w) (hnp : ¬p w) : q w

UNLESS includes ¬ in its meaning: at any world where ¬p is true AND q is true, the conditional holds. Conversely, at any world where the conditional holds and ¬p is true, q must be true.

theorem JinKoenig2021.unless_licensing : TriggerSubclass.unless.licensingCondition = LicensingCondition.logicalOperator

UNLESS maps to the logical operator licensing condition.

MORE THAN satisfies the comparative licensing condition

"Y is MORE Q THAN Z" entails (via @cite{jin-koenig-2021}, Table 6):

• Positive: Q(Z, D) — Z has property Q to degree D
• Negative: ¬Q(Z, D'), D' > D — Z does NOT have Q to degree D'

In the degree semantics of Theories.Semantics.Degree.Comparative: comparativeSem μ a b .positive ↔ μ(a) > μ(b)

This entails: ∃D (= μ(b)) such that Q(Z, D), and ∃D' (= μ(a)) > D such that ¬Q(Z, D'). The dual predication over distinct degrees is what licenses EN in the complement of comparatives.

theorem JinKoenig2021.comparative_dual_degrees {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) (h : Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive) : μ a > μ b

A comparative entails dual degree predication: Y exceeds Z on the scale, so Q(Z, μ(Z)) holds but ¬Q(Z, μ(Y)) — dual inference over distinct degrees.

theorem JinKoenig2021.comparative_antonymy_preserves_dual {Entity : Type u_1} {α : Type u_2} [LinearOrder α] (μ : Entity → α) (a b : Entity) : Semantics.Degree.Comparative.comparativeSem μ a b Core.Scale.ScalePolarity.positive ↔ Semantics.Degree.Comparative.comparativeSem μ b a Core.Scale.ScalePolarity.negative

The comparative antonymy theorem connects MORE and LESS: "A is more Q than B" ↔ "B is less Q than A" (= "B is more Q⁻ than A"). Both entail dual predication.

theorem JinKoenig2021.comparative_licensing : TriggerSubclass.moreThan.licensingCondition = LicensingCondition.comparative

Comparatives map to the comparative licensing condition.

Connecting FORGET-class subclasses to theory modules

The FORGET class (§6.1.4) is "semantically heterogeneous" — the paper groups these triggers by their shared negative entailment (¬p in w₀ or close to w₀), but they derive from distinct semantic mechanisms:

Subclass	Theory module	Key type
FORGET	Causation/Implicative	Implicative.negative
STOP/PREVENT	Causation/Builder	Causative.prevent
ALMOST	Degree/Comparative	threshold proximity

Each mechanism independently entails ¬p in the real world, unifying the class despite its heterogeneity.

theorem JinKoenig2021.forget_grounded_in_implicativity : Features.Implicative.negative.entailsComplement = false

FORGET is a negative implicative: "X forgot to do Y" entails that Y did NOT happen (¬p in w₀). This is DERIVED from the implicative builder's polarity, not stipulated. @cite{nadathur-2023}: negative implicatives entail complement falsity.

theorem JinKoenig2021.prevent_is_causative_builder : Features.Causative.prevent.assertsSufficiency = false

STOP/PREVENT are causative preventatives: "X prevented Y" entails that Y did NOT occur (¬p in w₀). The negative entailment comes from the causal blocking semantics of preventSem. @cite{nadathur-lauer-2020}: prevent = effect blocked with preventer, would have occurred without it.

theorem JinKoenig2021.forget_class_licensing : TriggerSubclass.forget.licensingCondition = LicensingCondition.propositionalAttitude ∧ TriggerSubclass.forget.inferenceDomainType = InferenceDomainType.modal

The FORGET class is unified by real-world negative entailment: all subclasses entail ¬p in w₀ (or worlds close to w₀), but through different semantic mechanisms. The class maps to the propositional attitude licensing condition because the positive inference involves a modal domain (obligations, normal course).

Connecting cross-linguistic EN attestation to fragment entries

Table 5 records that EN is attested in all five languages. The fragment files for each language formalize the negation markers. Here we verify that the fragment data is consistent with the attestation table: each language's EN markers exist and have the expected properties.

theorem JinKoenig2021.french_has_dedicated_en_marker : Fragments.French.Negation.enMarker = Fragments.French.Negation.neClitic

French uses dedicated ne (without pas) for high-entrenchment EN. This is distinct from standard ne...pas negation (@cite{jin-koenig-2021}, §4).

theorem JinKoenig2021.mandarin_fear_en_is_imperative : Fragments.Mandarin.Negation.bieParticle = "bié" ∧ Fragments.Mandarin.Negation.buyaoParticle = "búyào"

Mandarin FEAR triggers use imperative negation (bié/búyào), not the standard bù/méi. The imperative form lexicalizes the prohibition component of the FEAR meaning.

theorem JinKoenig2021.mandarin_regret_en_is_deontic : Fragments.Mandarin.Negation.bugaiParticle = "bùgāi"

Mandarin REGRET/COMPLAIN triggers use the deontic negator bùgāi 'shouldn't', connecting to the behavioral-standards semantics (negative inference = ¬p in worlds consistent with X's standards).

theorem JinKoenig2021.januubi_en_is_standard : Fragments.Januubi.Negation.enNegator.isStandardNeg = true

Januubi uses the standard negator maa for all EN contexts — no dedicated EN marker or trigger-class covariation.

theorem JinKoenig2021.zarma_en_determined_by_aspect : Fragments.ZarmaSonrai.Negation.enIpfv.isStandardNeg = true ∧ Fragments.ZarmaSonrai.Negation.enPfv.isStandardNeg = true

Zarma-Sonrai EN negator choice is determined by aspect (IPFV/PFV), not by trigger class. Both markers are standard negation markers.

Summary: Each licensing condition is now connected to theory-layer

semantics by construction.

Licensing condition	Theory module	Bridge theorem
propositionalAttitude	Attitudes.Preferential	fear_has_dual_inference
	Attitudes.NegRaising	deny_EN_via_negRaising
temporalOperator	Tense.TemporalConnectives	before_temporal_separation
logicalOperator	Modality.Kratzer	not_impossible_activates_p
	Conditionals.Basic	unless_modus_ponens
	(conjunction + negation)	without_entails_not_p
comparative	Degree.Comparative	comparative_dual_degrees

theorem JinKoenig2021.all_conditions_grounded : negativeValenceEntailsDual Features.AttitudeValence.negative = true ∧ TriggerSubclass.before.licensingCondition = LicensingCondition.temporalOperator ∧ TriggerSubclass.impossible.licensingCondition = LicensingCondition.logicalOperator ∧ TriggerSubclass.moreThan.licensingCondition = LicensingCondition.comparative

All four licensing conditions have at least one bridge theorem connecting them to a Theory-layer semantic operator.

The working definition of expletive negation

The paper's definition (ex. 2, p. 41) provides the basis for the entire study. EN is distinguished from other semantically vacuous negation (biased questions, negative concord, exclamatives) by requiring that it is (i) syntactically dependent on a specific trigger, (ii) triggered by that trigger's lexical semantics, and (iii) truth-conditionally vacuous in the complement clause.

structure JinKoenig2021.ENDefinition : Type

The three necessary conditions for an instance of negation to count as expletive negation (EN), per @cite{jin-koenig-2021}, ex. (2).

• isSyntacticDependent : Bool

  (i) The negator is in a syntactic dependent of a lexical item (verb, adposition, adverb, or collocation).

• isTriggeredByMeaning : Bool

  (ii) The negator is triggered by the meaning of that lexical item.

• isTruthConditionallyVacuous : Bool

  (iii) The negator does not contribute logical negation to the proposition denoted by the syntactic dependent.

@[implicit_reducible]

instance JinKoenig2021.instDecidableEqENDefinition : DecidableEq ENDefinition

Equations

• JinKoenig2021.instDecidableEqENDefinition = JinKoenig2021.instDecidableEqENDefinition.decEq

def JinKoenig2021.instDecidableEqENDefinition.decEq (x✝ x✝¹ : ENDefinition) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance JinKoenig2021.instReprENDefinition : Repr ENDefinition

Equations

• JinKoenig2021.instReprENDefinition = { reprPrec := JinKoenig2021.instReprENDefinition.repr }

def JinKoenig2021.instReprENDefinition.repr : ENDefinition → ℕ → Std.Format

Equations

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

def JinKoenig2021.isEN (d : ENDefinition) : Bool

An instance of negation is EN iff all three conditions hold.

Equations

• JinKoenig2021.isEN d = (d.isSyntacticDependent && d.isTriggeredByMeaning && d.isTruthConditionallyVacuous)

def JinKoenig2021.french_ne_fear : ENDefinition

French ne with peur (fear) satisfies all three conditions.

Equations

• JinKoenig2021.french_ne_fear = { isSyntacticDependent := true, isTriggeredByMeaning := true, isTruthConditionallyVacuous := true }

def JinKoenig2021.french_ne_wish : ENDefinition

French souhaiter (wish) + ne would NOT count as EN because wish does not trigger EN: replacing peur with souhaite in (1) yields an ungrammatical sentence (ex. 3).

Equations

• JinKoenig2021.french_ne_wish = { isSyntacticDependent := true, isTriggeredByMeaning := false, isTruthConditionallyVacuous := true }

theorem JinKoenig2021.fear_is_en : isEN french_ne_fear = true

theorem JinKoenig2021.wish_is_not_en : isEN french_ne_wish = false

Connecting JK2021 licensing conditions to Rett's ambidirectionality

@cite{rett-2026} (formalized in Rett2026) proposes that EN is licensed in ambidirectional constructions — those where negating an argument doesn't change truth conditions. This is a stronger, unified condition that subsumes JK2021's four conditions.

The mapping:

• Temporal operators (BEFORE, UNTIL) → ambidirectional on time intervals
• Comparatives (MORE THAN) → ambidirectional on degree intervals
• FEAR → ambidirectional via negative valence (dual activation)
• Logical operators (IMPOSSIBLE, WITHOUT, UNLESS) → these include ¬ in their meaning, making negation redundant (a form of ambidirectionality)

The key insight: JK2021's four conditions are necessary conditions observed bottom-up from data; Rett's ambidirectionality is a unified sufficient condition derived top-down from semantics. They are consistent: every JK2021 condition entails ambidirectionality.

theorem JinKoenig2021.temporal_triggers_are_rett_ambidirectional : TriggerSubclass.before.licensingCondition = LicensingCondition.temporalOperator ∧ TriggerSubclass.since.licensingCondition = LicensingCondition.temporalOperator

The two temporal trigger subclasses (BEFORE, SINCE) map to the temporal operator condition, which Rett connects to ambidirectionality on time intervals.

theorem JinKoenig2021.comparative_triggers_are_rett_ambidirectional : TriggerSubclass.moreThan.licensingCondition = LicensingCondition.comparative ∧ TriggerSubclass.tooTo.licensingCondition = LicensingCondition.comparative

Comparative triggers map to the comparative condition, which Rett connects to ambidirectionality on degree intervals.

theorem JinKoenig2021.fear_triggers_are_rett_ambidirectional : TriggerSubclass.fear.licensingCondition = LicensingCondition.propositionalAttitude ∧ negativeValenceEntailsDual Features.AttitudeValence.negative = true

FEAR triggers map to propositional attitude, which Rett derives from negative valence → dual activation → ambidirectionality.

Connecting English fragment verb entries to EN trigger status

Each of the three branches of VerbCore.isENTrigger corresponds to one class of JK2021 triggers. The general theorems below show that the semantic property (negative valence, negative implicativity, causative blocking) is sufficient for EN trigger status — the conclusion follows from the hypothesis, not by enumerating cases.

theorem JinKoenig2021.negative_valence_is_en_trigger (v : Semantics.Lexical.VerbCore) (h : v.preferentialValence = some Features.AttitudeValence.negative) : v.isENTrigger = true

Any verb with negative preferential valence is an EN trigger. This captures the FEAR class: negative valence activates both p (attitude content) and ¬p (desire content).

theorem JinKoenig2021.negative_implicative_is_en_trigger (v : Semantics.Lexical.VerbCore) (h : v.implicative = some Features.Implicative.negative) : v.isENTrigger = true

Any negative implicative verb is an EN trigger. This captures the FORGET class: "X forgot to p" entails ¬p in w₀.

theorem JinKoenig2021.prevent_builder_is_en_trigger (v : Semantics.Lexical.VerbCore) (h : v.causative = some Features.Causative.prevent) : v.isENTrigger = true

Any causative-prevent verb is an EN trigger. This captures the STOP/PREVENT class: blocking entails ¬p in w₀.

theorem JinKoenig2021.english_fear_is_en_trigger : Fragments.English.Predicates.Verbal.fear.isENTrigger = true

"fear" → negative valence → EN trigger.

theorem JinKoenig2021.english_dread_is_en_trigger : Fragments.English.Predicates.Verbal.dread.isENTrigger = true

"dread" → negative valence → EN trigger.

theorem JinKoenig2021.english_worry_is_en_trigger : Fragments.English.Predicates.Verbal.worry.isENTrigger = true

"worry" → negative valence (uncertainty-based) → EN trigger.

theorem JinKoenig2021.english_forget_is_en_trigger : Fragments.English.Predicates.Verbal.forget.isENTrigger = true

"forget" → negative implicative → EN trigger.

theorem JinKoenig2021.english_prevent_is_en_trigger : Fragments.English.Predicates.Verbal.prevent.isENTrigger = true

"prevent" → causative blocking → EN trigger.

ALMOST and BARELY are converses

The paper (§6.1.4, p. 65) notes that BARELY is "ALMOST's converse":

• ALMOST p: p in worlds close to w₀, ¬p in w₀
• BARELY p: p in w₀, ¬p in worlds close to w₀

The positive and negative inferences are swapped. Both belong to the FORGET class because they share the property that either p or ¬p holds in the real world.

theorem JinKoenig2021.almost_barely_same_class : JinKoenig2021.almostProfile✝.subclass = JinKoenig2021.barelyProfile✝.subclass

ALMOST and BARELY share the FORGET class despite being converses.

theorem JinKoenig2021.almost_barely_converse : JinKoenig2021.almostProfile✝.positiveInference = "p in worlds close to w₀" ∧ JinKoenig2021.barelyProfile✝.negativeInference = "¬p in worlds close to w₀" ∧ JinKoenig2021.barelyProfile✝.positiveInference = "p at w₀" ∧ JinKoenig2021.almostProfile✝.negativeInference = "¬p in w₀"

ALMOST and BARELY swap their domains (@cite{jin-koenig-2021}, §6.1.4):

• ALMOST: p holds "close to w₀", ¬p in "w₀"
• BARELY: p holds in "w₀", ¬p "close to w₀" The real-world (w₀) and close-to-real-world domains are exchanged.