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

def Phenomena.Negation.Studies.JinKoenig2021.survey : Typology.ENSurveyResult

The overall survey: 722 languages, EN in 74 (37 genera). Data is defined in Phenomena.Negation.Typology.enSurvey to avoid duplication across study files.

Equations

• Phenomena.Negation.Studies.JinKoenig2021.survey = Phenomena.Negation.Typology.enSurvey

structure Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerCount.repr : TriggerCount → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerCount : Repr TriggerCount

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerCount = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerCount.repr }

def Phenomena.Negation.Studies.JinKoenig2021.triggerCounts : List TriggerCount

Equations

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

theorem Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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.

instance Phenomena.Negation.Studies.JinKoenig2021.instDecidableEqLicensingCondition : DecidableEq LicensingCondition

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.instBEqLicensingCondition.beq : LicensingCondition → LicensingCondition → Bool

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqLicensingCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.Studies.JinKoenig2021.instBEqLicensingCondition : BEq LicensingCondition

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqLicensingCondition = { beq := Phenomena.Negation.Studies.JinKoenig2021.instBEqLicensingCondition.beq }

def Phenomena.Negation.Studies.JinKoenig2021.instReprLicensingCondition.repr : LicensingCondition → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.JinKoenig2021.instReprLicensingCondition : Repr LicensingCondition

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprLicensingCondition = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprLicensingCondition.repr }

inductive Phenomena.Negation.Studies.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

instance Phenomena.Negation.Studies.JinKoenig2021.instDecidableEqTriggerSubclass : DecidableEq TriggerSubclass

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.instBEqTriggerSubclass.beq : TriggerSubclass → TriggerSubclass → Bool

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqTriggerSubclass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.Studies.JinKoenig2021.instBEqTriggerSubclass : BEq TriggerSubclass

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqTriggerSubclass = { beq := Phenomena.Negation.Studies.JinKoenig2021.instBEqTriggerSubclass.beq }

def Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerSubclass.repr : TriggerSubclass → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerSubclass : Repr TriggerSubclass

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerSubclass = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerSubclass.repr }

def Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.licensingCondition : TriggerSubclass → LicensingCondition

Each subclass belongs to exactly one licensing condition.

Equations

• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.fear.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.propositionalAttitude
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.regret.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.propositionalAttitude
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.deny.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.propositionalAttitude
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.forget.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.propositionalAttitude
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.before.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.temporalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.cannotWait.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.temporalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.since.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.temporalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.rarely.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.temporalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.impossible.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.logicalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.without.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.logicalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.unless.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.logicalOperator
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.moreThan.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.comparative
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.differentThan.licensingCondition = Phenomena.Negation.Studies.JinKoenig2021.LicensingCondition.comparative
• Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.tooTo.licensingCondition = Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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)

instance Phenomena.Negation.Studies.JinKoenig2021.instReprDualInferenceProfile : Repr DualInferenceProfile

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprDualInferenceProfile = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprDualInferenceProfile.repr }

def Phenomena.Negation.Studies.JinKoenig2021.instReprDualInferenceProfile.repr : DualInferenceProfile → ℕ → Std.Format

Equations

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

def Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.negativeValenceEntailsDual (v : Semantics.Attitudes.Preferential.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

• Phenomena.Negation.Studies.JinKoenig2021.negativeValenceEntailsDual v = (v == Semantics.Attitudes.Preferential.AttitudeValence.negative)

theorem Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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.QuestionDen 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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.class2_licenses_EN : negativeValenceEntailsDual Semantics.Attitudes.Preferential.AttitudeValence.negative = true ∧ negativeValenceEntailsDual Semantics.Attitudes.Preferential.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 Phenomena.Negation.Studies.JinKoenig2021.deny_EN_via_negRaising : Semantics.Attitudes.NegRaising.negRaisingAvailable Semantics.Attitudes.Doxastic.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 Phenomena.Negation.Studies.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

instance Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerAttestation : Repr TriggerAttestation

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerAttestation = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerAttestation.repr }

def Phenomena.Negation.Studies.JinKoenig2021.instReprTriggerAttestation.repr : TriggerAttestation → ℕ → Std.Format

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.triggerAttestations : List TriggerAttestation

Equations

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

theorem Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.InferenceDomainType : Type

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

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

instance Phenomena.Negation.Studies.JinKoenig2021.instDecidableEqInferenceDomainType : DecidableEq InferenceDomainType

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.instBEqInferenceDomainType.beq : InferenceDomainType → InferenceDomainType → Bool

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqInferenceDomainType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Negation.Studies.JinKoenig2021.instBEqInferenceDomainType : BEq InferenceDomainType

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqInferenceDomainType = { beq := Phenomena.Negation.Studies.JinKoenig2021.instBEqInferenceDomainType.beq }

def Phenomena.Negation.Studies.JinKoenig2021.instReprInferenceDomainType.repr : InferenceDomainType → ℕ → Std.Format

Equations

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

instance Phenomena.Negation.Studies.JinKoenig2021.instReprInferenceDomainType : Repr InferenceDomainType

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprInferenceDomainType = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprInferenceDomainType.repr }

def Phenomena.Negation.Studies.JinKoenig2021.TriggerSubclass.inferenceDomainType : TriggerSubclass → InferenceDomainType

Each trigger subclass has a characteristic domain type.

Equations

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

theorem Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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.

theorem Phenomena.Negation.Studies.JinKoenig2021.impossible_licensing : TriggerSubclass.impossible.licensingCondition = LicensingCondition.logicalOperator

IMPOSSIBLE maps to the logical operator licensing condition.

theorem Phenomena.Negation.Studies.JinKoenig2021.not_impossible_activates_p (f : Semantics.Modality.Kratzer.ModalBase) (g : Semantics.Modality.Kratzer.OrderingSource) (p : BProp Semantics.Attitudes.Intensional.World) (w : Semantics.Attitudes.Intensional.World) : Semantics.Modality.Kratzer.necessity f g (fun (w' : Semantics.Attitudes.Intensional.World) => !p w') w = false → Semantics.Modality.Kratzer.possibility f g p w = true

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 Phenomena.Negation.Studies.JinKoenig2021.withoutSem {W : Type u_1} (q p : BProp W) : BProp W

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

Equations

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

theorem Phenomena.Negation.Studies.JinKoenig2021.without_entails_not_p {W : Type u_1} (q p : BProp W) (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 Phenomena.Negation.Studies.JinKoenig2021.without_entails_q {W : Type u_1} (q p : BProp W) (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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.unlessSem {W : Type u_1} (q p : BProp W) : BProp W

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

Equations

• Phenomena.Negation.Studies.JinKoenig2021.unlessSem q p = Semantics.Conditionals.materialImpB (fun (w : W) => !p w) q

theorem Phenomena.Negation.Studies.JinKoenig2021.unless_modus_ponens {W : Type u_1} (q p : BProp W) (w : W) (hcond : unlessSem q p w = true) (hnp : p w = false) : q w = true

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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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	ImplicativeBuilder.negative
STOP/PREVENT	Causation/Builder	CausativeBuilder.prevent
ALMOST	Degree/Comparative	threshold proximity

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

theorem Phenomena.Negation.Studies.JinKoenig2021.forget_grounded_in_implicativity : Nadathur2024.Implicative.ImplicativeBuilder.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 Phenomena.Negation.Studies.JinKoenig2021.prevent_is_causative_builder : NadathurLauer2020.Builder.CausativeBuilder.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.all_conditions_grounded : negativeValenceEntailsDual Semantics.Attitudes.Preferential.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 Phenomena.Negation.Studies.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.

instance Phenomena.Negation.Studies.JinKoenig2021.instDecidableEqENDefinition : DecidableEq ENDefinition

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instDecidableEqENDefinition = Phenomena.Negation.Studies.JinKoenig2021.instDecidableEqENDefinition.decEq

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

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.instBEqENDefinition.beq : ENDefinition → ENDefinition → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Negation.Studies.JinKoenig2021.instBEqENDefinition.beq x✝¹ x✝ = false

instance Phenomena.Negation.Studies.JinKoenig2021.instBEqENDefinition : BEq ENDefinition

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instBEqENDefinition = { beq := Phenomena.Negation.Studies.JinKoenig2021.instBEqENDefinition.beq }

instance Phenomena.Negation.Studies.JinKoenig2021.instReprENDefinition : Repr ENDefinition

Equations

• Phenomena.Negation.Studies.JinKoenig2021.instReprENDefinition = { reprPrec := Phenomena.Negation.Studies.JinKoenig2021.instReprENDefinition.repr }

def Phenomena.Negation.Studies.JinKoenig2021.instReprENDefinition.repr : ENDefinition → ℕ → Std.Format

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.isEN (d : ENDefinition) : Bool

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

Equations

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

def Phenomena.Negation.Studies.JinKoenig2021.french_ne_fear : ENDefinition

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

Equations

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

def Phenomena.Negation.Studies.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

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

theorem Phenomena.Negation.Studies.JinKoenig2021.fear_is_en : isEN french_ne_fear = true

theorem Phenomena.Negation.Studies.JinKoenig2021.wish_is_not_en : isEN french_ne_wish = false

Connecting JK2021 licensing conditions to Rett's ambidirectionality

@cite{rett-2026} (formalized in Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.fear_triggers_are_rett_ambidirectional : TriggerSubclass.fear.licensingCondition = LicensingCondition.propositionalAttitude ∧ negativeValenceEntailsDual Semantics.Attitudes.Preferential.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 Phenomena.Negation.Studies.JinKoenig2021.negative_valence_is_en_trigger (v : Core.Verbs.VerbCore) (h : v.preferentialValence = some Semantics.Attitudes.Preferential.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 Phenomena.Negation.Studies.JinKoenig2021.negative_implicative_is_en_trigger (v : Core.Verbs.VerbCore) (h : v.implicativeBuilder = some Nadathur2024.Implicative.ImplicativeBuilder.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 Phenomena.Negation.Studies.JinKoenig2021.prevent_builder_is_en_trigger (v : Core.Verbs.VerbCore) (h : v.causativeBuilder = some NadathurLauer2020.Builder.CausativeBuilder.prevent) : v.isENTrigger = true

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

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

"fear" → negative valence → EN trigger.

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

"dread" → negative valence → EN trigger.

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

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

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

"forget" → negative implicative → EN trigger.

theorem Phenomena.Negation.Studies.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 Phenomena.Negation.Studies.JinKoenig2021.almost_barely_same_class : Phenomena.Negation.Studies.JinKoenig2021.almostProfile✝.subclass = Phenomena.Negation.Studies.JinKoenig2021.barelyProfile✝.subclass

ALMOST and BARELY share the FORGET class despite being converses.

theorem Phenomena.Negation.Studies.JinKoenig2021.almost_barely_converse : Phenomena.Negation.Studies.JinKoenig2021.almostProfile✝.positiveInference = "p in worlds close to w₀" ∧ Phenomena.Negation.Studies.JinKoenig2021.barelyProfile✝.negativeInference = "¬p in worlds close to w₀" ∧ Phenomena.Negation.Studies.JinKoenig2021.barelyProfile✝¹.positiveInference = "p at w₀" ∧ Phenomena.Negation.Studies.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.