Contexts for dynamic predicate logic

Visser's contexts type the relations of dynamic predicate logic by the variables they touch. A context is a triple of finite sets of variables: the inputs I a relation reads, the blocks B at which it cuts the link between the input and the output value, and the outputs O it constrains, with I and O agreeing off B. A relation has a context when it changes only the blocks and membership in it is invariant under agreement on the inputs, on the outputs, and off the blocks. Contexts compose as relations do, so every formula gets a context by recursion, whose inputs are the free variables and whose blocks are the active quantifier variables of Groenendijk and Stokhof, and the formula's interpretation has it.

Main definitions

• DPL.Context: the contexts, a monoid under composition with an information order; the contexts Context.test, Context.reset, Context.impl.
• DPL.HasContext: the relations a context types.
• DPL.Formula.context: the context of a formula.

Main results

• DPL.HasContext.mono: the information order is sound for the typing (Theorem 3.5).
• DPL.HasContext.patch, DPL.HasContext.patch_unique: the output of a typed relation over a varied input exists and is unique (Lemma 3.7).
• DPL.HasContext.comp, DPL.HasContext.impl, DPL.HasContext.neg, DPL.HasContext.disj, DPL.HasContext.dexists: the typing of the connectives (Theorems 3.8 and 3.9).
• DPL.HasContext.dependsOn_dom: truth depends only on the inputs.
• DPL.HasContext.dom_comp: a relation that blocks no input of another commutes with its truth.
• DPL.Formula.hasContext_eval: a formula's interpretation has its context (Theorem 3.13), with DPL.Formula.context_I and DPL.Formula.context_B identifying its inputs and blocks.
• DPL.Formula.IsScopeBound.mem_dom_eval_iff: on the scope-bound formulas dynamic truth is first-order satisfaction.

Implementation notes

Coherence is stored in membership form, so that Context V needs no decidable equality; the paper's I ∪ B = O ∪ B is Context.union_blocks. The patched output of Lemma 3.7 is Finset.piecewise at the blocks. The paper's language has neither disjunction nor primitive negation and universal quantification; their contexts are those the paper's definitions of them yield, tests at the inputs. The context of a formula is not always the least one its interpretation has, x ≐ x reading x and denoting the identity.

References

• [Vis98]
• [GS91a]

Contexts (Definition 3.1)

structure DPL.Context (V : Type u_3) : Type u_3

A DPL-context (Definition 3.1) has an input set I of variables the incoming assignment is read at, a block set B of variables whose input-output link is cut, and an output set O of variables the outgoing assignment is constrained at, with I and O agreeing off B (the paper's I ∪ B = O ∪ B, Context.union_blocks).

• I : Finset V

  The input set.

• B : Finset V

  The block set is the barrier between past and future.

• O : Finset V

  The output set.

• coh ⦃v : V⦄ : v ∉ self.B → (v ∈ self.I ↔ v ∈ self.O)

  Off the blocks, inputs and outputs coincide.

theorem DPL.Context.ext {V : Type u_3} {x y : Context V} (I : x.I = y.I) (B : x.B = y.B) (O : x.O = y.O) : x = y

theorem DPL.Context.ext_iff {V : Type u_3} {x y : Context V} : x = y ↔ x.I = y.I ∧ x.B = y.B ∧ x.O = y.O

@[instance_reducible]

instance DPL.Context.instOne {V : Type u_1} : One (Context V)

Equations

• DPL.Context.instOne = { one := { I := ∅, B := ∅, O := ∅, coh := ⋯ } }

@[simp]

theorem DPL.Context.I_one {V : Type u_1} : I 1 = ∅

@[simp]

theorem DPL.Context.B_one {V : Type u_1} : B 1 = ∅

@[simp]

theorem DPL.Context.O_one {V : Type u_1} : O 1 = ∅

def DPL.Context.test {V : Type u_1} (s : Finset V) : Context V

The test context at s reads and writes s and blocks nothing. Conditions live here (hasContext_test), and implication contexts are tests (Context.impl).

Equations

• DPL.Context.test s = { I := s, B := ∅, O := s, coh := ⋯ }

@[simp]

theorem DPL.Context.I_test {V : Type u_1} (s : Finset V) : (test s).I = s

@[simp]

theorem DPL.Context.B_test {V : Type u_1} (s : Finset V) : (test s).B = ∅

@[simp]

theorem DPL.Context.O_test {V : Type u_1} (s : Finset V) : (test s).O = s

def DPL.Context.reset {V : Type u_1} (x : V) : Context V

The reset context at x, Definition 3.12's c_{∃v}, reads nothing, constrains no output, and blocks x.

Equations

• DPL.Context.reset x = { I := ∅, B := {x}, O := ∅, coh := ⋯ }

@[simp]

theorem DPL.Context.I_reset {V : Type u_1} (x : V) : (reset x).I = ∅

@[simp]

theorem DPL.Context.B_reset {V : Type u_1} (x : V) : (reset x).B = {x}

@[simp]

theorem DPL.Context.O_reset {V : Type u_1} (x : V) : (reset x).O = ∅

theorem DPL.Context.coh_mem {V : Type u_1} [DecidableEq V] (c : Context V) {v : V} : v ∈ c.I ∪ c.B ↔ v ∈ c.O ∪ c.B

Coherence in the union form the clauses of the typing use.

theorem DPL.Context.union_blocks {V : Type u_1} [DecidableEq V] (c : Context V) : c.I ∪ c.B = c.O ∪ c.B

The paper's statement of coherence.

@[instance_reducible]

instance DPL.Context.instMul {V : Type u_1} [DecidableEq V] : Mul (Context V)

Contexts compose by ⟨I,B,O⟩ * ⟨I',B',O'⟩ = ⟨I ∪ (I'∖B), B ∪ B', (O∖B') ∪ O'⟩ (Definition 3.1).

Equations

• DPL.Context.instMul = { mul := fun (c d : DPL.Context V) => { I := c.I ∪ d.I \ c.B, B := c.B ∪ d.B, O := c.O \ d.B ∪ d.O, coh := ⋯ } }

@[simp]

theorem DPL.Context.I_mul {V : Type u_1} [DecidableEq V] (c d : Context V) : (c * d).I = c.I ∪ d.I \ c.B

@[simp]

theorem DPL.Context.B_mul {V : Type u_1} [DecidableEq V] (c d : Context V) : (c * d).B = c.B ∪ d.B

@[simp]

theorem DPL.Context.O_mul {V : Type u_1} [DecidableEq V] (c d : Context V) : (c * d).O = c.O \ d.B ∪ d.O

@[instance_reducible]

instance DPL.Context.instMonoid {V : Type u_1} [DecidableEq V] : Monoid (Context V)

The contexts form a monoid (Theorem 3.3).

Equations

• DPL.Context.instMonoid = { toOne := DPL.Context.instOne, toMul := DPL.Context.instMul, mul_assoc := ⋯, one_mul := ⋯, mul_one := ⋯, npow := npowRecAuto, npow_zero := ⋯, npow_succ := ⋯ }

@[instance_reducible]

instance DPL.Context.instLE {V : Type u_1} [DecidableEq V] : LE (Context V)

In the information order on contexts (Definition 3.1), more informative contexts read, write, and block more, with new blocks confined to variables the larger context both reads and writes.

Equations

• DPL.Context.instLE = { le := fun (c d : DPL.Context V) => c.I ⊆ d.I ∧ c.O ⊆ d.O ∧ c.B ⊆ d.B ∧ d.B ⊆ c.B ∪ d.I ∩ d.O }

theorem DPL.Context.le_def {V : Type u_1} [DecidableEq V] {c d : Context V} : c ≤ d ↔ c.I ⊆ d.I ∧ c.O ⊆ d.O ∧ c.B ⊆ d.B ∧ d.B ⊆ c.B ∪ d.I ∩ d.O

@[instance_reducible]

instance DPL.Context.instDecidableLE {V : Type u_1} [DecidableEq V] : DecidableLE (Context V)

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff' (x✝¹.I ⊆ x✝.I ∧ x✝¹.O ⊆ x✝.O ∧ x✝¹.B ⊆ x✝.B ∧ x✝.B ⊆ x✝¹.B ∪ x✝.I ∩ x✝.O) ⋯

@[instance_reducible]

instance DPL.Context.instPartialOrder {V : Type u_1} [DecidableEq V] : PartialOrder (Context V)

The information order is a partial order (Theorem 3.3).

Equations

• DPL.Context.instPartialOrder = { le := fun (x1 x2 : DPL.Context V) => x1 ≤ x2, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

def DPL.Context.impl {V : Type u_1} [DecidableEq V] (c d : Context V) : Context V

The implication context (Definition 3.1) is a test reading the combined inputs.

Equations

• c.impl d = DPL.Context.test (c * d).I

@[simp]

theorem DPL.Context.I_impl {V : Type u_1} [DecidableEq V] (c d : Context V) : (c.impl d).I = c.I ∪ d.I \ c.B

@[simp]

theorem DPL.Context.B_impl {V : Type u_1} [DecidableEq V] (c d : Context V) : (c.impl d).B = ∅

@[simp]

theorem DPL.Context.O_impl {V : Type u_1} [DecidableEq V] (c d : Context V) : (c.impl d).O = c.I ∪ d.I \ c.B

c-relations (Definition 3.4)

structure DPL.HasContext {V : Type u_1} {E : Type u_2} (R : DynamicSemantics.Update (V → E)) (c : Context V) : Prop

A context c is a context for R (Definition 3.4) if R reads its input only at c.I, constrains its output only at c.O, and changes values only at c.B.

• blocks ⦃f g : V → E⦄ : (f, g) ∈ R → Set.EqOn f g (↑c.B)ᶜ

  Only blocked variables change.

• stable ⦃f f' g g' : V → E⦄ : (f, g) ∈ R → Set.EqOn f' f ↑c.I → Set.EqOn g g' ↑c.O → Set.EqOn f' g' (↑c.B)ᶜ → (f', g') ∈ R

  Membership is invariant under input agreement on I, output agreement on O, and preservation off B.

theorem DPL.hasContext_test_iff {V : Type u_1} {E : Type u_2} {s : Finset V} {R : DynamicSemantics.Update (V → E)} : HasContext R (Context.test s) ↔ R.IsTest ∧ ∀ ⦃f f' : V → E⦄, Set.EqOn f' f ↑s → (f, f) ∈ R → (f', f') ∈ R

The test V-typed relations are exactly the V-invariant tests — Definition 2.2's ⟨V⟩-conditions (noted after Definition 3.4).

theorem DPL.hasContext_test {V : Type u_1} {E : Type u_2} (s : Finset V) (p : Set (V → E)) (hp : ∀ ⦃f f' : V → E⦄, Set.EqOn f f' ↑s → f ∈ p → f' ∈ p) : HasContext (DynamicSemantics.Update.test p) (Context.test s)

A condition depending only on V is a Context.test V-relation as a test (the atomic case of the paper's semantic Theorem 3.13).

theorem DPL.hasContext_test_of_dependsOn {V : Type u_1} {E : Type u_2} {s : Finset V} {p : Set (V → E)} (hp : DependsOn (fun (x : V → E) => x ∈ p) ↑s) : HasContext (DynamicSemantics.Update.test p) (Context.test s)

A condition that depends only on s is typed as a test at s.

theorem DPL.hasContext_id {V : Type u_1} {E : Type u_2} : HasContext SetRel.id 1

The identity is typed by the unit context.

The order is sound for the typing (Theorem 3.5)

theorem DPL.HasContext.mono {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R : DynamicSemantics.Update (V → E)} (h : HasContext R c) (hcd : c ≤ d) : HasContext R d

Larger contexts type more relations (Theorem 3.5(1)), so if c ≤ d and R is a c-relation, then R is a d-relation.

The unique-output lemma (Lemma 3.7)

theorem DPL.HasContext.patch_eqOn {V : Type u_1} {E : Type u_2} [DecidableEq V] {c : Context V} {R : DynamicSemantics.Update (V → E)} {f f' g : V → E} {J : Set V} (h : HasContext R c) (hR : (f, g) ∈ R) (hJ : Set.EqOn f' f J) : Set.EqOn (c.B.piecewise g f') g (J ∪ ↑c.B)

The patch agrees with g at the blocks and wherever the inputs agree (Lemma 3.7, transfer).

theorem DPL.HasContext.patch {V : Type u_1} {E : Type u_2} [DecidableEq V] {c : Context V} {R : DynamicSemantics.Update (V → E)} {f f' g : V → E} (h : HasContext R c) (hI : Set.EqOn f' f ↑c.I) (hR : (f, g) ∈ R) : (f', c.B.piecewise g f') ∈ R

If f' agrees with f on the inputs and f R g, then R relates f' to the patch of f' by g at the blocks (Lemma 3.7, existence).

theorem DPL.HasContext.patch_unique {V : Type u_1} {E : Type u_2} [DecidableEq V] {c : Context V} {R : DynamicSemantics.Update (V → E)} {f' g g' : V → E} (h : HasContext R c) (hR : (f', g') ∈ R) (hB : Set.EqOn g' g ↑c.B) : g' = c.B.piecewise g f'

The patch is the only output over f' agreeing with g on the blocks (Lemma 3.7, uniqueness).

Composition and implication typing (Theorems 3.8–3.9)

theorem DPL.HasContext.comp {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R S : DynamicSemantics.Update (V → E)} (hR : HasContext R c) (hS : HasContext S d) : HasContext (SetRel.comp R S) (c * d)

The composition of a c-relation and a d-relation is a c * d-relation (Theorem 3.8).

theorem DPL.HasContext.impl {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R S : DynamicSemantics.Update (V → E)} (hR : HasContext R c) (hS : HasContext S d) : HasContext (DynamicSemantics.Update.test (R.impl S)) (c.impl d)

The DPL implication of a c-relation and a d-relation is a (c → d)-relation (Theorem 3.9).

The DPL generators, typed

theorem DPL.hasContext_randomAssign {V : Type u_1} {E : Type u_2} [DecidableEq V] (x : V) : HasContext (DynamicSemantics.Update.randomAssign x) (Context.reset x)

The reset is typed at ⟨∅, {x}, ∅⟩, Definition 3.12's c_{∃v}, which reads nothing, constrains no output, and blocks x.

theorem DPL.HasContext.dexists {V : Type u_1} {E : Type u_2} [DecidableEq V] {c : Context V} {φ : DynamicSemantics.Update (V → E)} (x : V) (h : HasContext φ c) : HasContext (DynamicSemantics.Update.dexists x φ) (Context.reset x * c)

Blocking x before a c-relation types ∃x φ (Definition 3.12's c_{∃v} • c_φ).

Truth depends on the inputs

theorem DPL.HasContext.dependsOn_dom {V : Type u_1} {E : Type u_2} [DecidableEq V] {c : Context V} {R : DynamicSemantics.Update (V → E)} (h : HasContext R c) : DependsOn (fun (x : V → E) => x ∈ SetRel.dom R) ↑c.I

The domain of a c-relation depends only on the inputs (noted after Lemma 3.7).

theorem DPL.HasContext.mem_dom_iff {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R S : DynamicSemantics.Update (V → E)} {f g : V → E} (hR : HasContext R c) (hS : HasContext S d) (hd : Disjoint c.B d.I) (hfg : (f, g) ∈ R) : f ∈ SetRel.dom S ↔ g ∈ SetRel.dom S

A relation that blocks none of the inputs of another preserves the other's truth.

theorem DPL.HasContext.dom_comp {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R S : DynamicSemantics.Update (V → E)} (hR : HasContext R c) (hS : HasContext S d) (hd : Disjoint c.B d.I) : (SetRel.comp R S).dom = SetRel.dom R ∩ SetRel.dom S

A relation that blocks none of the inputs of another commutes with its truth, so the sequence is true where both are.

theorem DPL.HasContext.impl_eq {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R S : DynamicSemantics.Update (V → E)} (hR : HasContext R c) (hS : HasContext S d) (hd : Disjoint c.B d.I) : R.impl S = (SetRel.dom R)ᶜ ∪ SetRel.dom S

An implication from a relation that blocks no input of the consequent is material.

theorem DPL.HasContext.neg {V : Type u_1} {E : Type u_2} [DecidableEq V] {c : Context V} {R : DynamicSemantics.Update (V → E)} (h : HasContext R c) : HasContext (DynamicSemantics.Update.test R.neg) (Context.test c.I)

The negation of a c-relation is a test at its inputs.

theorem DPL.HasContext.disj {V : Type u_1} {E : Type u_2} [DecidableEq V] {c d : Context V} {R S : DynamicSemantics.Update (V → E)} (hR : HasContext R c) (hS : HasContext S d) : HasContext (DynamicSemantics.Update.test (R.disj S)) (Context.test (c.I ∪ d.I))

The disjunction of a c-relation and a d-relation is a test at their inputs.

The context of a formula (Definition 3.12, Theorem 3.13)

def DPL.Formula.context {V : Type u_1} [DecidableEq V] {L : FirstOrder.Language} : Formula L V → Context V

The context of a formula (Definition 3.12). The paper's language has no disjunction and defines negation and the universal; they are typed here as the definitions would be.

Equations

• DPL.Formula.top.context = 1
• (DPL.Formula.rel R ts).context = DPL.Context.test (DPL.Formula.rel R ts).fv
• (DPL.Formula.equal t₁ t₂).context = DPL.Context.test (DPL.Formula.equal t₁ t₂).fv
• φ.neg.context = DPL.Context.test φ.context.I
• (φ.conj ψ).context = φ.context * ψ.context
• (φ.disj ψ).context = DPL.Context.test (φ.context.I ∪ ψ.context.I)
• (φ.imp ψ).context = φ.context.impl ψ.context
• (DPL.Formula.ex x_1 φ).context = DPL.Context.reset x_1 * φ.context
• (DPL.Formula.all x_1 φ).context = (DPL.Context.reset x_1).impl φ.context

theorem DPL.Formula.context_B {V : Type u_1} [DecidableEq V] {L : FirstOrder.Language} (φ : Formula L V) : φ.context.B = φ.aqv

The blocks of a formula's context are its active quantifier variables.

theorem DPL.Formula.context_I {V : Type u_1} [DecidableEq V] {L : FirstOrder.Language} (φ : Formula L V) : φ.context.I = φ.fv

The inputs of a formula's context are its free variables.

theorem DPL.Formula.hasContext_eval {V : Type u_1} [DecidableEq V] {L : FirstOrder.Language} (M : Type u_3) [L.Structure M] (φ : Formula L V) : HasContext (eval M φ) φ.context

The interpretation of a formula is typed by its context (Theorem 3.13).

theorem DPL.Formula.IsScopeBound.mem_dom_eval_iff {V : Type u_1} [DecidableEq V] {L : FirstOrder.Language} (M : Type u_3) [L.Structure M] {φ : Formula L V} (h : φ.IsScopeBound) {g : V → M} : g ∈ SetRel.dom (eval M φ) ↔ φ.toFormula.Realize g

A scope-bound formula is true under the dynamic interpretation exactly where it is satisfied as a first-order formula ([GS91a]'s Fact 19).