Abney & Keshet (2025): PIP Compositional Operations

@cite{abney-keshet-2025} @cite{keshet-abney-2024}

The Glossa companion paper to @cite{keshet-abney-2024} enriches PIP with explicit set-based compositional operations: sigma evaluation (Σxφ), set-based generalized quantifiers (EVERY/SOME as set inclusion/intersection), three-argument modals with modal bases, and the FX type-lifting operation for restricted variables.

This file verifies these operations on finite models and demonstrates the paper's predictions about quantificational subordination, strong donkey anaphora, modal subordination, and the exists/sigma bridge.

Worked Examples

1. Sigma evaluation — Σx(farmer(x)) = {alice, bob} on a finite model
2. Sigma set algebra — Σx(φ∧ψ) = Σxφ ∩ Σxψ instantiated
3. GQ over sigma sets — EVERY(Σf farmer, Σf (farmer∧buyer)) via setEvery
4. Quantificational subordination — Σx(farmer(x) ∧ bought-donkey(x)) ⊆ Σx(farmer(x))
5. Exists↔sigma bridge — ∃x(farmer(x)) ↔ (Σx(farmer(x))).Nonempty
6. Strong donkey — summation pronouns as exhaustive sigma sets
7. FX thematic roles — ↑AGENT accumulates assertions
8. Paycheck pronouns — sigma set varies with external free variable
9. Modal subordination — MUST/MIGHT on two-world intensional model

inductive AbneyKeshet2025.Ent : Type

Four-entity domain: two farmers and two donkeys.

• alice : Ent
• bob : Ent
• spot : Ent
• rex : Ent

@[implicit_reducible]

instance AbneyKeshet2025.instDecidableEqEnt : DecidableEq Ent

Equations

• AbneyKeshet2025.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AbneyKeshet2025.instReprEnt : Repr Ent

Equations

• AbneyKeshet2025.instReprEnt = { reprPrec := AbneyKeshet2025.instReprEnt.repr }

def AbneyKeshet2025.instReprEnt.repr : Ent → ℕ → Std.Format

Equations

• AbneyKeshet2025.instReprEnt.repr AbneyKeshet2025.Ent.alice prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.Ent.alice")).group prec✝
• AbneyKeshet2025.instReprEnt.repr AbneyKeshet2025.Ent.bob prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.Ent.bob")).group prec✝
• AbneyKeshet2025.instReprEnt.repr AbneyKeshet2025.Ent.spot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.Ent.spot")).group prec✝
• AbneyKeshet2025.instReprEnt.repr AbneyKeshet2025.Ent.rex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.Ent.rex")).group prec✝

inductive AbneyKeshet2025.W1 : Type

Single-world model (extensional fragment).

• w0 : W1

@[implicit_reducible]

instance AbneyKeshet2025.instDecidableEqW1 : DecidableEq W1

Equations

• AbneyKeshet2025.instDecidableEqW1 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance AbneyKeshet2025.instReprW1 : Repr W1

Equations

• AbneyKeshet2025.instReprW1 = { reprPrec := AbneyKeshet2025.instReprW1.repr }

def AbneyKeshet2025.instReprW1.repr : W1 → ℕ → Std.Format

Equations

• AbneyKeshet2025.instReprW1.repr AbneyKeshet2025.W1.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.W1.w0")).group prec✝

@[implicit_reducible]

instance AbneyKeshet2025.instInhabitedW1 : Inhabited W1

Equations

• AbneyKeshet2025.instInhabitedW1 = { default := AbneyKeshet2025.instInhabitedW1.default }

def AbneyKeshet2025.instInhabitedW1.default : W1

Equations

• AbneyKeshet2025.instInhabitedW1.default = AbneyKeshet2025.W1.w0

@[implicit_reducible]

instance AbneyKeshet2025.instFiniteDomainEnt : Semantics.PIP.FiniteDomain Ent

Equations

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

@[implicit_reducible]

instance AbneyKeshet2025.instFintypeW1 : Fintype W1

Equations

• AbneyKeshet2025.instFintypeW1 = { elems := {AbneyKeshet2025.W1.w0}, complete := AbneyKeshet2025.instFintypeW1._proof_1 }

def AbneyKeshet2025.farmerBody : Ent → Semantics.PIP.PIPExprF W1 Ent

Farmer predicate: true for alice and bob.

Equations

• AbneyKeshet2025.farmerBody AbneyKeshet2025.Ent.alice = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.farmerBody AbneyKeshet2025.Ent.bob = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.farmerBody AbneyKeshet2025.Ent.spot = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false
• AbneyKeshet2025.farmerBody AbneyKeshet2025.Ent.rex = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false

def AbneyKeshet2025.donkeyBody : Ent → Semantics.PIP.PIPExprF W1 Ent

Donkey predicate: true for spot and rex.

Equations

• AbneyKeshet2025.donkeyBody AbneyKeshet2025.Ent.spot = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.donkeyBody AbneyKeshet2025.Ent.rex = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.donkeyBody AbneyKeshet2025.Ent.alice = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false
• AbneyKeshet2025.donkeyBody AbneyKeshet2025.Ent.bob = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false

theorem AbneyKeshet2025.sigma_farmer_alice : Ent.alice ∈ Semantics.PIP.sigmaEval farmerBody W1.w0

Alice is a farmer (in the sigma set).

theorem AbneyKeshet2025.sigma_farmer_bob : Ent.bob ∈ Semantics.PIP.sigmaEval farmerBody W1.w0

Bob is a farmer.

theorem AbneyKeshet2025.sigma_farmer_not_spot : Ent.spot ∉ Semantics.PIP.sigmaEval farmerBody W1.w0

Spot is not a farmer.

theorem AbneyKeshet2025.sigma_farmer_not_rex : Ent.rex ∉ Semantics.PIP.sigmaEval farmerBody W1.w0

Rex is not a farmer.

theorem AbneyKeshet2025.sigma_donkey_spot : Ent.spot ∈ Semantics.PIP.sigmaEval donkeyBody W1.w0

Spot is a donkey.

theorem AbneyKeshet2025.sigma_donkey_not_alice : Ent.alice ∉ Semantics.PIP.sigmaEval donkeyBody W1.w0

Alice is not a donkey.

theorem AbneyKeshet2025.sigma_conj_farmer_donkey : Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (donkeyBody d)) W1.w0 = Semantics.PIP.sigmaEval farmerBody W1.w0 ∩ Semantics.PIP.sigmaEval donkeyBody W1.w0

Σx(farmer ∧ donkey) = Σx(farmer) ∩ Σx(donkey) — no entity is both.

theorem AbneyKeshet2025.sigma_disj_farmer_donkey : Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).disj (donkeyBody d)) W1.w0 = Semantics.PIP.sigmaEval farmerBody W1.w0 ∪ Semantics.PIP.sigmaEval donkeyBody W1.w0

Σx(farmer ∨ donkey) = Σx(farmer) ∪ Σx(donkey) — all four entities.

theorem AbneyKeshet2025.farmer_donkey_disjoint (d : Ent) : d ∉ Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (donkeyBody d)) W1.w0

Verify: the farmer∧donkey intersection is empty.

def AbneyKeshet2025.boughtDonkeyBody : Ent → Semantics.PIP.PIPExprF W1 Ent

"Bought a donkey" predicate: alice and bob each bought one.

Equations

• AbneyKeshet2025.boughtDonkeyBody AbneyKeshet2025.Ent.alice = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.boughtDonkeyBody AbneyKeshet2025.Ent.bob = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.boughtDonkeyBody AbneyKeshet2025.Ent.spot = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false
• AbneyKeshet2025.boughtDonkeyBody AbneyKeshet2025.Ent.rex = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false

theorem AbneyKeshet2025.every_farmer_bought_donkey : Semantics.PIP.setEvery (Semantics.PIP.sigmaEval farmerBody W1.w0) (Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0)

EVERY(Σf farmer, Σf (farmer ∧ boughtDonkey)) — via setEvery.

"Every farmer bought a donkey" modeled as: the set of farmers is a subset of the set of farmer-buyers. This connects to the GQ bridge in Bridges.lean via setEvery_eq_pipEvery.

theorem AbneyKeshet2025.no_donkey_is_farmer : ¬Semantics.PIP.setSome (Semantics.PIP.sigmaEval donkeyBody W1.w0) (Semantics.PIP.sigmaEval farmerBody W1.w0)

SOME(Σf donkey, Σf farmerBody) — no donkey is a farmer. This demonstrates setSome negation: the intersection is empty.

theorem AbneyKeshet2025.farmer_buyer_subordination : Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0 ⊆ Semantics.PIP.sigmaEval farmerBody W1.w0

Quantificational subordination:

"Every farmer bought a donkey. He vaccinated it."

The subordinate quantifier's sigma set (farmers who bought a donkey and vaccinated it) is a subset of the main quantifier's sigma set (farmers). This follows from sigma_subordination.

theorem AbneyKeshet2025.farmer_buyer_alice : Ent.alice ∈ Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0

All farmer-buyers are indeed farmers (pointwise verification).

theorem AbneyKeshet2025.farmer_buyer_spot_excluded : Ent.spot ∉ Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0

theorem AbneyKeshet2025.exists_farmer : (Semantics.PIP.PIPExprF.exists_ farmerBody).truth W1.w0 = true

∃x(farmer(x)) is true (at least one farmer exists).

theorem AbneyKeshet2025.exists_farmer_bridge : (Semantics.PIP.PIPExprF.exists_ farmerBody).truth W1.w0 = true ↔ (Semantics.PIP.sigmaEval farmerBody W1.w0).Nonempty

The sigma bridge: ∃x(farmer(x)) ↔ nonempty sigma set.

theorem AbneyKeshet2025.forall_farmer_false : (Semantics.PIP.PIPExprF.forall_ farmerBody).truth W1.w0 = false

∀x(farmer(x)) is false (donkeys are not farmers).

Strong donkey anaphora via summation pronouns (paper's §4.3 analysis):

"Every farmer who bought a donkey vaccinated them."

The pronoun "them" is a summation pronoun: its denotation is the sigma set of all farmer-buyers, not a single witness. As noted in PIP.Composition, summation pronoun denotation IS sigmaEval — the distinction from simple pronouns is presuppositional (PL vs SG), handled by PIP.Bridges.plural.

theorem AbneyKeshet2025.strong_donkey_alice : Ent.alice ∈ Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0

Both alice and bob are in the sigma set — exhaustive, not a single witness.

theorem AbneyKeshet2025.strong_donkey_bob : Ent.bob ∈ Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0

theorem AbneyKeshet2025.strong_donkey_plural : Semantics.PIP.Bridges.plural (Semantics.PIP.sigmaEval (fun (d : Ent) => (farmerBody d).conj (boughtDonkeyBody d)) W1.w0)

The sigma set has 2+ elements → plural presupposition satisfied.

def AbneyKeshet2025.agentRole : Ent → W1 → Bool

AGENT role predicate: alice and bob are agents.

Equations

• AbneyKeshet2025.agentRole AbneyKeshet2025.Ent.alice x✝ = true
• AbneyKeshet2025.agentRole AbneyKeshet2025.Ent.bob x✝ = true
• AbneyKeshet2025.agentRole AbneyKeshet2025.Ent.spot x✝ = false
• AbneyKeshet2025.agentRole AbneyKeshet2025.Ent.rex x✝ = false

def AbneyKeshet2025.patientRole : Ent → W1 → Bool

PATIENT role predicate: spot and rex are patients.

Equations

• AbneyKeshet2025.patientRole AbneyKeshet2025.Ent.spot x✝ = true
• AbneyKeshet2025.patientRole AbneyKeshet2025.Ent.rex x✝ = true
• AbneyKeshet2025.patientRole AbneyKeshet2025.Ent.alice x✝ = false
• AbneyKeshet2025.patientRole AbneyKeshet2025.Ent.bob x✝ = false

def AbneyKeshet2025.buyEvent : W1 → Bool

Equations

• AbneyKeshet2025.buyEvent x✝ = true

theorem AbneyKeshet2025.fx_agent_alice : Semantics.PIP.fxApply agentRole buyEvent Ent.alice W1.w0 = true

↑AGENT(buy)(alice) = true — alice is an agent of buying.

theorem AbneyKeshet2025.fx_agent_spot : Semantics.PIP.fxApply agentRole buyEvent Ent.spot W1.w0 = false

↑AGENT(buy)(spot) = false — spot is not an agent.

theorem AbneyKeshet2025.fx_double_spot : Semantics.PIP.fxApply patientRole (Semantics.PIP.fxApply agentRole buyEvent Ent.spot) Ent.spot W1.w0 = false

Iterated FX: ↑PATIENT(↑AGENT(buy))(spot) = false — agent fails for spot.

theorem AbneyKeshet2025.fx_double_decomposes : Semantics.PIP.fxApply patientRole (Semantics.PIP.fxApply agentRole buyEvent Ent.alice) Ent.alice W1.w0 = (patientRole Ent.alice W1.w0 && agentRole Ent.alice W1.w0 && buyEvent W1.w0)

↑PATIENT(↑AGENT(buy))(alice, alice) — decomposes by fxApply_twice.

Paycheck pronouns (paper's §4.2, Karttunen 1969, Jacobson 2000):

"Almost every girl brought the diorama she made to class. Very few of them forgot it at home."

The pronoun "it" is a summation pronoun whose antecedent formula D ≡ DIORAMA([d]) ∧ MADE(x, d) contains a free variable x bound by a different quantifier at the pronoun's use site vs its antecedent's. The sigma set ΣdD varies with x: when x = alice, it denotes alice's diorama(s); when x = bob, bob's diorama(s).

This is the defining property of paycheck pronouns. PIP handles them via summation pronouns with formula labels that contain free variables. Dynamic logics struggle with this because they only store individuals already quantified over, not formulas with free variables.

def AbneyKeshet2025.dioramaBody : Ent → Semantics.PIP.PIPExprF W1 Ent

Diorama predicate: d1 and d2 are dioramas.

Equations

• AbneyKeshet2025.dioramaBody AbneyKeshet2025.Ent.spot = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.dioramaBody AbneyKeshet2025.Ent.rex = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.dioramaBody AbneyKeshet2025.Ent.alice = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false
• AbneyKeshet2025.dioramaBody AbneyKeshet2025.Ent.bob = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false

def AbneyKeshet2025.madeBody (maker : Ent) : Ent → Semantics.PIP.PIPExprF W1 Ent

"Made" relation parameterized by maker (external free variable x): alice made spot (d1), bob made rex (d2).

Equations

• AbneyKeshet2025.madeBody AbneyKeshet2025.Ent.alice AbneyKeshet2025.Ent.spot = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.madeBody AbneyKeshet2025.Ent.bob AbneyKeshet2025.Ent.rex = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => true
• AbneyKeshet2025.madeBody maker x✝ = Semantics.PIP.PIPExprF.pred fun (x : AbneyKeshet2025.W1) => false

def AbneyKeshet2025.paycheckBody (maker d : Ent) : Semantics.PIP.PIPExprF W1 Ent

Paycheck body: D ≡ DIORAMA([d]) ∧ MADE(x, d) with x as free variable. The sigma set ΣdD depends on who x is.

Equations

• AbneyKeshet2025.paycheckBody maker d = (AbneyKeshet2025.dioramaBody d).conj (AbneyKeshet2025.madeBody maker d)

theorem AbneyKeshet2025.paycheck_alice_spot : Ent.spot ∈ Semantics.PIP.sigmaEval (paycheckBody Ent.alice) W1.w0

When x = alice, ΣdD = {spot} (alice's diorama).

theorem AbneyKeshet2025.paycheck_alice_not_rex : Ent.rex ∉ Semantics.PIP.sigmaEval (paycheckBody Ent.alice) W1.w0

theorem AbneyKeshet2025.paycheck_bob_rex : Ent.rex ∈ Semantics.PIP.sigmaEval (paycheckBody Ent.bob) W1.w0

When x = bob, ΣdD = {rex} (bob's diorama).

theorem AbneyKeshet2025.paycheck_bob_not_spot : Ent.spot ∉ Semantics.PIP.sigmaEval (paycheckBody Ent.bob) W1.w0

theorem AbneyKeshet2025.paycheck_varies : Semantics.PIP.sigmaEval (paycheckBody Ent.alice) W1.w0 ≠ Semantics.PIP.sigmaEval (paycheckBody Ent.bob) W1.w0

The paycheck property: the sigma set varies with the external free variable. This is what distinguishes paycheck pronouns from ordinary anaphora — the pronoun's denotation depends on who the binder is.

theorem AbneyKeshet2025.paycheck_alice_single : Semantics.PIP.Bridges.single (Semantics.PIP.sigmaEval (paycheckBody Ent.alice) W1.w0)

Each maker's sigma set is a singleton — satisfying the SG presupposition.

theorem AbneyKeshet2025.paycheck_bob_single : Semantics.PIP.Bridges.single (Semantics.PIP.sigmaEval (paycheckBody Ent.bob) W1.w0)

inductive AbneyKeshet2025.W2 : Type

Two-world model for modal subordination.

• actual : W2
• alt : W2

@[implicit_reducible]

instance AbneyKeshet2025.instDecidableEqW2 : DecidableEq W2

Equations

• AbneyKeshet2025.instDecidableEqW2 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def AbneyKeshet2025.instReprW2.repr : W2 → ℕ → Std.Format

Equations

• AbneyKeshet2025.instReprW2.repr AbneyKeshet2025.W2.actual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.W2.actual")).group prec✝
• AbneyKeshet2025.instReprW2.repr AbneyKeshet2025.W2.alt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AbneyKeshet2025.W2.alt")).group prec✝

@[implicit_reducible]

instance AbneyKeshet2025.instReprW2 : Repr W2

Equations

• AbneyKeshet2025.instReprW2 = { reprPrec := AbneyKeshet2025.instReprW2.repr }

def AbneyKeshet2025.instInhabitedW2.default : W2

Equations

• AbneyKeshet2025.instInhabitedW2.default = AbneyKeshet2025.W2.actual

@[implicit_reducible]

instance AbneyKeshet2025.instInhabitedW2 : Inhabited W2

Equations

• AbneyKeshet2025.instInhabitedW2 = { default := AbneyKeshet2025.instInhabitedW2.default }

@[implicit_reducible]

instance AbneyKeshet2025.instFintypeW2 : Fintype W2

Equations

• AbneyKeshet2025.instFintypeW2 = { elems := {AbneyKeshet2025.W2.actual, AbneyKeshet2025.W2.alt}, complete := AbneyKeshet2025.instFintypeW2._proof_1 }

Modal subordination (paper's §4.5, Roberts 1987 wolf example):

"A wolf might come in. It would eat you first."

MIGHT(β_w, ΣwW) where W ≡ (WOLF([x]) ∧ ENTERS(x)) MUST(β_w, ΣwW, ΣwE) where E ≡ (W ∧ TIM([t]) ∧ EATS(x,t))

The nuclear scope of the first sentence is stored in label W. The restriction of the second sentence's MUST is anaphoric to W — this is modal subordination, parallel to quantificational subordination.

def AbneyKeshet2025.modalBase : Set W2

Modal base: actual can access alt, and alt accesses itself.

Equations

• AbneyKeshet2025.modalBase = {AbneyKeshet2025.W2.actual, AbneyKeshet2025.W2.alt}

def AbneyKeshet2025.wolfEntersW : Set W2

Worlds where a wolf enters (only alt).

Equations

• AbneyKeshet2025.wolfEntersW = {AbneyKeshet2025.W2.alt}

def AbneyKeshet2025.wolfEatsTimW : Set W2

Worlds where the wolf eats Tim (also only alt).

Equations

• AbneyKeshet2025.wolfEatsTimW = {AbneyKeshet2025.W2.alt}

theorem AbneyKeshet2025.wolf_might_enter : Semantics.PIP.mightBase modalBase Set.univ wolfEntersW

MIGHT(β, ⊤, wolfEnters) — a wolf might enter. The modal base intersected with the wolf-enters set is nonempty.

theorem AbneyKeshet2025.wolf_must_eat_tim : Semantics.PIP.mustBase modalBase wolfEntersW wolfEatsTimW

MUST(β, wolfEnters, wolfEatsTim) — it would eat Tim. Modal subordination: the restriction wolfEnters (from the first sentence's label W) constrains MUST. Every wolf-entry world is also a wolf-eats-Tim world.

theorem AbneyKeshet2025.wolf_not_must_enter : ¬Semantics.PIP.mustBase modalBase Set.univ wolfEntersW

Modal duality instantiated: ¬MUST(β, ⊤, wolfEnters) because the wolf doesn't enter at actual.

theorem AbneyKeshet2025.wolf_might_not_enter : Semantics.PIP.mightBase modalBase Set.univ wolfEntersWᶜ

Modal duality: ¬MUST ↔ MIGHT(complement). The wolf doesn't necessarily enter, so it's possible it doesn't.