File Change Semantics

[Hei82] [Hei83]

[Hei82]'s file change potentials over referential information states: FCP W V M is CCP.Partial at the possibility type — the partiality effect of Dynamic/Partial.lean over the root states of Dynamic/State.lean. A file is an information state: its cards are the familiar referents, Dom(F) the shared domain of a uniform file. Presupposition is Part-definedness (CCP.Partial.admits, Heim's "F admits φ"), so the Novelty and Familiarity Conditions are genuine definedness conditions; sequencing and its monoid laws are PFun.comp's (PFun.comp_assoc, PFun.id_comp, PFun.comp_id).

The assertive update is consistent merge (the State monoid's *, [KvGR11] Def. 26): [Hei83]'s revised atomic rule (18), which filters where the input already defines the atom's cards (rule (13), atomVar_eq_of_familiar) and extends where it does not (atomVar_eq_of_novel) — per point, so atoms are total and appropriateness ((15)) lives on indef/def_, as in the paper. Principle (A) in its general form is ascent in informativeness (le_ofState); set-shrinking eliminativity is its familiar face.

Negation keeps the points of F that do not subsist in the scope's update — the no-verifying-extension clause, generalizing [Hei83]'s world-only s \ s[φ] (CCP.Partial.neg): on a uniform stratum the two coincide (neg_eq_partial_neg), so the 1983 clauses are the referent-free shadow of the 1982 ones.

Main definitions

• FCP: file change potentials — CCP.Partial (Possibility W V (Part M)).
• FCP.ofState: assertive update as consistent merge; FCP.atomW, FCP.atomVar, FCP.atomVar2 are its instances at proposition states.
• FCP.neg, FCP.cond: negation as non-subsistence; if as ¬(φ ∧ ¬ψ).
• FCP.indef, FCP.def_: the Novelty and Familiarity Conditions as Part.assert guards on State.randomAssign and identity.
• FCP.trueIn, FCP.falseIn, FCP.supports, FCP.fcpEntails: truth criterion (C) (Ch. III §3.2) and dynamic entailment.

Main results

• admits_def_, admits_indef: the Familiarity and Novelty Conditions are exactly definedness.
• le_ofState: Principle (A) — updates only add information.
• atomW_eq, atomVar_eq_of_familiar, atomVar_eq_of_novel: the filtering and extending regimes of the merge-based atom (rules (13) and (18)).
• neg_eq_partial_neg: on a uniform stratum, non-subsistence negation is [Hei83]'s set-difference negation.

@[reducible, inline]

abbrev DynamicSemantics.FCP (W : Type u_1) (V : Type u_2) (M : Type u_3) : Type (max (max u_3 u_2) u_1)

A file change potential ([Hei82], Ch. III): a partial update of referential information states — CCP.Partial at the possibility type. Partiality is presupposition (CCP.Partial.admits); Heim's files number their cards, V := ℕ.

Equations

• DynamicSemantics.FCP W V M = DynamicSemantics.CCP.Partial (DynamicSemantics.Possibility W V (Part M))

def DynamicSemantics.FCP.refersTo {W : Type u_1} {V : Type u_2} {M : Type u_3} (F : State W V M) (x : V) (m : M) : Prop

Card x in F refers to m: every point assigns m to x (Ch. III §2.3).

Equations

• DynamicSemantics.FCP.refersTo F x m = ∀ p ∈ F, m ∈ p.assignment x

def DynamicSemantics.FCP.ofState {W : Type u_1} {V : Type u_2} {M : Type u_3} (A : State W V M) : FCP W V M

Assertive update by a state: consistent merge ([Hei83]'s revised atomic rule (18), which is [KvGR11] Def. 26's consistent merge, the State monoid's *) — each input point pairs with every compatible point of A, filtering where their domains overlap and extending where A defines more. Total: appropriateness ((15), the Novelty/Familiarity Condition) lives on indef/def_, as in the paper.

Equations

• DynamicSemantics.FCP.ofState A F = Part.some (F.lubs A)

theorem DynamicSemantics.FCP.le_ofState {W : Type u_1} {V : Type u_2} {M : Type u_3} (A : State W V M) {F F' : State W V M} (h : F' ∈ ofState A F) : F ≤ F'

Principle (A), general form: assertive update ascends in informativeness — State.left_le_mul. Set-shrinking eliminativity is its familiar-regime shadow (atomVar_eq_of_familiar); on novel referents the update extends rather than shrinks.

def DynamicSemantics.FCP.atomW {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : W → Prop) : FCP W V M

Atomic predicate on the world: merge with the empty-domain proposition state.

Equations

• DynamicSemantics.FCP.atomW pred = DynamicSemantics.FCP.ofState {q : DynamicSemantics.Possibility W V (Part M) | q.domain = ∅ ∧ pred q.world}

def DynamicSemantics.FCP.atomVar {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : M → Prop) (x : V) : FCP W V M

Atomic predicate at card x: merge with the {x}-domain proposition state. Familiar x filters (rule (13)); novel x extends (rule (18)) — per point, so partially familiar files update pointwise.

Equations

• DynamicSemantics.FCP.atomVar pred x = DynamicSemantics.FCP.ofState {q : DynamicSemantics.Possibility W V (Part M) | q.domain = {x} ∧ ∃ m ∈ q.assignment x, pred m}

def DynamicSemantics.FCP.atomVar2 {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : M → M → Prop) (x y : V) : FCP W V M

Binary atomic predicate at x and y.

Equations

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

def DynamicSemantics.FCP.neg {W : Type u_1} {V : Type u_2} {M : Type u_3} (φ : FCP W V M) : FCP W V M

Negation: keep the points of F that do not subsist in the scope's update — the no-verifying-extension clause, as non-subsistence. Referents introduced inside the scope are trapped. Undefined when the scope is.

Equations

• φ.neg F = Part.map (fun (F' : Set (DynamicSemantics.Possibility W V (Part M))) => {p : DynamicSemantics.Possibility W V (Part M) | p ∈ F ∧ p ∉ lowerClosure F'}) (φ F)

def DynamicSemantics.FCP.cond {W : Type u_1} {V : Type u_2} {M : Type u_3} (φ ψ : FCP W V M) : FCP W V M

Conditional: F + [if φ then ψ] = F + [¬(φ ∧ ¬ψ)] — Heim's analysis of conditionals as negated conjunctions.

Equations

• φ.cond ψ = DynamicSemantics.FCP.neg (DynamicSemantics.CCP.Partial.seq φ ψ.neg)

def DynamicSemantics.FCP.indef {W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] (x : V) (body : FCP W V M) : FCP W V M

Indefinite introduction: defined only if x is novel (the Novelty Condition — no point defines it); then introduce x by random assignment and update with the body. Indefinites don't quantify — they open a new file card. [Hei91] later derives novelty from Maximize Presupposition rather than stipulating it; the guard here is the original (15).

Equations

• DynamicSemantics.FCP.indef x body F = Part.assert (∀ p ∈ F, ¬(p.assignment x).Dom) fun (x_1 : ∀ p ∈ F, ¬(p.assignment x).Dom) => body (DynamicSemantics.State.randomAssign F x)

def DynamicSemantics.FCP.def_ {W : Type u_1} {V : Type u_2} {M : Type u_3} (x : V) (body : FCP W V M) : FCP W V M

Definite reference: defined only if x is familiar (the Familiarity Condition); the card is already established, so the file passes through to the body.

Equations

• DynamicSemantics.FCP.def_ x body F = Part.assert (DynamicSemantics.State.Familiar F x) fun (x : DynamicSemantics.State.Familiar F x) => body F

Truth and entailment (Ch. III §3)

def DynamicSemantics.FCP.trueIn {W : Type u_1} {V : Type u_2} {M : Type u_3} (F : State W V M) (φ : FCP W V M) : Prop

Truth criterion (C) (Ch. III §3.2): φ is true w.r.t. F iff F + φ is defined and consistent. Existential quantification is built into truth itself — indefinites need no existential closure.

Equations

• DynamicSemantics.FCP.trueIn F φ = ∃ F' ∈ φ F, F'.Nonempty

def DynamicSemantics.FCP.falseIn {W : Type u_1} {V : Type u_2} {M : Type u_3} (F : State W V M) (φ : FCP W V M) : Prop

φ is false w.r.t. F iff F + φ is defined but absurd.

Equations

• DynamicSemantics.FCP.falseIn F φ = ∃ F' ∈ φ F, ¬F'.Nonempty

def DynamicSemantics.FCP.supports {W : Type u_1} {V : Type u_2} {M : Type u_3} (F : State W V M) (φ : FCP W V M) : Prop

F supports φ iff updating changes nothing — the dynamic notion of entailment, stronger than trueIn.

Equations

• DynamicSemantics.FCP.supports F φ = (φ F = Part.some F)

def DynamicSemantics.FCP.fcpEntails {W : Type u_1} {V : Type u_2} {M : Type u_3} (φ ψ : FCP W V M) : Prop

φ semantically entails ψ iff every defined update with φ supports ψ.

Equations

• φ.fcpEntails ψ = ∀ (F : DynamicSemantics.State W V M), ∀ F' ∈ φ F, DynamicSemantics.FCP.supports F' ψ

theorem DynamicSemantics.FCP.trueIn_admits {W : Type u_1} {V : Type u_2} {M : Type u_3} {F : State W V M} {φ : FCP W V M} (h : trueIn F φ) : CCP.Partial.admits φ F

Truth implies definedness.

theorem DynamicSemantics.FCP.supports_trueIn {W : Type u_1} {V : Type u_2} {M : Type u_3} {F : State W V M} {φ : FCP W V M} (hsup : supports F φ) (hcons : Set.Nonempty F) : trueIn F φ

Support implies truth for consistent files.

theorem DynamicSemantics.FCP.supports_idempotent {W : Type u_1} {V : Type u_2} {M : Type u_3} {F : State W V M} {φ : FCP W V M} (h : supports F φ) : CCP.Partial.seq φ φ F = φ F

Support is idempotent: if F supports φ, updating twice is the same as once.

Admittance

theorem DynamicSemantics.FCP.admits_indef {W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] (x : V) (body : FCP W V M) (F : State W V M) : CCP.Partial.admits (indef x body) F ↔ ∃ (_ : ∀ p ∈ F, ¬(p.assignment x).Dom), (body (F.randomAssign x)).Dom

The Novelty Condition is definedness: an indefinite is defined iff its card is novel and the body is defined on the extended file.

theorem DynamicSemantics.FCP.admits_def_ {W : Type u_1} {V : Type u_2} {M : Type u_3} (x : V) (body : FCP W V M) (F : State W V M) : CCP.Partial.admits (def_ x body) F ↔ ∃ (_ : F.Familiar x), (body F).Dom

The Familiarity Condition is definedness ((15)): a definite is defined iff its card is familiar (and the body is defined).

The two regimes: filtering and extension

The merge-based atom has rule (13) as its familiar face and rule (18)'s domain extension as its novel face, per point; ⊆-eliminativity holds exactly on the familiar face, while Principle (A) in general is le_ofState.

theorem DynamicSemantics.FCP.atomW_eq {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : W → Prop) (F : State W V M) : atomW pred F = Part.some {p : Possibility W V (Part M) | p ∈ F ∧ pred p.world}

World atoms filter, unconditionally: merging with an empty-domain proposition state eliminates the points at incompatible worlds.

theorem DynamicSemantics.FCP.atomVar_eq_of_familiar {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : M → Prop) (x : V) {F : State W V M} (hfam : F.Familiar x) : atomVar pred x F = Part.some {p : Possibility W V (Part M) | p ∈ F ∧ ∃ m ∈ p.assignment x, pred m}

Rule (13), the familiar regime: at a familiar card the atom filters — and in particular is eliminative.

theorem DynamicSemantics.FCP.atomVar_eq_of_novel {W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] (pred : M → Prop) (x : V) {F : State W V M} (hnov : ∀ p ∈ F, ¬(p.assignment x).Dom) : atomVar pred x F = Part.some {p : Possibility W V (Part M) | p ∈ F.randomAssign x ∧ ∃ m ∈ p.assignment x, pred m}

Rule (18), the novel regime: at a novel card the atom extends each point with every witness — random assignment then filtering, in one step. The indefinite needs no extra content clause; indef adds only the Novelty guard.

theorem DynamicSemantics.FCP.atomW_eliminative {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : W → Prop) {F F' : State W V M} (h : F' ∈ atomW pred F) : F' ⊆ F

World atoms are eliminative (the familiar face of Principle (A)).

theorem DynamicSemantics.FCP.atomVar_eliminative {W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : M → Prop) (x : V) {F F' : State W V M} (hfam : F.Familiar x) (h : F' ∈ atomVar pred x F) : F' ⊆ F

Variable atoms are eliminative at familiar cards.

theorem DynamicSemantics.FCP.neg_eliminative {W : Type u_1} {V : Type u_2} {M : Type u_3} (φ : FCP W V M) {F F' : State W V M} (h : F' ∈ φ.neg F) : F' ⊆ F

Negation is eliminative.

The referent-free shadow

theorem DynamicSemantics.FCP.neg_eq_partial_neg {W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] {X : Finset V} {φ : FCP W V M} {F : State W V M} (hF : State.UniformAt (↑X) F) (hφ : ∀ F' ∈ φ F, State.UniformAt (↑X) F') : φ.neg F = CCP.Partial.neg φ F

On a uniform stratum, non-subsistence negation is [Hei83]'s set-difference negation (CCP.Partial.neg): with every referent shared, a point subsists in the update exactly when it survives into it. The 1983 clauses are the referent-free shadow of the 1982 ones.