Entailment Closure on Roots

[BKG20] treat roots as networks of entailments, where some atoms entail others, and state two collocational restrictions as definitional: +result entails +state, and +cause entails +result.

Two levels of closure, each a mathlib ClosureOperator:

• Kind level (canonical): Root.closedKinds is the collocational closure Root.Kinds.close of the root's derived signature. Both book restrictions hold of closed signatures by construction (closedKinds_wellFormed).
• Atom level (label-tracking): Root.closedEntailments closes the labeled atom set under bkgRules (becomesState s ⇒ hasState s), packaged as bkgCloseOp. Only the result→state edge is expressible here — hasCause is nullary, so cause→result lives at kind level only (kind_closedEntailments_le).

Main declarations

• bkgRules, bkgClose, bkgCloseOp, Root.closedEntailments
• Root.closedKinds
• mem_kind_closedEntailments — the atom/kind bridge

Atom-level rules and closure

def Verb.bkgRules : LexEntailment → Finset LexEntailment

The documented B&K-G atom-level entailment rule: becomesState s ⇒ hasState s (a change of state to s entails the resulting state attribution s, label preserved). The cause→result restriction is not expressible at atom level (hasCause carries no label) and is handled by Root.Kinds.close.

Equations

• Verb.bkgRules (Verb.LexEntailment.becomesState s) = {Verb.LexEntailment.hasState s}
• Verb.bkgRules x✝ = ∅

theorem Verb.bkgRules_kind {a b : LexEntailment} (h : a ∈ bkgRules b) : a.kind = some LexKind.state ∧ b.kind = some LexKind.result

Every atom produced by bkgRules is a state atom, produced from a result atom.

theorem Verb.bkgRules_output_inert {a b : LexEntailment} (h : a ∈ bkgRules b) : bkgRules a = ∅

Rule outputs trigger no further rules: the closure stabilizes in one step.

def Verb.bkgClose (atoms : Finset LexEntailment) : Finset LexEntailment

Close an atom set under bkgRules: adjoin everything the rules fire from a member.

Equations

• Verb.bkgClose atoms = atoms ∪ atoms.biUnion Verb.bkgRules

theorem Verb.le_bkgClose (atoms : Finset LexEntailment) : atoms ≤ bkgClose atoms

theorem Verb.bkgClose_mono {s t : Finset LexEntailment} (h : s ≤ t) : bkgClose s ≤ bkgClose t

theorem Verb.bkgClose_idem (s : Finset LexEntailment) : bkgClose (bkgClose s) = bkgClose s

def Verb.bkgCloseOp : ClosureOperator (Finset LexEntailment)

The atom-level closure as a mathlib ClosureOperator.

Equations

• Verb.bkgCloseOp = { toFun := Verb.bkgClose, monotone' := ⋯, le_closure' := Verb.le_bkgClose, idempotent' := Verb.bkgClose_idem, isClosed_iff := @Verb.bkgCloseOp._proof_1 }

def Verb.Root.closedEntailments (r : Root) : Finset LexEntailment

The B&K-G closure of the root's base entailments.

Equations

• r.closedEntailments = Verb.bkgClose r.entailments

Kind-level closure

def Verb.Root.closedKinds (r : Root) : Kinds

The closed kind signature: the collocational closure of the derived signature. Captures both book restrictions (result→state and cause→result).

Equations

• r.closedKinds = r.kinds.close

theorem Verb.Root.closedKinds_wellFormed (r : Root) : r.closedKinds.WellFormed

The closed signature satisfies the collocational constraints by construction — what RootEntailments.WellFormed used to stipulate is a theorem of closure.

theorem Verb.Root.kinds_le_closed (r : Root) : r.kinds ≤ r.closedKinds

theorem Verb.Root.closed_violatesBifurcation_iff (r : Root) : r.closedKinds.ViolatesBifurcation ↔ r.ViolatesBifurcation

Both theses are insensitive to the closure edges: a root violates Bifurcation iff its closed signature does.

The atom/kind bridge

theorem Verb.Root.mem_kind_closedEntailments {r : Root} {k : LexKind} : (∃ a ∈ r.closedEntailments, a.kind = some k) ↔ k ∈ r.kinds ∨ k = LexKind.state ∧ r.HasResult

Kinds realized by the atom-level closure: the base kinds plus a state kind whenever a result atom is present.

theorem Verb.Root.kind_closedEntailments_le (r : Root) {k : LexKind} (h : ∃ a ∈ r.closedEntailments, a.kind = some k) : k ∈ r.closedKinds

The atom-level closure realizes at most the kinds of the kind-level closure (strictly fewer when a root carries cause without a result atom — the cause→result edge is kind-level only).