Structural operations on DRSs

This file develops the structural theory of the DRS type of DRS/Defs.lean: renaming of discourse referents, the merge algebra, transport of the extension relation along renaming, occurrence and freeness predicates, and accessibility. Renaming along a bijection is [KR93]'s alphabetic variant (the prose preceding Def. 1.4.8).

Main declarations

• DRS.map: renaming along f : V → W, functorial.
• DRS.varFinset, DRS.freeVarFinset: occurring and free referents.
• DRS.IsProper: no free referent (Def. 1.4.2–1.4.3); decidable.
• DRS.ReuseFreeAt: no referent declared twice along a nesting path.
• DRS.accessibleFrom, DRS.Accessible: accessible referents, computed by [vE06]'s left-and-up walk; decidable.
• AccessibleTo, accessibleDomain: [GBM24]'s accessibility preorder over the sub-DRSs of a host, and its accessible domain A_K.

Main statements

• DRS.Accessible.exists_mem_accessibleDomain: every computed accessibility verdict is realized by genuine accessibility edges.

Conditions

Renaming

@[irreducible]

def DRT.Condition.map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) : Condition L V → Condition L W

Rename discourse referents along f throughout a condition.

Equations

• DRT.Condition.map f (DRT.Condition.rel R args) = DRT.Condition.rel R fun (i : Fin n) => f (args i)
• DRT.Condition.map f (DRT.Condition.eq a b) = DRT.Condition.eq (f a) (f b)
• DRT.Condition.map f (DRT.Condition.neg K) = DRT.Condition.neg (DRT.Box.map f (DRT.Condition.map f) K)
• DRT.Condition.map f (DRT.Condition.imp a c) = DRT.Condition.imp (DRT.Box.map f (DRT.Condition.map f) a) (DRT.Box.map f (DRT.Condition.map f) c)
• DRT.Condition.map f (DRT.Condition.dis l r) = DRT.Condition.dis (DRT.Box.map f (DRT.Condition.map f) l) (DRT.Box.map f (DRT.Condition.map f) r)

@[simp]

theorem DRT.Condition.map_id {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) : map id c = c

Renaming a condition along the identity is the identity.

theorem DRT.Condition.map_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {X : Type u_2} [DecidableEq W] [DecidableEq X] (g : W → X) (f : V → W) (c : Condition L V) : map g (map f c) = map (g ∘ f) c

Renaming a condition along a composite is the composite of the renamings.

Occurring referents

@[irreducible]

def DRT.Condition.varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Condition L V → Finset V

Occurring referents (free or bound) in a condition, as a Finset — the DRS analogue of mathlib's Term.varFinset. Membership x ∈ varFinset c is decidable, so downstream consumers get decidable occurrence for free.

Equations

• One or more equations did not get rendered due to their size.
• (DRT.Condition.rel R args).varFinset = Finset.image args Finset.univ
• (DRT.Condition.eq a b).varFinset = {a, b}
• (DRT.Condition.neg K).varFinset = K.referents ∪ List.foldr (fun (x1 x2 : Finset V) => x1 ∪ x2) ∅ (List.map DRT.Condition.varFinset K.conditions)

def DRT.Condition.varFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs : List (Condition L V)) : Finset V

Occurring referents in a list of conditions.

Equations

• DRT.Condition.varFinsetL cs = List.foldr (fun (x1 x2 : Finset V) => x1 ∪ x2) ∅ (List.map DRT.Condition.varFinset cs)

@[simp]

theorem DRT.Condition.varFinsetL_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : varFinsetL [] = ∅

@[simp]

theorem DRT.Condition.varFinsetL_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) (cs : List (Condition L V)) : varFinsetL (c :: cs) = c.varFinset ∪ varFinsetL cs

@[simp]

theorem DRT.Condition.varFinset_rel {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {n : ℕ} (R : L.Relations n) (args : Fin n → V) : (rel R args).varFinset = Finset.image args Finset.univ

@[simp]

theorem DRT.Condition.varFinset_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (u v : V) : (eq u v).varFinset = {u, v}

@[simp]

theorem DRT.Condition.varFinsetL_append {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs ds : List (Condition L V)) : varFinsetL (cs ++ ds) = varFinsetL cs ∪ varFinsetL ds

theorem DRT.Condition.varFinset_subset_varFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {c : Condition L V} {cs : List (Condition L V)} (hc : c ∈ cs) : c.varFinset ⊆ varFinsetL cs

A condition's occurring referents are among its list's.

Free discourse referents

@[irreducible]

def DRT.Condition.freeVarFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : Condition L V → Finset V

The free discourse referents of a condition.

Equations

• One or more equations did not get rendered due to their size.
• (DRT.Condition.rel R args).freeVarFinset = Finset.image args Finset.univ
• (DRT.Condition.eq a b).freeVarFinset = {a, b}
• (DRT.Condition.neg K).freeVarFinset = List.foldr (fun (x1 x2 : Finset V) => x1 ∪ x2) ∅ (List.map DRT.Condition.freeVarFinset K.conditions) \ K.referents

def DRT.Condition.freeVarFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs : List (Condition L V)) : Finset V

Free referents of a list of conditions.

Equations

• DRT.Condition.freeVarFinsetL cs = List.foldr (fun (x1 x2 : Finset V) => x1 ∪ x2) ∅ (List.map DRT.Condition.freeVarFinset cs)

@[simp]

theorem DRT.Condition.freeVarFinset_rel {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {n : ℕ} (R : L.Relations n) (args : Fin n → V) : (rel R args).freeVarFinset = Finset.image args Finset.univ

@[simp]

theorem DRT.Condition.freeVarFinset_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (u v : V) : (eq u v).freeVarFinset = {u, v}

@[simp]

theorem DRT.Condition.freeVarFinsetL_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] : freeVarFinsetL [] = ∅

@[simp]

theorem DRT.Condition.freeVarFinsetL_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) (cs : List (Condition L V)) : freeVarFinsetL (c :: cs) = c.freeVarFinset ∪ freeVarFinsetL cs

@[simp]

theorem DRT.Condition.freeVarFinsetL_append {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs ds : List (Condition L V)) : freeVarFinsetL (cs ++ ds) = freeVarFinsetL cs ∪ freeVarFinsetL ds

Reuse-freeness

No discourse referent is declared twice along a nesting path: each universe is fresh for the ambient declarations, threaded through sub-boxes the way verification threads the base (the antecedent of a ⇒ feeds its referents into the consequent). This is the hypothesis under which the total agree-off-universe semantics and the persistence semantics coincide (DRS.trueRel_iff_toRelAt in DRS/Indexed.lean).

@[irreducible]

def DRT.Condition.ReuseFreeAt {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) : Condition L V → Prop

A condition is reuse-free at ambient declarations X: each sub-box universe is fresh for the declarations in scope, threaded the way verification threads the base (the antecedent of a ⇒ feeds its referents into the consequent).

Equations

• One or more equations did not get rendered due to their size.
• DRT.Condition.ReuseFreeAt X (DRT.Condition.rel R args) = True
• DRT.Condition.ReuseFreeAt X (DRT.Condition.eq a b) = True
• DRT.Condition.ReuseFreeAt X (DRT.Condition.neg K) = (Disjoint X K.referents ∧ ∀ c ∈ K.conditions, DRT.Condition.ReuseFreeAt (X ∪ K.referents) c)

def DRT.Condition.ReuseFreeAllAt {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (cs : List (Condition L V)) : Prop

Reuse-freeness for a list of conditions.

Equations

• DRT.Condition.ReuseFreeAllAt X cs = ∀ c ∈ cs, DRT.Condition.ReuseFreeAt X c

@[simp]

theorem DRT.Condition.reuseFreeAt_rel {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) {n : ℕ} (R : L.Relations n) (args : Fin n → V) : ReuseFreeAt X (rel R args)

@[simp]

theorem DRT.Condition.reuseFreeAt_eq {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (u v : V) : ReuseFreeAt X (eq u v)

@[simp]

theorem DRT.Condition.reuseFreeAllAt_nil {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) : ReuseFreeAllAt X []

@[simp]

theorem DRT.Condition.reuseFreeAllAt_cons {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (c : Condition L V) (cs : List (Condition L V)) : ReuseFreeAllAt X (c :: cs) ↔ ReuseFreeAt X c ∧ ReuseFreeAllAt X cs

Accessibility threading

Accessibility (Def. 1.4.11) is relative to a host DRS: "u accessible at box B" means u lies in the universe of B or of a box on the path from the host down to B. A host-free ∃ D, WeakSubordinate K D ∧ u ∈ D.referents is vacuous, since a superordinate D introducing any referent can be manufactured. accScope computes accessibility top-down, by [vE06]'s walk in the directions left (from the consequent of a ⇒ to its antecedent) and up, threading the in-scope referents along the first path to the box declaring the target; the declarative counterpart is the host-anchored preorder AccessibleTo at the end of this file.

@[irreducible]

def DRT.Condition.accScope {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) : Condition L V → V → Option (Finset V)

Accessibility threading through a condition.

Equations

• One or more equations did not get rendered due to their size.
• DRT.Condition.accScope s (DRT.Condition.rel R args) x✝ = none
• DRT.Condition.accScope s (DRT.Condition.eq u v) x✝ = none

def DRT.Condition.accScopeL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) (cs : List (Condition L V)) (x : V) : Option (Finset V)

Accessibility threading through a list of conditions: the first hit wins.

Equations

• DRT.Condition.accScopeL s cs x = List.foldr (fun (r acc : Option (Finset V)) => r.orElse fun (x : Unit) => acc) none (List.map (fun (c : DRT.Condition L V) => DRT.Condition.accScope s c x) cs)

DRSs

Renaming

def DRT.DRS.map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) : DRS L V → DRS L W

Rename discourse referents along f : V → W throughout a DRS.

Equations

• DRT.DRS.map f = DRT.Box.map f (DRT.Condition.map f)

@[simp]

theorem DRT.DRS.referents_map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) (K : DRS L V) : (map f K).referents = Finset.image f K.referents

@[simp]

theorem DRT.DRS.conditions_map {L : FirstOrder.Language} {V : Type w} {W : Type x} [DecidableEq W] (f : V → W) (K : DRS L V) : (map f K).conditions = List.map (Condition.map f) K.conditions

@[simp]

theorem DRT.DRS.map_id {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : map id K = K

Renaming a DRS along the identity is the identity.

theorem DRT.DRS.map_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {X : Type u_2} [DecidableEq W] [DecidableEq X] (g : W → X) (f : V → W) (K : DRS L V) : map g (map f K) = map (g ∘ f) K

Renaming a DRS along a composite is the composite of the renamings.

theorem DRT.DRS.extends_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {M : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f g : Embedding W M) : Box.Extends (map (⇑e) K) f g ↔ Box.Extends K (f ∘ ⇑e) (g ∘ ⇑e)

Extension along a renamed DRS is extension of the precompositions.

theorem DRT.DRS.exists_extends_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {M : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f : Embedding W M) (P : Embedding V M → Prop) : (∃ (g : Embedding W M), Box.Extends (map (⇑e) K) f g ∧ P (g ∘ ⇑e)) ↔ ∃ (g : Embedding V M), Box.Extends K (f ∘ ⇑e) g ∧ P g

The extensions of f at K.map e are the extensions of f ∘ e at K, via precomposition.

theorem DRT.DRS.forall_extends_map {L : FirstOrder.Language} {V : Type w} {W : Type x} {M : Type u_1} [DecidableEq W] (e : V ≃ W) (K : DRS L V) (f : Embedding W M) (P : Embedding V M → Prop) : (∀ (g : Embedding W M), Box.Extends (map (⇑e) K) f g → P (g ∘ ⇑e)) ↔ ∀ (g : Embedding V M), Box.Extends K (f ∘ ⇑e) g → P g

The ∀ analogue of DRS.exists_extends_map.

Merge algebra

@[simp]

theorem DRT.DRS.empty_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : empty.merge K = K

@[simp]

theorem DRT.DRS.merge_empty {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.merge empty = K

theorem DRT.DRS.merge_assoc {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K₁ K₂ K₃ : DRS L V) : (K₁.merge K₂).merge K₃ = K₁.merge (K₂.merge K₃)

Occurring and free referents

def DRT.DRS.varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Finset V

Occurring referents in a DRS (its universe and those of its conditions).

Equations

• K.varFinset = K.referents ∪ DRT.Condition.varFinsetL K.conditions

@[simp]

theorem DRT.DRS.varFinset_mk {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (conds : List (Condition L V)) : varFinset { referents := U, conditions := conds } = U ∪ Condition.varFinsetL conds

theorem DRT.DRS.varFinsetL_subset_varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Condition.varFinsetL K.conditions ⊆ K.varFinset

A DRS's conditions' occurring referents are among the DRS's.

def DRT.DRS.freeVarFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Finset V

The free discourse referents of a DRS: referents occurring in its conditions and not bound by its universe or by an ancestor reachable "left and up" (the antecedent of a ⇒ threads its referents into the consequent). K.freeVarFinset ⊆ b says every referent of K is bound in context b.

Equations

• K.freeVarFinset = DRT.Condition.freeVarFinsetL K.conditions \ K.referents

@[simp]

theorem DRT.DRS.freeVarFinset_mk {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (U : Finset V) (conds : List (Condition L V)) : freeVarFinset { referents := U, conditions := conds } = Condition.freeVarFinsetL conds \ U

theorem DRT.DRS.freeVarFinset_subset_iff {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {U X : Finset V} {conds : List (Condition L V)} : freeVarFinset { referents := U, conditions := conds } ⊆ X ↔ Condition.freeVarFinsetL conds ⊆ X ∪ U

The characteristic form of the referential presupposition: a box's free referents are supplied by X iff its conditions' are supplied by the grown base.

theorem DRT.DRS.freeVarFinset_merge_subset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {X : Finset V} {K₁ K₂ : DRS L V} (h₁ : K₁.freeVarFinset ⊆ X) (h₂ : K₂.freeVarFinset ⊆ X ∪ K₁.referents) : (K₁.merge K₂).freeVarFinset ⊆ X

Merging preserves boundedness: the merge's free referents are supplied by X when the context's are and the increment's are supplied by the grown base.

def DRT.DRS.IsProper {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Prop

A DRS is proper iff it has no free discourse referent (Def. 1.4.2–1.4.3).

Equations

• K.IsProper = (K.freeVarFinset = ∅)

@[instance_reducible]

instance DRT.DRS.instDecidableIsProper {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : Decidable K.IsProper

Equations

• K.instDecidableIsProper = decidable_of_iff (K.freeVarFinset = ∅) ⋯

theorem DRT.DRS.isProper_merge {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {K₁ K₂ : DRS L V} (h₁ : K₁.IsProper) (h₂ : K₂.freeVarFinset ⊆ K₁.referents) : (K₁.merge K₂).IsProper

Merging preserves properness when the increment's free referents are supplied by the context DRS's universe.

Reuse-freeness

def DRT.DRS.ReuseFreeAt {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (K : DRS L V) : Prop

A DRS is reuse-free at ambient declarations X: its universe avoids X and its conditions are reuse-free at the grown set.

Equations

• DRT.DRS.ReuseFreeAt X K = (Disjoint X K.referents ∧ DRT.Condition.ReuseFreeAllAt (X ∪ K.referents) K.conditions)

@[simp]

theorem DRT.DRS.reuseFreeAt_mk {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X U : Finset V) (conds : List (Condition L V)) : ReuseFreeAt X { referents := U, conditions := conds } ↔ Disjoint X U ∧ Condition.ReuseFreeAllAt (X ∪ U) conds

Accessibility

def DRT.DRS.accScope {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) (K : DRS L V) (x : V) : Option (Finset V)

Descend K, accumulating in-scope referents s ([vE06]'s "left and up" walk); on reaching the box introducing x, return that box's in-scope set s ∪ U. The ⇒-consequent additionally sees the antecedent's universe.

Equations

• DRT.DRS.accScope s K x = if x ∈ K.referents then some (s ∪ K.referents) else DRT.Condition.accScopeL (s ∪ K.referents) K.conditions x

def DRT.DRS.accessibleFrom {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (T : DRS L V) (u : V) : Finset V

The referents accessible from u's introduction in T, as a decidable Finset; ∅ if u is not introduced in T. (Def. 1.4.11 defines accessibility of a referent from a condition; this is the derived referent-to-referent relation of the surrounding prose.)

Equations

• T.accessibleFrom u = (DRT.DRS.accScope ∅ T u).getD ∅

def DRT.DRS.Accessible {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (T : DRS L V) (u v : V) : Prop

v is accessible from u's position in T. Decidable (Finset membership).

Equations

• T.Accessible u v = (v ∈ T.accessibleFrom u)

@[instance_reducible]

instance DRT.DRS.instDecidableAccessible {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (T : DRS L V) (u v : V) : Decidable (T.Accessible u v)

Equations

• T.instDecidableAccessible u v = DRT.DRS.instDecidableAccessible._aux_1 T u v

Sub-box characterizations

The per-constructor forms of the condition-level predicates, phrased through the corresponding DRS-level notion of the sub-boxes, and the subset relations tying free to occurring referents.

@[simp]

theorem DRT.Condition.varFinset_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : (neg K).varFinset = K.varFinset

@[simp]

theorem DRT.Condition.varFinset_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a c : DRS L V) : (imp a c).varFinset = a.varFinset ∪ c.varFinset

@[simp]

theorem DRT.Condition.varFinset_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (l r : DRS L V) : (dis l r).varFinset = l.varFinset ∪ r.varFinset

@[simp]

theorem DRT.Condition.freeVarFinset_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : (neg K).freeVarFinset = K.freeVarFinset

@[simp]

theorem DRT.Condition.freeVarFinset_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (a c : DRS L V) : (imp a c).freeVarFinset = a.freeVarFinset ∪ c.freeVarFinset \ a.referents

@[simp]

theorem DRT.Condition.freeVarFinset_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (l r : DRS L V) : (dis l r).freeVarFinset = l.freeVarFinset ∪ r.freeVarFinset

theorem DRT.Condition.freeVarFinset_subset_varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (c : Condition L V) : c.freeVarFinset ⊆ c.varFinset

Free referents of a condition occur.

theorem DRT.DRS.freeVarFinset_subset_varFinset {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (K : DRS L V) : K.freeVarFinset ⊆ K.varFinset

Free referents occur.

theorem DRT.Condition.freeVarFinsetL_subset_varFinsetL {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (cs : List (Condition L V)) : freeVarFinsetL cs ⊆ varFinsetL cs

The list analogue of Condition.freeVarFinset_subset_varFinset.

@[simp]

theorem DRT.Condition.reuseFreeAt_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (K : DRS L V) : ReuseFreeAt X (neg K) ↔ DRS.ReuseFreeAt X K

@[simp]

theorem DRT.Condition.reuseFreeAt_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (a c : DRS L V) : ReuseFreeAt X (imp a c) ↔ DRS.ReuseFreeAt X a ∧ DRS.ReuseFreeAt (X ∪ a.referents) c

@[simp]

theorem DRT.Condition.reuseFreeAt_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (X : Finset V) (l r : DRS L V) : ReuseFreeAt X (dis l r) ↔ DRS.ReuseFreeAt X l ∧ DRS.ReuseFreeAt X r

theorem DRT.Condition.accScope_neg {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) (K : DRS L V) (x : V) : accScope s (neg K) x = DRS.accScope s K x

theorem DRT.Condition.accScope_imp {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) (a c : DRS L V) (x : V) : accScope s (imp a c) x = (DRS.accScope s a x).orElse fun (x_1 : Unit) => DRS.accScope (s ∪ a.referents) c x

theorem DRT.Condition.accScope_dis {L : FirstOrder.Language} {V : Type w} [DecidableEq V] (s : Finset V) (l r : DRS L V) (x : V) : accScope s (dis l r) x = (DRS.accScope s l x).orElse fun (x_1 : Unit) => DRS.accScope s r x

Accessibility as the smallest preorder

Following [GBM24] §4.2, accessibility is the smallest preorder on the sub-DRSs of a host such that a box is accessible to the sub-boxes of its complex conditions and a conditional's antecedent is accessible to its consequent. Each generating edge anchors its containing box below the host, which keeps the relation non-vacuous. DRS.Accessible.exists_mem_accessibleDomain shows every verdict of the computed accScope is realized by genuine edges.

inductive DRT.AccessibleEdge {L : FirstOrder.Language} {V : Type w} (host : DRS L V) : DRS L V → DRS L V → Prop

A generating edge of the accessibility preorder over the sub-DRSs of host (§4.2): a box is accessible to the sub-boxes of its complex conditions, and the antecedent of a conditional is accessible to its consequent.

• neg {L : FirstOrder.Language} {V : Type w} {host K K' : DRS L V} : WeakSubordinate K host → Condition.neg K' ∈ K.conditions → AccessibleEdge host K K'

  A box is accessible to the body of its ¬-conditions.

• impAnte {L : FirstOrder.Language} {V : Type w} {host K K' K'' : DRS L V} : WeakSubordinate K host → Condition.imp K' K'' ∈ K.conditions → AccessibleEdge host K K'

  A box is accessible to the antecedents of its ⇒-conditions.

• impCons {L : FirstOrder.Language} {V : Type w} {host K K' K'' : DRS L V} : WeakSubordinate K host → Condition.imp K' K'' ∈ K.conditions → AccessibleEdge host K' K''

  The antecedent of a ⇒-condition is accessible to its consequent.

• disLeft {L : FirstOrder.Language} {V : Type w} {host K K' K'' : DRS L V} : WeakSubordinate K host → Condition.dis K' K'' ∈ K.conditions → AccessibleEdge host K K'

  A box is accessible to the left disjunct of its ∨-conditions.

• disRight {L : FirstOrder.Language} {V : Type w} {host K K' K'' : DRS L V} : WeakSubordinate K host → Condition.dis K' K'' ∈ K.conditions → AccessibleEdge host K K''

  A box is accessible to the right disjunct of its ∨-conditions.

@[reducible, inline]

abbrev DRT.AccessibleTo {L : FirstOrder.Language} {V : Type w} (host : DRS L V) : DRS L V → DRS L V → Prop

AccessibleTo host K K' says K is accessible to K' among the sub-DRSs of host — the smallest preorder containing the generating edges (§4.2).

Equations

• DRT.AccessibleTo host = Relation.ReflTransGen (DRT.AccessibleEdge host)

theorem DRT.AccessibleEdge.weakSubordinate_right {L : FirstOrder.Language} {V : Type w} {host K K' : DRS L V} (h : AccessibleEdge host K K') : WeakSubordinate K' host

The target of an accessibility edge is a sub-DRS of the host.

def DRT.accessibleDomain {L : FirstOrder.Language} {V : Type w} (host K : DRS L V) : Set V

The accessible domain A_K of K in host — the set of referents declared in some box accessible to K (§4.2).

Equations

• DRT.accessibleDomain host K = {x : V | ∃ (K' : DRT.DRS L V), DRT.AccessibleTo host K' K ∧ x ∈ K'.referents}

theorem DRT.referents_subset_accessibleDomain {L : FirstOrder.Language} {V : Type w} (host K : DRS L V) : ↑K.referents ⊆ accessibleDomain host K

theorem DRT.accessibleDomain_mono {L : FirstOrder.Language} {V : Type w} {host K K' : DRS L V} (h : AccessibleTo host K K') : accessibleDomain host K ⊆ accessibleDomain host K'

Soundness of the computed accessibility

theorem DRT.DRS.Accessible.exists_mem_accessibleDomain {L : FirstOrder.Language} {V : Type w} [DecidableEq V] {T : DRS L V} {u v : V} (h : T.Accessible u v) : ∃ (K : DRS L V), WeakSubordinate K T ∧ u ∈ K.referents ∧ v ∈ accessibleDomain T K

Every computed accessibility verdict is realized by genuine §4.2 edges: if v ∈ accessibleFrom T u, then u is declared in a sub-DRS K of T and v lies in K's accessible domain. The converse choice among multiple declaration sites of u is algorithmic (first hit); its characterization is future work.