File change semantics

import Linglib.Semantics.Dynamic.FileChange

This file defines file change potentials, the meanings of sentences in Heim's file change semantics. A file records what a discourse has established so far: it keeps a card for each individual that has been mentioned, and a sequence of individuals satisfies the file when, read card by card, it fits every entry. Uttering a sentence changes the file. It filters out the sequences the sentence rules out and opens a card for each individual the sentence introduces, and the meaning of the sentence is the function from files to files that its utterance brings about.

A file is an information state (State) whose points are the sequences and whose established cards are the referents every point defines. The dissertation's files, which distinguish only finitely many cards, are the states uniform at a set of cards. A file change potential is a partial function on states. It is undefined at a file that fails the sentence's felicity conditions, so presupposition is definedness: the Novelty Condition on an indefinite requires its card to be new to the file, and the Familiarity Condition on a definite requires the card to be present. Sequencing is composition of partial functions.

The assertive update by an atomic sentence merges the file with the sentence's proposition state. At the cards the file already has the merge filters the sequences, and at new cards it extends each sequence by every value, which is Heim's atomic rule read point by point. Every update only adds information, so it is eliminative in the informativeness order, Heim's Principle (A) as PartialUpdate.IsEliminative, and a card, once established, is never lost. Negation keeps the sequences that no extension carries into the scope's update, which traps the referents introduced inside the scope. On a uniform file negation is set difference, as in the later propositional presentation of the theory.

Main definitions

FCP: file change potentials, partial updates of information states.
FCP.ofState: the assertive update by a state, merging the file with it.
FCP.atomVar: the update by an atomic predicate at a card.
FCP.atomW: the update by an atomic predicate on the world alone.
FCP.neg, FCP.cond: negation as non-subsistence, and the conditional as ¬(φ ∧ ¬ψ).
FCP.indef: the indefinite, guarded by the Novelty Condition.
FCP.def_: the definite, guarded by the Familiarity Condition and its descriptive content.
FCP.trueIn: consistency of the updated file, the truth clause of Heim's criterion (C) for files without worlds.

Main results

FCP.ofState_mul: updating by two states in sequence is updating by their merge.
FCP.semiconj_ofState: up to informational equivalence, assertion is additive.
FCP.atomVar_eq: the atom extends the file along its card and filters by its predicate.
FCP.atomVar_eq_of_familiar, FCP.atomVar_eq_of_novel: at an established card the atom filters, and at a new card it is random assignment followed by filtering.
FCP.admits_indef, FCP.admits_def_: the felicity conditions are definedness.
FCP.isEliminative_ofState, FCP.isEliminative_neg, PartialUpdate.IsEliminative.indef: every clause only adds information.
PartialUpdate.IsEliminative.familiar: an established card stays established.
FCP.neg_eq_partial_neg: on a uniform file, negation is set difference.

References

Heim 1991, Artikel und Definitheit
Kamp et al. 2011, Discourse Representation Theory formalized

Declarations

A file change potential (Heim 1982): a partial update of referential information states. Partiality is presupposition (PartialUpdate.Admits); Heim numbers her cards, V := ℕ.

@[reducible, inline] abbrev FCP L69–72

(W : Type u_1) (V : Type u_2) (M : Type u_3) :

Type (max (max u_3 u_2) u_1)

FCP W V M = DynamicSemantics.PartialUpdate (DynamicSemantics.State W V M)

Used by FCP.ofState, FCP.atomW, FCP.atomVar, FCP.neg, FCP.cond, FCP.indef, FCP.def_, FCP.admits_neg, FCP.admits_cond, FCP.admits_indef, FCP.indef_apply, FCP.admits_def_, FCP.def_apply, FCP.subset_of_mem_neg, FCP.isEliminative_neg, FCP.isEliminative_cond, DynamicSemantics.PartialUpdate.IsEliminative.indef, FCP.isEliminative_def_, DynamicSemantics.PartialUpdate.IsEliminative.eq_empty_of_mem, DynamicSemantics.PartialUpdate.IsEliminative.familiar, FCP.trueIn, FCP.trueIn_admits, FCP.trueIn_of_supports, FCP.neg_eq_partial_neg

Used in Heim1982, Heim1983

Assertive update

Assertive update by a state: the file merges with it. Each point of the file pairs with every compatible point of A, filtering where their domains overlap and extending where A defines more. The update is total; appropriateness lives on indef and def_.

def FCP.ofState L80–84

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

FCP W V M

FCP.ofState A F = Part.some (F * A)

Built from

Used by FCP.ofState_apply, FCP.mem_ofState, FCP.ofState_one, FCP.ofState_mul, FCP.ofState_le, FCP.atomW, FCP.atomVar, FCP.isEliminative_ofState

Used in Heim1982

L86

L88

L90

Assertive update is the regular action of the merge monoid: updating by A and then by B is updating by A * B.

theorem FCP.ofState_mul L92–95

{W : Type u_1} {V : Type u_2} {M : Type u_3} {A B : DynamicSemantics.State W V M} :

ofState (A * B) = DynamicSemantics.PartialUpdate.seq (ofState A) (ofState B)

Built from

L97

Up to informational equivalence, assertion is additive in the sense of Semantics/Dynamic/Consequence.lean: on the upper sets of possibilities it meets the file with the content of A (isAdditive_inf_right). Merging need not be literally idempotent, since two compatible points of a file merge into a third, so literal fixed points of assertion are finer than informational acceptance.

theorem FCP.semiconj_ofState L99–108

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

Function.Semiconj (⇑OrderDual.toDual ∘ upperClosure) (fun (x : DynamicSemantics.State W V M) => x * A) fun (x : (UpperSet (DynamicSemantics.Possibility W V (Flat M)))ᵒᵈ) => x ⊓ OrderDual.toDual (upperClosure A)

Atoms

An atomic predicate on the world: merge with its proposition at the empty stratum.

def FCP.atomW L112–115

{W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : W → Prop) :

FCP W V M

FCP.atomW pred = FCP.ofState {q : DynamicSemantics.Possibility W V (Flat M) | q ∈ DynamicSemantics.State.stratum ∅ ∧ pred q.world}

Built from ,

Used by FCP.atomW_eq

An atomic predicate at card x: merge with its proposition state at the stratum {x}.

def FCP.atomVar L117–119

{W : Type u_1} {V : Type u_2} {M : Type u_3} (pred : M → Prop) (x : V) :

FCP W V M

FCP.atomVar pred x = FCP.ofState (DynamicSemantics.State.atomAt x fun (x : W) => pred)

Built from ,

Used by FCP.atomVar_eq, FCP.atomVar_eq_of_familiar, FCP.atomVar_eq_of_novel

Used in Heim1982

L121–128

The card atom extends the file along its card, then filters by its predicate: the satisfaction clause and the domain clause of Heim 1982's atomic rule, per point.

theorem FCP.atomVar_eq L130–136

{W : Type u_1} {V : Type u_2} {M : Type u_3} {F : DynamicSemantics.State W V M} (pred : M → Prop) (x : V) :

atomVar pred x F = Part.some {p : DynamicSemantics.Possibility W V (Flat M) | p ∈ F * DynamicSemantics.State.stratum {x} ∧ ∃ (m : M), p.assignment x = ↑m ∧ pred m}

Built from

At an established card the atom filters.

theorem FCP.atomVar_eq_of_familiar L138–141

{W : Type u_1} {V : Type u_2} {M : Type u_3} {F : DynamicSemantics.State W V M} {x : V} (pred : M → Prop) (hfam : F.Familiar x) :

atomVar pred x F = Part.some {p : DynamicSemantics.Possibility W V (Flat M) | p ∈ F ∧ ∃ (m : M), p.assignment x = ↑m ∧ pred m}

Built from

At a novel card the atom is random assignment followed by filtering, so the indefinite adds only the Novelty guard.

theorem FCP.atomVar_eq_of_novel L143–148

{W : Type u_1} {V : Type u_2} {M : Type u_3} {F : DynamicSemantics.State W V M} {x : V} [DecidableEq V] (pred : M → Prop) (hnov : F.Novel x) :

atomVar pred x F = Part.some {p : DynamicSemantics.Possibility W V (Flat M) | p ∈ F.randomAssign x ∧ ∃ (m : M), p.assignment x = ↑m ∧ pred m}

Built from

Connectives and felicity conditions

Negation keeps the points of F that do not subsist in the scope's update: no extension of the point verifies the scope, so referents introduced inside it are trapped. Undefined when the scope is.

def FCP.neg L152–156

{W : Type u_1} {V : Type u_2} {M : Type u_3} (φ : FCP W V M) :

FCP W V M

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

Built from

Used by FCP.cond, FCP.admits_neg, FCP.subset_of_mem_neg, FCP.isEliminative_neg, FCP.neg_eq_partial_neg

Used in Heim1982, Heim1983

The conditional is the negated conjunction ¬(φ ∧ ¬ψ).

def FCP.cond L158–159

{W : Type u_1} {V : Type u_2} {M : Type u_3} (φ ψ : FCP W V M) :

FCP W V M

φ.cond ψ = FCP.neg (DynamicSemantics.PartialUpdate.seq φ ψ.neg)

Built from ,

Used by FCP.admits_cond, FCP.isEliminative_cond

Used in Heim1982

An indefinite at card x: defined only if x is novel (the Novelty Condition), then random assignment at x followed by the body. Indefinites do not quantify; they open a card. Heim 1991 later derives novelty from Maximize Presupposition rather than stipulating it.

def FCP.indef L161–166

{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

FCP.indef x body F = Part.assert (F.Novel x) fun (x_1 : F.Novel x) => body (F.randomAssign x)

Built from

Used by FCP.admits_indef, FCP.indef_apply, DynamicSemantics.PartialUpdate.IsEliminative.indef

Used in Heim1982

A definite at card x with descriptive content N: defined only if x is established and the file supports its content (the Extended Novelty-Familiarity-Condition), and then changes nothing.

def FCP.def_L168–173

{W : Type u_1} {V : Type u_2} {M : Type u_3} (x : V) (N : FCP W V M) :

FCP W V M

FCP.def_ x N F = Part.assert (F.Familiar x ∧ DynamicSemantics.PartialUpdate.supports F N) fun (x : F.Familiar x ∧ DynamicSemantics.PartialUpdate.supports F N) => Part.some F

Built from

Used by FCP.admits_def_, FCP.def_apply, FCP.isEliminative_def_

Used in Heim1982

L175

L177–178

The Novelty Condition is definedness.

theorem FCP.admits_indef L180–183

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

DynamicSemantics.PartialUpdate.Admits (indef x body) F ↔ ∃ (_ : F.Novel x), (body (F.randomAssign x)).Dom

Built from ,

L185–186

The Extended Familiarity Condition is definedness.

theorem FCP.admits_def_L188–191

{W : Type u_1} {V : Type u_2} {M : Type u_3} {F : DynamicSemantics.State W V M} {x : V} (N : FCP W V M) :

DynamicSemantics.PartialUpdate.Admits (def_ x N) F ↔ F.Familiar x ∧ DynamicSemantics.PartialUpdate.supports F N

Built from ,

L193–194

L196–198

Principle (A)

Every defined update only adds information: it descends in informativeness. On a uniform stratum this is set shrinking (State.UniformAt.le_iff_subset); at a novel card an update extends rather than shrinks.

theorem FCP.isEliminative_ofState L206–207

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

DynamicSemantics.PartialUpdate.IsEliminative (ofState A)

Built from

theorem FCP.isEliminative_neg L209–210

{W : Type u_1} {V : Type u_2} {M : Type u_3} (φ : FCP W V M) :

DynamicSemantics.PartialUpdate.IsEliminative φ.neg

Built from ,

L212–213

theorem DynamicSemantics.PartialUpdate.IsEliminative.indef L215–219

{W : Type u_1} {V : Type u_2} {M : Type u_3} [DecidableEq V] {body : FCP W V M} (h : IsEliminative body) (x : V) :

IsEliminative (FCP.indef x body)

Built from ,

L221–222

L224–226

A card, once established, stays established.

theorem DynamicSemantics.PartialUpdate.IsEliminative.familiar L228–231

{W : Type u_1} {V : Type u_2} {M : Type u_3} {F F' : State W V M} {φ : FCP W V M} {x : V} (h : IsEliminative φ) (hx : F.Familiar x) (hF' : F' ∈ φ F) :

F'.Familiar x

Built from

Truth

φ is true with respect to F when F + φ is defined and consistent. This is the truth clause of the criterion (C) of Heim 1982 (Ch. III §3.2) for files without worlds, where a file is true iff its satisfaction set is nonempty. On points that carry worlds consistency is truth at some world, not at a given one, and the falsity clause of (C) is not stated. Existential quantification is built into it, so indefinites need no existential closure.

def FCP.trueIn L235–240

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

Prop

FCP.trueIn F φ = ∃ F' ∈ φ F, Set.Nonempty F'

Built from

Used by FCP.trueIn_admits, FCP.trueIn_of_supports

Used in Heim1982

L242–244

L246–248

The uniform shadow

On a uniform stratum, non-subsistence negation is Heim 1983's set-difference negation (CCP.Partial.neg): with every referent shared, a point subsists in the update exactly when it survives into it.

theorem FCP.neg_eq_partial_neg L252–263

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

φ.neg F = DynamicSemantics.CCP.Partial.neg φ F

Built from ,