Heim (1983): On the Projection Problem for Presuppositions

This file formalizes Heim's paper. A context admits a sentence when the sentence's context change potential is defined on it, a sentence presupposes what every admitting context entails (12), and the heritage properties that Karttunen and Peters stipulate for if and not are read off the potentials (14) and (15): a context admits "If A, B" iff it admits A and its update by A admits B, and negation is a hole. The King example (1)–(3) is worked as the paper does (king_admits_iff), and the two ways of accommodating a presupposition under negation are (16)'s global and local readings (globalNeg_entails, localNeg_entails); a preference for the global one recaptures Gazdar's cancellation under the threat of inconsistency (cancellation_only_under_inconsistency). Contexts as sets of sequence–world pairs (§3) carry the potentials for open sentences and for every (21): under the novelty stipulation (22), "Every nation cherishes its king" presupposes that every nation has a king (every_nation_presupposes), a presupposition in the restrictor projects universally (23), and an indefinite's presupposition projects universally unless it is accommodated in the course of the update (§3.3).

Implementation notes

The propositional part (§2) uses the substrate's partial context change potentials over a type of worlds: ofTrivalent for a sentence with a trivalent meaning, cond for (14), neg for (15), and Admits for definedness, so that the heritage properties are the substrate's admits_cond and admits_neg. Presupposing a proposition p (12) is the substrate's Presupposes of the update ofTrivalent fun w ↦ ofProp (p w) (presupposes_ofProp_iff). The file part (§3) uses the same potentials over pairs of a sequence ℕ → M and a world, with atom, atomP, and every stated here as (19)–(21) and entailment by a context read as inclusion. The paper gives no potential for no (24), so that sentence is a row only.

A file whose membership depends only on the cards in X is, restricted to those cards, a state of the substrate uniform at X (File.toState), and on such files the paper's clauses are the file change potentials of Heim's dissertation read on that stratum: the atom is the merge with the atom's proposition state (toState_atom), negation by set difference is non-subsistence (neg_toState), and (21) is rule (III) of the dissertation (toState_everyClause). The novelty stipulation (22) is the file's independence of the card (novelIn_iff_determinedBy).

References

• [Hei83]
• [Hei82a]
• [Kar73]
• [Kar74a]
• [KP79]
• [Gaz79]
• [Lew79c]

Admittance and presupposition (§2.1–§2.2)

def Heim1983.TrueWrt {W : Type u_1} (φ : DynamicSemantics.CCP.Partial W) (c : Set W) (w : W) : Prop

S is true in w with respect to c (13) iff c admits S and the context c updated by S is true in w.

Equations

• Heim1983.TrueWrt φ c w = ∃ (h : DynamicSemantics.PartialUpdate.Admits φ c), w ∈ (φ c).get h

theorem Heim1983.trueWrt_ofTrivalent {W : Type u_1} {p : W → SignType} {c : Set W} {w : W} (hw : w ∈ c) (h : DynamicSemantics.PartialUpdate.Admits (DynamicSemantics.CCP.Partial.ofTrivalent p) c) : TrueWrt (DynamicSemantics.CCP.Partial.ofTrivalent p) c w ↔ p w = 1

The content property is derivable from the potential. With respect to a context that is true in w and admits it, an atomic sentence is true in w iff it is true there.

noncomputable def Heim1983.kingHasSon {W : Type u_1} (king son : W → Prop) : W → SignType

The king has a son (1) presupposes a king and asserts that he has a son.

Equations

• Heim1983.kingHasSon king son = {w : W | king w}.indicator fun (w : W) => SignType.ofProp (son w)

noncomputable def Heim1983.kingsSonBald {W : Type u_1} (king son bald : W → Prop) : W → SignType

The king's son is bald (2) presupposes a king with a son.

Equations

• Heim1983.kingsSonBald king son bald = {w : W | king w ∧ son w}.indicator fun (w : W) => SignType.ofProp (bald w)

noncomputable def Heim1983.ifKingHasSon {W : Type u_1} (king son bald : W → Prop) : DynamicSemantics.CCP.Partial W

(3) "If the king has a son, the king's son is bald", by (14).

Equations

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

theorem Heim1983.king_admits_iff {W : Type u_1} {king son bald : W → Prop} (c : Set W) : DynamicSemantics.PartialUpdate.Admits (ifKingHasSon king son bald) c ↔ ∀ w ∈ c, king w

A context admits (3) iff it entails that there is a king (§2.1), since it must admit (1), and its update by (1) then admits (2) automatically.

theorem Heim1983.king_presupposes {W : Type u_1} {king son bald : W → Prop} : DynamicSemantics.PartialUpdate.Presupposes (ifKingHasSon king son bald) (DynamicSemantics.CCP.Partial.ofTrivalent fun (w : W) => SignType.ofProp (king w))

(3) presupposes that there is a king, which (1) presupposes in its antecedent.

theorem Heim1983.not_presupposes_son {W : Type u_1} {king son bald : W → Prop} (h : ∃ (w : W), king w ∧ ¬son w) : ¬DynamicSemantics.PartialUpdate.Presupposes (ifKingHasSon king son bald) (DynamicSemantics.CCP.Partial.ofTrivalent fun (w : W) => SignType.ofProp (son w))

(3) does not presuppose that the king has a son, as soon as some world has a sonless king.

Accommodation (§2.3)

def Heim1983.globalNeg {W : Type u_1} (φ : DynamicSemantics.CCP.Partial W) (p : Set W) : DynamicSemantics.CCP.Partial W

The global option (A) evaluates Not S in a context that does not admit S by amending the context to c ∩ p and computing (c ∩ p) + Not S.

Equations

• Heim1983.globalNeg φ p c = φ.neg (c ∩ p)

def Heim1983.localNeg {W : Type u_1} (φ : DynamicSemantics.CCP.Partial W) (p : Set W) : DynamicSemantics.CCP.Partial W

The local option (B) amends the context to c ∩ p only to compute (c ∩ p) + S, and subtracts that from c itself.

Equations

• Heim1983.localNeg φ p c = Part.map (fun (x : Set W) => c \ x) (φ (c ∩ p))

theorem Heim1983.globalNeg_admits {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c : Set W} (h : DynamicSemantics.PartialUpdate.Admits φ (c ∩ p)) : DynamicSemantics.PartialUpdate.Admits (globalNeg φ p) c

Both options make the update defined once the amended context admits S.

theorem Heim1983.localNeg_admits {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c : Set W} (h : DynamicSemantics.PartialUpdate.Admits φ (c ∩ p)) : DynamicSemantics.PartialUpdate.Admits (localNeg φ p) c

theorem Heim1983.globalNeg_entails {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c c' : Set W} (h : c' ∈ globalNeg φ p c) : c' ⊆ p

The global option's result entails the accommodated presupposition, so (16) read in isolation has France with a king.

theorem Heim1983.localNeg_entails {W : Type u_1} {p : Set W} {came : W → Prop} [DecidablePred came] {c c' : Set W} (h : c' ∈ localNeg (DynamicSemantics.CCP.Partial.ofTrivalent (p.indicator fun (w : W) => SignType.ofProp (came w))) p c) : c' = {w : W | w ∈ c ∧ (w ∉ p ∨ ¬came w)}

The local option's result is the context minus the amended update, so (16) continued with because France doesn't have a king entails only that either France has no king or he did not come.

theorem Heim1983.globalNeg_disjoint {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c c' : Set W} (h : c' ∈ globalNeg φ p c) : c' ∩ pᶜ = ∅

The local option is what a continuation denying the presupposition needs, since the global result cannot contain a world without the presupposition and the local one can.

noncomputable def Heim1983.preferGlobal {W : Type u_1} (k g l : Set W) : Set W

The paper's ceteris paribus preference for global over local accommodation takes the global result g continued by k, unless k is inconsistent with it, and otherwise the local result l continued by k.

Equations

• Heim1983.preferGlobal k g l = if (g ∩ k).Nonempty then g ∩ k else l ∩ k

theorem Heim1983.preferGlobal_univ_subset {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c g : Set W} (l : Set W) (hg : g ∈ globalNeg φ p c) (hne : g.Nonempty) : preferGlobal Set.univ g l ⊆ p

In (16) in isolation nothing contradicts the global result, so the preferred reading entails that France has a king.

theorem Heim1983.preferGlobal_compl {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c g : Set W} (l : Set W) (hg : g ∈ globalNeg φ p c) : preferGlobal pᶜ g l = l ∩ pᶜ

When (16) is continued with because France doesn't have a king, the continuation is inconsistent with the global result, so the preferred reading is the local one.

theorem Heim1983.cancellation_only_under_inconsistency {W : Type u_1} {φ : DynamicSemantics.CCP.Partial W} {p c g l k : Set W} (hg : g ∈ globalNeg φ p c) (h : ¬preferGlobal k g l ⊆ p) : g ∩ k = ∅

The preference recaptures [Gaz79]'s assumption that presupposition cancellation occurs only under the threat of inconsistency. A preferred reading that does not entail the presupposition comes from a global result inconsistent with the continuation.

Files: contexts as sets of sequence–world pairs (§3)

@[reducible, inline]

abbrev Heim1983.File (M : Type u_3) (W : Type u_4) : Type (max u_4 u_3)

A file is a set of pairs of a sequence of individuals and a world (§3.1).

Equations

• Heim1983.File M W = Set ((ℕ → M) × W)

def Heim1983.File.prop {M : Type u_1} {W : Type u_2} (c : File M W) : Set W

The proposition a file determines (17).

Equations

• c.prop = {w : W | ∃ (g : ℕ → M), (g, w) ∈ c}

def Heim1983.File.TrueIn {M : Type u_1} {W : Type u_2} (c : File M W) (w : W) : Prop

A file is true in a world when some sequence fits it there (18).

Equations

• c.TrueIn w = ∃ (g : ℕ → M), (g, w) ∈ c

def Heim1983.atom {M : Type u_1} {W : Type u_2} (P : M → W → Prop) (i : ℕ) : DynamicSemantics.CCP.Partial ((ℕ → M) × W)

The update by an open sentence P xᵢ without presupposition (19).

Equations

• Heim1983.atom P i = DynamicSemantics.PartialUpdate.ofTotal fun (c : Set ((ℕ → M) × W)) => {gw : (ℕ → M) × W | gw ∈ c ∧ P (gw.1 i) gw.2}

def Heim1983.atomP {M : Type u_1} {W : Type u_2} (pre P : M → W → Prop) (i : ℕ) : DynamicSemantics.CCP.Partial ((ℕ → M) × W)

An open sentence P xᵢ presupposing pre xᵢ is admitted by a file iff every pair in it satisfies the presupposition at the i-th member (20).

Equations

• Heim1983.atomP pre P i c = { Dom := ∀ gw ∈ c, pre (gw.1 i) gw.2, get := fun (x : ∀ gw ∈ c, pre (gw.1 i) gw.2) => {gw : (ℕ → M) × W | gw ∈ c ∧ P (gw.1 i) gw.2} }

def Heim1983.File.everyClause {M : Type u_1} {W : Type u_2} (i : ℕ) (c cA cAB : File M W) : File M W

The clause of (21) keeps the pairs of c each of whose i-variants in cA survives in cAB.

Equations

• Heim1983.File.everyClause i c cA cAB = {gw : (ℕ → M) × W | gw ∈ c ∧ ∀ (a : M), (Function.update gw.1 i a, gw.2) ∈ cA → (Function.update gw.1 i a, gw.2) ∈ cAB}

def Heim1983.every {M : Type u_1} {W : Type u_2} (i : ℕ) (A B : DynamicSemantics.CCP.Partial ((ℕ → M) × W)) : DynamicSemantics.CCP.Partial ((ℕ → M) × W)

c + Every xᵢ, A, B (21) keeps the pairs of c each of whose i-variants in c + A survives in c + A + B, and is defined iff c + A and c + A + B are.

Equations

• Heim1983.every i A B c = (A c).bind fun (cA : Set ((ℕ → M) × W)) => Part.map (fun (cAB : Heim1983.File M W) => Heim1983.File.everyClause i c cA cAB) (B cA)

def Heim1983.File.NovelIn {M : Type u_1} {W : Type u_2} (c : File M W) (i : ℕ) : Prop

The file does not yet distinguish the i-th member of a sequence (22), the lexical novelty requirement of every and of an indefinite indexed i.

Equations

• c.NovelIn i = ∀ (g : ℕ → M) (w : W) (a : M), (g, w) ∈ c ↔ (Function.update g i a, w) ∈ c

theorem Heim1983.atom_admits {M : Type u_1} {W : Type u_2} (P : M → W → Prop) (i : ℕ) (c : File M W) : DynamicSemantics.PartialUpdate.Admits (atom P i) c

theorem Heim1983.atomP_admits_iff {M : Type u_1} {W : Type u_2} (pre P : M → W → Prop) (i : ℕ) (c : File M W) : DynamicSemantics.PartialUpdate.Admits (atomP pre P i) c ↔ ∀ gw ∈ c, pre (gw.1 i) gw.2

theorem Heim1983.every_admits_iff {M : Type u_1} {W : Type u_2} (i : ℕ) (A B : DynamicSemantics.CCP.Partial ((ℕ → M) × W)) (c : File M W) : DynamicSemantics.PartialUpdate.Admits (every i A B) c ↔ ∃ (h : DynamicSemantics.PartialUpdate.Admits A c), DynamicSemantics.PartialUpdate.Admits B ((A c).get h)

The heritage of every is that c admits Every xᵢ, A, B iff it admits A and c + A admits B.

theorem Heim1983.every_atom_admits_iff {M : Type u_1} {W : Type u_2} (i : ℕ) (A pre B : M → W → Prop) (c : File M W) : DynamicSemantics.PartialUpdate.Admits (every i (atom A i) (atomP pre B i)) c ↔ ∀ gw ∈ c, A (gw.1 i) gw.2 → pre (gw.1 i) gw.2

With a presupposition-free restrictor A xᵢ and a nuclear scope presupposing pre xᵢ, the file must satisfy pre at the i-th member of every pair that survives A ((ii) of §3.2).

theorem Heim1983.every_nation_presupposes {M : Type u_1} {W : Type u_2} (i : ℕ) (nation hasKing cherishes : M → W → Prop) {c : File M W} (hc : c.NovelIn i) : DynamicSemantics.PartialUpdate.Admits (every i (atom nation i) (atomP hasKing cherishes i)) c ↔ ∀ w ∈ c.prop, ∀ (a : M), nation a w → hasKing a w

(7) presupposes that every nation has a king. Under (22) the condition of every_atom_admits_iff holds iff, in every world of the file's proposition, every individual satisfying the restrictor satisfies the presupposition. The novelty stipulation is what makes the universal presupposition necessary, not only sufficient.

theorem Heim1983.every_restrictor_presupposes {M : Type u_1} {W : Type u_2} (i : ℕ) (hasKing serves rewarded : M → W → Prop) {c : File M W} (hc : c.NovelIn i) : DynamicSemantics.PartialUpdate.Admits (every i (atomP hasKing serves i) (atom rewarded i)) c ↔ ∀ w ∈ c.prop, ∀ (a : M), hasKing a w

A presupposition in the restrictor projects universally too (23). Everyone who serves his king will be rewarded presupposes that everyone has a king, where [KP79] predict no presupposition.

Files as uniform states

A file whose membership depends only on the cards in X is, restricted to X, an information state uniform at X, and on such files the clauses (19), (15) and (21) are the file change potentials of [Hei82a] on that stratum.

noncomputable def Heim1983.File.pointAt {M : Type u_1} {W : Type u_2} (X : Set ℕ) (gw : (ℕ → M) × W) : DynamicSemantics.Possibility W ℕ (Flat M)

The point of a sequence–world pair at the cards X restricts the sequence to X.

Equations

• Heim1983.File.pointAt X gw = ↑((DynamicSemantics.Possibility.domainEquiv X).symm (gw.2, fun (i : ↑X) => gw.1 ↑i))

@[simp]

theorem Heim1983.File.pointAt_world {M : Type u_1} {W : Type u_2} {X : Set ℕ} (gw : (ℕ → M) × W) : (pointAt X gw).world = gw.2

@[simp]

theorem Heim1983.File.domain_pointAt {M : Type u_1} {W : Type u_2} {X : Set ℕ} (gw : (ℕ → M) × W) : (pointAt X gw).domain = X

theorem Heim1983.File.pointAt_assignment {M : Type u_1} {W : Type u_2} {X : Set ℕ} (gw : (ℕ → M) × W) (j : ℕ) : (pointAt X gw).assignment j = if j ∈ X then ↑(gw.1 j) else ⊥

theorem Heim1983.File.pointAt_assignment_eq_coe_iff {M : Type u_1} {W : Type u_2} {X : Set ℕ} {g : ℕ → M} {w : W} {i : ℕ} {m : M} : (pointAt X (g, w)).assignment i = ↑m ↔ i ∈ X ∧ g i = m

theorem Heim1983.File.pointAt_eq_coe {M : Type u_1} {W : Type u_2} {X : Set ℕ} {g : ℕ → M} {w : W} {i : ℕ} (hj : i ∈ X) : (pointAt X (g, w)).assignment i = ↑(g i)

theorem Heim1983.File.pointAt_le_pointAt {M : Type u_1} {W : Type u_2} {X Y : Set ℕ} {g g' : ℕ → M} {w w' : W} : pointAt X (g, w) ≤ pointAt Y (g', w') ↔ X ⊆ Y ∧ w = w' ∧ Set.EqOn g g' X

Points descend as their cards and values extend.

theorem Heim1983.File.pointAt_eq_pointAt {M : Type u_1} {W : Type u_2} {X : Set ℕ} {g g' : ℕ → M} {w w' : W} : pointAt X (g, w) = pointAt X (g', w') ↔ w = w' ∧ Set.EqOn g g' X

def Heim1983.File.toState {M : Type u_1} {W : Type u_2} (X : Set ℕ) (c : File M W) : DynamicSemantics.State W ℕ M

The state of a file at the cards X.

Equations

• Heim1983.File.toState X c = Heim1983.File.pointAt X '' c

theorem Heim1983.File.mem_toState {M : Type u_1} {W : Type u_2} {X : Set ℕ} {c : File M W} {p : DynamicSemantics.Possibility W ℕ (Flat M)} : p ∈ toState X c ↔ ∃ gw ∈ c, pointAt X gw = p

theorem Heim1983.File.uniformAt_toState {M : Type u_1} {W : Type u_2} {X : Set ℕ} {c : File M W} : DynamicSemantics.State.UniformAt X (toState X c)

def Heim1983.File.DeterminedBy {M : Type u_1} {W : Type u_2} (X : Set ℕ) (c : File M W) : Prop

A file is determined by the cards X when its membership depends only on them.

Equations

• Heim1983.File.DeterminedBy X c = ∀ ⦃g g' : ℕ → M⦄ ⦃w : W⦄, Set.EqOn g g' X → (g, w) ∈ c → (g', w) ∈ c

theorem Heim1983.File.DeterminedBy.mono {M : Type u_1} {W : Type u_2} {X Y : Set ℕ} {c : File M W} (h : X ⊆ Y) (hc : DeterminedBy X c) : DeterminedBy Y c

theorem Heim1983.File.novelIn_iff_determinedBy {M : Type u_1} {W : Type u_2} {i : ℕ} {c : File M W} : c.NovelIn i ↔ DeterminedBy {i}ᶜ c

(22) is independence of the card, the file not distinguishing i iff it is determined by the other cards.

theorem Heim1983.File.pointAt_mem_toState {M : Type u_1} {W : Type u_2} {X : Set ℕ} {c : File M W} (hc : DeterminedBy X c) (gw : (ℕ → M) × W) : pointAt X gw ∈ toState X c ↔ gw ∈ c

theorem Heim1983.File.toState_mul_stratum {M : Type u_1} {W : Type u_2} {X Y : Set ℕ} {c : File M W} (hc : DeterminedBy X c) : toState X c * DynamicSemantics.State.stratum Y = toState (X ∪ Y) c

Extension along cards is the state of the file at more cards, since the file, being determined by X, already ranges over every value at the new cards.

theorem Heim1983.File.toState_sep {M : Type u_1} {W : Type u_2} {X : Set ℕ} {i : ℕ} {c : File M W} (hi : i ∈ X) (P : M → W → Prop) : toState X {gw : (ℕ → M) × W | gw ∈ c ∧ P (gw.1 i) gw.2} = {r : DynamicSemantics.Possibility W ℕ (Flat M) | r ∈ toState X c ∧ ∃ (m : M), r.assignment i = ↑m ∧ P m r.world}

theorem Heim1983.File.toState_atom {M : Type u_1} {W : Type u_2} {X : Set ℕ} {i : ℕ} {c : File M W} (hc : DeterminedBy X c) (P : M → W → Prop) : toState (insert i X) {gw : (ℕ → M) × W | gw ∈ c ∧ P (gw.1 i) gw.2} = toState X c * DynamicSemantics.State.atomAt i fun (w : W) (m : M) => P m w

(19) is the atomic rule of [Hei82a]. The update of a file by an open sentence, read at the cards of the file together with the sentence's, is the merge of the file's state with the atom's proposition state.

theorem Heim1983.File.toState_sdiff {M : Type u_1} {W : Type u_2} {X : Set ℕ} {c c' : File M W} (hc' : DeterminedBy X c') : toState X (c \ c') = toState X c \ toState X c'

theorem Heim1983.File.neg_toState {M : Type u_1} {W : Type u_2} {X : Set ℕ} {c c' : File M W} {φ : FCP W ℕ M} (hφ : φ (toState X c) = Part.some (toState X c')) (hc' : DeterminedBy X c') : φ.neg (toState X c) = Part.some (toState X (c \ c'))

(15) is non-subsistence negation. On the stratum, a potential that sends the file's state to a determined file's state negates, in the sense of [Hei82a], to the set difference of the files.

theorem Heim1983.File.toState_everyClause {M : Type u_1} {W : Type u_2} {X : Set ℕ} {i : ℕ} {c cA cAB : File M W} (hi : i ∉ X) (hA : DeterminedBy (insert i X) cA) (hB : DeterminedBy (insert i X) cAB) : toState X (everyClause i c cA cAB) = {p : DynamicSemantics.Possibility W ℕ (Flat M) | p ∈ toState X c ∧ ∀ q ∈ toState (insert i X) cA, p ≤ q → ∃ r ∈ toState (insert i X) cAB, q ≤ r}

(21) is rule (III) of [Hei82a]. On files determined by their cards, the clause keeping the pairs each of whose i-variants surviving A survives B is the clause keeping the points each of whose extensions in F + A extends into (F + A) + B.

Indefinites (§3.3)

def Heim1983.fatManBicycle {M : Type u_1} {W : Type u_2} (i : ℕ) (fatMan hasBicycle pushing : M → W → Prop) : DynamicSemantics.CCP.Partial ((ℕ → M) × W)

A fat man was pushing his bicycle (26)–(27) is the sequence of two open sentences, the second presupposing that xᵢ has a bicycle.

Equations

• Heim1983.fatManBicycle i fatMan hasBicycle pushing = DynamicSemantics.PartialUpdate.seq (Heim1983.atom fatMan i) (Heim1983.atomP hasBicycle pushing i)

theorem Heim1983.fatManBicycle_admits_iff {M : Type u_1} {W : Type u_2} (i : ℕ) (fatMan hasBicycle pushing : M → W → Prop) {c : File M W} (hc : c.NovelIn i) : DynamicSemantics.PartialUpdate.Admits (fatManBicycle i fatMan hasBicycle pushing) c ↔ ∀ w ∈ c.prop, ∀ (a : M), fatMan a w → hasBicycle a w

Without accommodation, (25) carries the universal presupposition that every fat man had a bicycle by (22), which is prima facie too strong.

def Heim1983.fatManBicycleAcc {M : Type u_1} {W : Type u_2} (i : ℕ) (fatMan hasBicycle pushing : M → W → Prop) : DynamicSemantics.CCP.Partial ((ℕ → M) × W)

Accommodation in the course of the update amends c + "xᵢ is a fat man" with xᵢ has a bicycle before the second sentence is evaluated.

Equations

• Heim1983.fatManBicycleAcc i fatMan hasBicycle pushing c = Heim1983.atomP hasBicycle pushing i {gw : (ℕ → M) × W | gw ∈ c ∧ fatMan (gw.1 i) gw.2 ∧ hasBicycle (gw.1 i) gw.2}

theorem Heim1983.fatManBicycleAcc_admits {M : Type u_1} {W : Type u_2} (i : ℕ) (fatMan hasBicycle pushing : M → W → Prop) (c : File M W) : DynamicSemantics.PartialUpdate.Admits (fatManBicycleAcc i fatMan hasBicycle pushing) c

The accommodated update is always defined, and its result entails that xᵢ was a fat man, had a bicycle, and was pushing it.

theorem Heim1983.fatManBicycleAcc_entails {M : Type u_1} {W : Type u_2} (i : ℕ) (fatMan hasBicycle pushing : M → W → Prop) {c c' : File M W} (h : c' ∈ fatManBicycleAcc i fatMan hasBicycle pushing c) (gw : (ℕ → M) × W) : gw ∈ c' → fatMan (gw.1 i) gw.2 ∧ hasBicycle (gw.1 i) gw.2 ∧ pushing (gw.1 i) gw.2

theorem Heim1983.fatManBicycleAcc_not_universal : ∃ c' ∈ fatManBicycleAcc 0 (fun (x : Bool) (x_1 : Unit) => True) (fun (a : Bool) (x : Unit) => a = true) (fun (x : Bool) (x_1 : Unit) => True) Set.univ, c'.TrueIn () ∧ ¬∀ w ∈ c'.prop, ∀ (a : Bool), a = true

The accommodated result entails nothing about fat men in general. In a two-individual model where only one fat man has a bicycle, the update is defined and non-empty.

The conjunction filter of Karttunen (1973)

theorem Heim1983.admits_seq_iff_conj {W : Type u_1} (c : Set W) (p q : W → SignType) : (DynamicSemantics.PartialUpdate.seq (DynamicSemantics.CCP.Partial.ofTrivalent p) (DynamicSemantics.CCP.Partial.ofTrivalent q)).Admits c ↔ ∀ C ∈ Writer.log (Karttunen1973.conj (fun (P C : Set W) => c ∩ P ⊆ C) (Karttunen1973.Presupposing.ofTrivalent p) (Karttunen1973.Presupposing.ofTrivalent q)), c ⊆ C

Admittance of the sequenced update is [Kar74a]'s satisfaction condition for conjunction, that the context satisfies the presuppositions of the first conjunct, and the context incremented with the first conjunct those of the second. [Kar73]'s filter for conjunction, relativized to the context as its assumed facts, requires the same of the context, the equivalence [Kar74a] proves for the conditional, (8)–(14). The relativized filter leaves out Murphy's restriction that the facts be consistent with the first conjunct, under which a context contradicting the first conjunct would still have to satisfy the presuppositions of the second, though it admits the update.