Mandelkern (2022): Witnesses

This file formalizes Mandelkern's bounded theory of definites and indefinites. The language is first-order with a two-place indefinite ɜx(p, q), a two-place definite ιx(p, q), of which a pronoun is the case with the tautological restrictor ⊤x, and quantifiers Q x^δ (p, q) over domain variables. Truth at an assignment–world pair is classical. A second dimension, the bounds, is satisfied (satt) relative to a context, a set of such pairs: an indefinite's witness bound, that if it is true its variable denotes a witness; a definite's familiarity bound, that its restrictor is true and satt throughout the context; and a quantifier's bounds, that it pairs each individual with an assignment making its restrictor and scope satt without moving familiar variables. Bounds project through local contexts, asymmetric or symmetric, and updating a context keeps the points at which a sentence is true and satt.

At a context the two dimensions form a trivalent proposition (Formula.toTrivalent), undefined where the bounds fail, so bound entailment is Strawson entailment at every context (BoundEntails). An indefinite keeps the points whose variable is a witness, so a later pronoun finds it familiar, while the logically equivalent Sue is a parent licenses none; double negation and the bathroom disjunction keep the indefinite's witness. Under a quantifier the same contrast is covariation: everyone who has a child loves them pairs each parent with a child, while every parent loves them can only be about one familiar individual. With asymmetric local contexts a pronoun cannot precede its indefinite in a conjunction; with symmetric ones it can. The three renderings of open scope in (20) are true and satt at the same indices without being logically equivalent, and footnote 20's extension of their bound equivalences to arbitrary formulae fails for one of them (not_boundEntails_ex20b_ex20a).

Main statements

• update_indef_then_it, logicallyEquivalent_hasChild_isParent, update_isParent_then_it: an indefinite licenses a later pronoun, and a logically equivalent sentence without one does not.
• realize_ex22b_iff, realize_ex21b_iff_of_familiar: a pronoun covaries under a quantifier only with an indefinite in the restrictor.
• felicitous_ex15a_asymmetric, not_felicitous_ex15b_asymmetric, satt_ex15b_symmetric: a pronoun after its indefinite in a conjunction is felicitous, and one before it depends on the order of local contexts.

Implementation notes

• An atomic valuation is a world-indexed family of structures I : W → L.Structure E, and atoms take variables only. Bounds fill the presupposition slot, the support of the trivalent proposition, though the paper leaves open whether they are presuppositions; not_univ_subset_support_indef_atom₁ shows why update keeps the true and satt points rather than requiring admission.
• A domain variable's value pairs every individual with an assignment, which builds in the bound that each individual has one pair, and the paired assignments value individual variables only; in the paper the value is a set of pairs whose assignments value domain variables too.
• The quantifier bound on variables not novel in the context reads them, as the paper's parenthetical does, as the already familiar ones, valued at every point; §3's gloss of novelty as nowhere defined would fix every variable in the null context and block (22-b).
• Determiners are number trees: .all is the paper's every on finite domains, and .most its most where the restrictor set is finite and nonempty.

TODO

• The weak and strong readings of donkey sentences (p. 1111).
• The cross-world witness bound for modal subordination sketched in the conclusion, (23)–(24).

References

• [Man22]
• [Hei82a]
• [Kar76]
• [Sch09a]
• [Sta78]
• [vF99a]

inductive Mandelkern2022.Order : Type

The two orders of local contexts the paper compares (p. 1106).

• asymmetric : Order

  The left junct's local context is the global context, and the right junct's is the global context updated with the left junct (p. 1105).

• symmetric : Order

  Each junct's local context is the global context updated with the other junct (p. 1106).

@[instance_reducible]

instance Mandelkern2022.instDecidableEqOrder : DecidableEq Order

Equations

• Mandelkern2022.instDecidableEqOrder x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Mandelkern2022.Assign (V : Type u_1) (Δ : Type u_2) (E : Type u_3) : Type (max (max u_1 u_2) u_3)

An assignment of both sorts of variable (p. 1110). Individual variables take individuals, partially, and a domain variable pairs every individual with an assignment.

• ind : PartialAssign V E

  The values of the individual variables.

• dom : Δ → E → PartialAssign V E

  The value of each domain variable, pairing every individual with an assignment.

@[instance_reducible]

instance Mandelkern2022.Assign.instCoeFunForallFlat {V : Type u_1} {Δ : Type u_2} {E : Type u_3} : CoeFun (Assign V Δ E) fun (x : Assign V Δ E) => V → Flat E

Equations

• Mandelkern2022.Assign.instCoeFunForallFlat = { coe := fun (g : Mandelkern2022.Assign V Δ E) => g.ind }

@[instance_reducible]

instance Mandelkern2022.Assign.instBot {V : Type u_1} {Δ : Type u_2} {E : Type u_3} : Bot (Assign V Δ E)

The assignment valuing no individual variable and pairing every individual with it.

Equations

• Mandelkern2022.Assign.instBot = { bot := { ind := ⊥, dom := fun (x : Δ) (x_1 : E) => ⊥ } }

@[simp]

theorem Mandelkern2022.Assign.coe_mk {V : Type u_1} {Δ : Type u_2} {E : Type u_3} (i : PartialAssign V E) (d : Δ → E → PartialAssign V E) (x : V) : { ind := i, dom := d }.ind x = i x

@[simp]

theorem Mandelkern2022.Assign.bot_apply {V : Type u_1} {Δ : Type u_2} {E : Type u_3} (x : V) : ⊥.ind x = ⊥

def Mandelkern2022.Assign.update {V : Type u_1} {Δ : Type u_2} {E : Type u_3} [DecidableEq V] (g : Assign V Δ E) (x : V) (a : E) : Assign V Δ E

g[x→a], the assignment resetting the individual variable x to a.

Equations

• g.update x a = { ind := g.ind.update x a, dom := g.dom }

@[simp]

theorem Mandelkern2022.Assign.update_apply_self {V : Type u_1} {Δ : Type u_2} {E : Type u_3} [DecidableEq V] {g : Assign V Δ E} {x : V} {a : E} : (g.update x a).ind x = ↑a

@[simp]

theorem Mandelkern2022.Assign.update_apply_of_ne {V : Type u_1} {Δ : Type u_2} {E : Type u_3} [DecidableEq V] {g : Assign V Δ E} {x y : V} {a : E} (h : y ≠ x) : (g.update x a).ind y = g.ind y

theorem Mandelkern2022.Assign.update_eq_self {V : Type u_1} {Δ : Type u_2} {E : Type u_3} [DecidableEq V] {g : Assign V Δ E} {x : V} {a : E} (h : g.ind x = ↑a) : g.update x a = g

def Mandelkern2022.Assign.pair {V : Type u_1} {Δ : Type u_2} {E : Type u_3} [DecidableEq V] (g : Assign V Δ E) (δ : Δ) (x : V) (a : E) : Assign V Δ E

The assignment at which a quantifier over the domain variable δ evaluates its restrictor and scope at the individual a, the paired assignment reset at x to a (p. 1110).

Equations

• g.pair δ x a = { ind := (g.dom δ a).update x a, dom := g.dom }

@[simp]

theorem Mandelkern2022.Assign.pair_apply {V : Type u_1} {Δ : Type u_2} {E : Type u_3} [DecidableEq V] {g : Assign V Δ E} {x : V} (δ : Δ) (a : E) (y : V) : (g.pair δ x a).ind y = (g.dom δ a).update x a y

inductive Mandelkern2022.Formula (L : FirstOrder.Language) (V : Type u_1) (Δ : Type u_2) : Type (max (max u_1 u_2) u_4)

The language of the paper (pp. 1101 and 1110), with atoms over variables, the pronoun restrictor ⊤x, the classical connectives, the two-place indefinite and definite, and the generalized quantifiers.

• atom {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {n : ℕ} (R : L.Relations n) (xs : Fin n → V) : Formula L V Δ

  The atom A(x₁, …, xₙ).

• top {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (x : V) : Formula L V Δ

  The tautological restrictor ⊤x of a pronoun.

• conj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (p q : Formula L V Δ) : Formula L V Δ

  Conjunction p & q.

• disj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (p q : Formula L V Δ) : Formula L V Δ

  Disjunction p ∨ q.

• neg {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (p : Formula L V Δ) : Formula L V Δ

  Negation ¬p.

• indef {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (x : V) (p q : Formula L V Δ) : Formula L V Δ

  The indefinite ɜx(p, q), some p is q.

• iota {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (x : V) (p q : Formula L V Δ) : Formula L V Δ

  The definite ιx(p, q), the p is q.

• quant {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (Q : Quantifier.NumberTree) (x : V) (δ : Δ) (p q : Formula L V Δ) : Formula L V Δ

  The quantifier Q x^δ (p, q) over the domain variable δ, whose determiner is a number tree, every being .all and most .most (p. 1110).

def Mandelkern2022.Order.junct {A : Type u_1} {W : Type u_2} (o : Order) (sp sq : Set (A × W) → A → W → Prop) (kp kq : A → W → Prop) (c : Set (A × W)) (g : A) (w : W) : Prop

The local contexts of a junction of p and q in each order (pp. 1105–1106), where sp and sq are the juncts' bounds and kp, kq select the points of a junct's local context, where it is true in a conjunction and false in a disjunction.

Equations

• Mandelkern2022.Order.asymmetric.junct sp sq kp kq c g w = (sp c g w ∧ sq {i : A × W | i ∈ c ∧ kp i.1 i.2 ∧ sp c i.1 i.2} g w)
• Mandelkern2022.Order.symmetric.junct sp sq kp kq c g w = (sp {i : A × W | i ∈ c ∧ kq i.1 i.2 ∧ sq c i.1 i.2} g w ∧ sq {i : A × W | i ∈ c ∧ kp i.1 i.2 ∧ sp c i.1 i.2} g w)

theorem Mandelkern2022.Order.junct_right {A : Type u_1} {W : Type u_2} {o : Order} {sp sq : Set (A × W) → A → W → Prop} {kp kq : A → W → Prop} {c : Set (A × W)} {g : A} {w : W} (h : o.junct sp sq kp kq c g w) : sq {i : A × W | i ∈ c ∧ kp i.1 i.2 ∧ sp c i.1 i.2} g w

In either order the right junct's local context is the left junct's update.

def Mandelkern2022.Familiar {V : Type u_1} {Δ : Type u_2} {E : Type u_3} {W : Type u_4} (c : Set (Assign V Δ E × W)) (y : V) : Prop

A variable is familiar in a context when every point of the context values it (p. 1103); the paper's not novel in the bounds of quantifiers.

Equations

• Mandelkern2022.Familiar c y = ∀ i ∈ c, i.1.ind y ≠ ⊥

def Mandelkern2022.extension {L : FirstOrder.Language} {W : Type u_3} {E : Type u_4} (I : W → L.Structure E) (R : L.Relations 1) (w : W) : Set E

The extension A_w of a one-place relation symbol at a world (p. 1103).

Equations

• Mandelkern2022.extension I R w = {a : E | FirstOrder.Language.Structure.RelMap R ![a]}

def Mandelkern2022.valuedIn {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} (x : V) (S : W → Set E) : Set (Assign V Δ E × W)

The points at which x has a value in S, as given at the point's world.

Equations

• Mandelkern2022.valuedIn x S = {i : Mandelkern2022.Assign V Δ E × W | ∃ a ∈ S i.2, i.1.ind x = ↑a}

@[simp]

theorem Mandelkern2022.mem_extension {L : FirstOrder.Language} {W : Type u_3} {E : Type u_4} {I : W → L.Structure E} {R : L.Relations 1} {w : W} {a : E} : a ∈ extension I R w ↔ FirstOrder.Language.Structure.RelMap R ![a]

@[simp]

theorem Mandelkern2022.mem_valuedIn {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} {S : W → Set E} {x : V} {i : Assign V Δ E × W} : i ∈ valuedIn x S ↔ ∃ a ∈ S i.2, i.1.ind x = ↑a

theorem Mandelkern2022.valuedIn_inter_valuedIn {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} {S T : W → Set E} {x : V} : valuedIn x S ∩ valuedIn x T = valuedIn x (S ⊓ T)

theorem Mandelkern2022.valuedIn_mono {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} {S T : W → Set E} {x : V} (h : S ≤ T) : valuedIn x S ⊆ valuedIn x T

theorem Mandelkern2022.ne_bot_of_mem_valuedIn {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} {S : W → Set E} {x : V} {i : Assign V Δ E × W} (h : i ∈ valuedIn x S) : i.1.ind x ≠ ⊥

def Mandelkern2022.Formula.Realize {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) : Formula L V Δ → Assign V Δ E → W → Prop

Truth at an assignment and a world (pp. 1101, 1110 and 1114). An atom is true when its variables are valued and their values stand in the relation, and ⊤x is true when x is valued. A quantifier relates, by its number tree, the individuals whose paired assignments make the restrictor true to those that make the restrictor and scope true.

Equations

• One or more equations did not get rendered due to their size.
• Mandelkern2022.Formula.Realize I (Mandelkern2022.Formula.atom R xs) x✝¹ x✝ = ∃ (es : Fin n → E), (∀ (i : Fin n), x✝¹.ind (xs i) = ↑(es i)) ∧ FirstOrder.Language.Structure.RelMap R es
• Mandelkern2022.Formula.Realize I (Mandelkern2022.Formula.top x_3) x✝¹ x✝ = (x✝¹.ind x_3 ≠ ⊥)
• Mandelkern2022.Formula.Realize I (p.conj q) x✝¹ x✝ = (Mandelkern2022.Formula.Realize I p x✝¹ x✝ ∧ Mandelkern2022.Formula.Realize I q x✝¹ x✝)
• Mandelkern2022.Formula.Realize I (p.disj q) x✝¹ x✝ = (Mandelkern2022.Formula.Realize I p x✝¹ x✝ ∨ Mandelkern2022.Formula.Realize I q x✝¹ x✝)
• Mandelkern2022.Formula.Realize I p.neg x✝¹ x✝ = ¬Mandelkern2022.Formula.Realize I p x✝¹ x✝
• Mandelkern2022.Formula.Realize I (Mandelkern2022.Formula.iota x_3 p q) x✝¹ x✝ = (Mandelkern2022.Formula.Realize I p x✝¹ x✝ ∧ Mandelkern2022.Formula.Realize I q x✝¹ x✝)

def Mandelkern2022.Formula.Satt {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (o : Order) : Formula L V Δ → Set (Assign V Δ E × W) → Assign V Δ E → W → Prop

The bounds of a formula are satisfied (satt) at a context, an assignment and a world, in the order o (pp. 1105–1106, 1110 and 1114). A quantifier's bounds hold at every individual's paired assignment, whose restrictor and conjunction of restrictor and scope must be satt, and which agrees with the given assignment on the familiar variables.

Equations

• One or more equations did not get rendered due to their size.
• Mandelkern2022.Formula.Satt I o (Mandelkern2022.Formula.atom R xs) x✝² x✝¹ x✝ = ∀ (i : Fin n), x✝¹.ind (xs i) ≠ ⊥
• Mandelkern2022.Formula.Satt I o (Mandelkern2022.Formula.top x_4) x✝² x✝¹ x✝ = (x✝¹.ind x_4 ≠ ⊥)
• Mandelkern2022.Formula.Satt I o p.neg x✝² x✝¹ x✝ = Mandelkern2022.Formula.Satt I o p x✝² x✝¹ x✝

noncomputable def Mandelkern2022.Formula.toTrivalent {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (o : Order) (c : Set (Assign V Δ E × W)) (p : Formula L V Δ) : Assign V Δ E × W → SignType

The two dimensions of a formula's meaning at a context as a trivalent proposition, undefined where the bounds fail and otherwise the formula's truth value.

Equations

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

def Mandelkern2022.Formula.update {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (o : Order) (c : Set (Assign V Δ E × W)) (p : Formula L V Δ) : Set (Assign V Δ E × W)

Updating c with p keeps the points of c at which p is true and satt (p. 1103). This set is also the local context cᵖ of the projection clauses.

Equations

• Mandelkern2022.Formula.update I o c p = {i : Mandelkern2022.Assign V Δ E × W | i ∈ c ∧ Mandelkern2022.Formula.Realize I p i.1 i.2 ∧ Mandelkern2022.Formula.Satt I o p c i.1 i.2}

def Mandelkern2022.Formula.Felicitous {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (o : Order) (c : Set (Assign V Δ E × W)) (p : Formula L V Δ) : Prop

A sentence is felicitous in a context when its bounds hold at some point of it; infelicity is their failure at every point (p. 1104).

Equations

• Mandelkern2022.Formula.Felicitous I o c p = ∃ i ∈ c, Mandelkern2022.Formula.Satt I o p c i.1 i.2

Truth and bounds

@[simp]

theorem Mandelkern2022.Formula.realize_atom {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {n : ℕ} {R : L.Relations n} {xs : Fin n → V} : Realize I (atom R xs) g w ↔ ∃ (es : Fin n → E), (∀ (i : Fin n), g.ind (xs i) = ↑(es i)) ∧ FirstOrder.Language.Structure.RelMap R es

@[simp]

theorem Mandelkern2022.Formula.realize_top {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {x : V} : Realize I (top x) g w ↔ g.ind x ≠ ⊥

@[simp]

theorem Mandelkern2022.Formula.realize_conj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} : Realize I (p.conj q) g w ↔ Realize I p g w ∧ Realize I q g w

@[simp]

theorem Mandelkern2022.Formula.realize_disj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} : Realize I (p.disj q) g w ↔ Realize I p g w ∨ Realize I q g w

@[simp]

theorem Mandelkern2022.Formula.realize_neg {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p : Formula L V Δ} : Realize I p.neg g w ↔ ¬Realize I p g w

@[simp]

theorem Mandelkern2022.Formula.realize_indef {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} : Realize I (indef x p q) g w ↔ ∃ (a : E), Realize I p (g.update x a) w ∧ Realize I q (g.update x a) w

@[simp]

theorem Mandelkern2022.Formula.realize_iota {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} : Realize I (iota x p q) g w ↔ Realize I p g w ∧ Realize I q g w

@[simp]

theorem Mandelkern2022.Formula.realize_quant {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} {Q : Quantifier.NumberTree} {δ : Δ} : Realize I (quant Q x δ p q) g w ↔ Q.toGQ (fun (a : E) => Realize I p (g.pair δ x a) w) fun (a : E) => Realize I p (g.pair δ x a) w ∧ Realize I q (g.pair δ x a) w

theorem Mandelkern2022.Formula.satt_quant {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} {Q : Quantifier.NumberTree} {δ : Δ} : Satt I o (quant Q x δ p q) c g w ↔ ∀ (a : E), Satt I o p c (g.pair δ x a) w ∧ o.junct (Satt I o p) (Satt I o q) (Realize I p) (Realize I q) c (g.pair δ x a) w ∧ ∀ (y : V), Familiar c y → g.dom δ a y = g.ind y

A quantifier's bounds hold when at every individual's paired assignment the restrictor is satt, the restrictor and scope are satt as a junction, and the familiar variables keep their values (p. 1114).

@[simp]

theorem Mandelkern2022.Formula.mem_update {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} {i : Assign V Δ E × W} : i ∈ update I o c p ↔ i ∈ c ∧ Realize I p i.1 i.2 ∧ Satt I o p c i.1 i.2

theorem Mandelkern2022.Formula.update_subset {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} : update I o c p ⊆ c

@[simp]

theorem Mandelkern2022.Formula.toTrivalent_eq_zero_iff {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} {i : Assign V Δ E × W} : toTrivalent I o c p i = 0 ↔ ¬Satt I o p c i.1 i.2

@[simp]

theorem Mandelkern2022.Formula.toTrivalent_eq_one_iff {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} {i : Assign V Δ E × W} : toTrivalent I o c p i = 1 ↔ Satt I o p c i.1 i.2 ∧ Realize I p i.1 i.2

theorem Mandelkern2022.Formula.update_eq_inter_posExt {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} : update I o c p = c ∩ Trivalent.posExt (toTrivalent I o c p)

Updating keeps the points of the context at which the meaning there is true.

@[simp]

theorem Mandelkern2022.Formula.satt_atom {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {n : ℕ} {R : L.Relations n} {xs : Fin n → V} : Satt I o (atom R xs) c g w ↔ ∀ (i : Fin n), g.ind (xs i) ≠ ⊥

@[simp]

theorem Mandelkern2022.Formula.satt_top {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} : Satt I o (top x) c g w ↔ g.ind x ≠ ⊥

theorem Mandelkern2022.Formula.satt_conj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} : Satt I Order.asymmetric (p.conj q) c g w ↔ Satt I Order.asymmetric p c g w ∧ Satt I Order.asymmetric q (update I Order.asymmetric c p) g w

theorem Mandelkern2022.Formula.satt_disj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} : Satt I Order.asymmetric (p.disj q) c g w ↔ Satt I Order.asymmetric p c g w ∧ Satt I Order.asymmetric q (update I Order.asymmetric c p.neg) g w

The right disjunct is satt at the local context c¬ᵖ.

@[simp]

theorem Mandelkern2022.Formula.satt_neg {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p : Formula L V Δ} : Satt I o p.neg c g w ↔ Satt I o p c g w

theorem Mandelkern2022.Formula.satt_indef {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} : Satt I o (indef x p q) c g w ↔ (∃ (g' : Assign V Δ E), Satt I o (p.conj q) c g' w) ∧ (Realize I (indef x p q) g w → Realize I (p.conj q) g w ∧ Satt I o (p.conj q) c g w)

An indefinite's bounds hold when its body is satt at some assignment and, if the indefinite is true, its body is true and satt at the given one (p. 1114).

theorem Mandelkern2022.Formula.satt_iota {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} : Satt I o (iota x p q) c g w ↔ update I o c p = c ∧ (Realize I p g w → Satt I o q (update I o c p) g w)

A definite's bounds hold when updating with its restrictor leaves the context unchanged and its scope is satt at cᵖ if the restrictor is true (p. 1114).

theorem Mandelkern2022.Formula.realize_indef_of_ne_bot {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} (hx : g.ind x ≠ ⊥) (hp : Realize I p g w) (hq : Realize I q g w) : Realize I (indef x p q) g w

theorem Mandelkern2022.Formula.realize_conj_of_satt_indef {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {p q : Formula L V Δ} {x : V} (hs : Satt I o (indef x p q) c g w) (hr : Realize I (indef x p q) g w) : Realize I p g w ∧ Realize I q g w

A true indefinite whose bounds hold has a true body.

The calculus of positive extensions

The points at which a formula is true and satt at a context, the positive extension posExt (p.toTrivalent I o c), decompose along the connectives; updating a context intersects it with this set (update_eq_inter_posExt).

theorem Mandelkern2022.Formula.posExt_conj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} : Trivalent.posExt (toTrivalent I Order.asymmetric c (p.conj q)) = Trivalent.posExt (toTrivalent I Order.asymmetric c p) ∩ Trivalent.posExt (toTrivalent I Order.asymmetric (update I Order.asymmetric c p) q)

A conjunction is true and satt where its left conjunct is, at the context, and its right conjunct is, at the left conjunct's local context.

theorem Mandelkern2022.Formula.posExt_indef {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} : Trivalent.posExt (toTrivalent I o c (indef x p q)) = {i : Assign V Δ E × W | i ∈ Trivalent.posExt (toTrivalent I o c (p.conj q)) ∧ Realize I (indef x p q) i.1 i.2}

An indefinite is true and satt where its body is and the indefinite is true.

theorem Mandelkern2022.Formula.posExt_indef_of_ne_bot {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} (hp : ∀ (g : Assign V Δ E) (w : W), Realize I p g w → g.ind x ≠ ⊥) : Trivalent.posExt (toTrivalent I o c (indef x p q)) = Trivalent.posExt (toTrivalent I o c (p.conj q))

An indefinite whose restrictor values its variable is true and satt where its body is.

theorem Mandelkern2022.Formula.posExt_iota_of_update_eq {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} (h : update I o c p = c) : Trivalent.posExt (toTrivalent I o c (iota x p q)) = {i : Assign V Δ E × W | Realize I p i.1 i.2} ∩ Trivalent.posExt (toTrivalent I o c q)

A definite whose restrictor is idle on the context is true and satt where its restrictor is true and its scope true and satt.

theorem Mandelkern2022.Formula.posExt_iota_eq_empty {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} (h : update I o c p ≠ c) : Trivalent.posExt (toTrivalent I o c (iota x p q)) = ∅

A definite whose restrictor is not idle on the context is satt nowhere, since the familiarity bound holds at all points of a context or at none (p. 1104).

@[simp]

theorem Mandelkern2022.Formula.toTrivalent_neg_neg {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} : toTrivalent I o c p.neg.neg = toTrivalent I o c p

Double negation changes neither dimension of a meaning (p. 1109).

The update calculus

theorem Mandelkern2022.Formula.update_conj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} : update I Order.asymmetric c (p.conj q) = update I Order.asymmetric (update I Order.asymmetric c p) q

A conjunction updates in sequence, the reason the paper's points carry over to sequences (fn. 20).

theorem Mandelkern2022.Formula.update_indef {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} : update I o c (indef x p q) = {i : Assign V Δ E × W | i ∈ update I o c (p.conj q) ∧ Realize I (indef x p q) i.1 i.2}

An indefinite updates as its body does, at the points where it is true.

theorem Mandelkern2022.Formula.update_indef_of_ne_bot {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} (hp : ∀ (g : Assign V Δ E) (w : W), Realize I p g w → g.ind x ≠ ⊥) : update I o c (indef x p q) = update I o c (p.conj q)

An indefinite whose restrictor values its variable updates as its body.

theorem Mandelkern2022.Formula.update_iota_of_update_eq {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} (h : update I Order.asymmetric c p = c) : update I Order.asymmetric c (iota x p q) = update I Order.asymmetric c (p.conj q)

A definite whose restrictor is idle on the context updates as the conjunction of its restrictor and scope.

theorem Mandelkern2022.Formula.update_iota_eq_empty {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p q : Formula L V Δ} {x : V} (h : update I o c p ≠ c) : update I o c (iota x p q) = ∅

A definite whose restrictor is not idle on the context empties it (p. 1104).

theorem Mandelkern2022.Formula.update_iota_top_eq_empty {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {q : Formula L V Δ} {x : V} (h : ∃ i ∈ c, i.1.ind x = ⊥) : update I o c (iota x (top x) q) = ∅

A pronoun whose variable is unvalued at some point of the context empties it.

@[simp]

theorem Mandelkern2022.Formula.update_neg_neg {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {p : Formula L V Δ} : update I o c p.neg.neg = update I o c p

One-place atoms

def Mandelkern2022.Formula.atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (R : L.Relations 1) (x : V) : Formula L V Δ

The one-place atom Rx.

Equations

• Mandelkern2022.Formula.atom₁ R x = Mandelkern2022.Formula.atom R ![x]

@[simp]

theorem Mandelkern2022.Formula.realize_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {x : V} {R : L.Relations 1} : Realize I (atom₁ R x) g w ↔ ∃ a ∈ extension I R w, g.ind x = ↑a

@[simp]

theorem Mandelkern2022.Formula.satt_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} {R : L.Relations 1} : Satt I o (atom₁ R x) c g w ↔ g.ind x ≠ ⊥

theorem Mandelkern2022.Formula.ne_bot_of_realize_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {x : V} {R : L.Relations 1} (h : Realize I (atom₁ R x) g w) : g.ind x ≠ ⊥

def Mandelkern2022.Formula.atom₂ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (R : L.Relations 2) (x y : V) : Formula L V Δ

The two-place atom R(x, y).

Equations

• Mandelkern2022.Formula.atom₂ R x y = Mandelkern2022.Formula.atom R ![x, y]

theorem Mandelkern2022.Formula.realize_atom₂ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {x : V} {R : L.Relations 2} {y : V} : Realize I (atom₂ R x y) g w ↔ ∃ (a : E) (b : E), g.ind x = ↑a ∧ g.ind y = ↑b ∧ FirstOrder.Language.Structure.RelMap R ![a, b]

theorem Mandelkern2022.Formula.satt_atom₂ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} {R : L.Relations 2} {y : V} : Satt I o (atom₂ R x y) c g w ↔ g.ind x ≠ ⊥ ∧ g.ind y ≠ ⊥

theorem Mandelkern2022.Formula.setOf_realize_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {R : L.Relations 1} : {i : Assign V Δ E × W | Realize I (atom₁ R x) i.1 i.2} = valuedIn x (extension I R)

theorem Mandelkern2022.Formula.posExt_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {x : V} {R : L.Relations 1} : Trivalent.posExt (toTrivalent I o c (atom₁ R x)) = valuedIn x (extension I R)

theorem Mandelkern2022.Formula.posExt_top {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {x : V} : Trivalent.posExt (toTrivalent I o c (top x)) = {i : Assign V Δ E × W | i.1.ind x ≠ ⊥}

theorem Mandelkern2022.Formula.update_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {x : V} {R : L.Relations 1} : update I o c (atom₁ R x) = c ∩ valuedIn x (extension I R)

theorem Mandelkern2022.Formula.update_atom₁_of_subset {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {x : V} {R : L.Relations 1} (h : c ⊆ valuedIn x (extension I R)) : update I o c (atom₁ R x) = c

An atom true throughout a context is idle on it.

theorem Mandelkern2022.Formula.update_top_of_subset {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {x : V} {S : W → Set E} (h : c ⊆ valuedIn x S) : update I o c (top x) = c

A pronoun restrictor is idle on a context that values its variable throughout.

Indefinites open files (§5.4)

theorem Mandelkern2022.realize_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {x : V} (F G : L.Relations 1) : Formula.Realize I (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)) g w ↔ (extension I F w ∩ extension I G w).Nonempty

theorem Mandelkern2022.satt_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} (F G : L.Relations 1) [Nonempty E] : Formula.Satt I Order.asymmetric (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)) c g w ↔ (extension I F w ∩ extension I G w).Nonempty → (g, w) ∈ valuedIn x (extension I F ⊓ extension I G)

The witness bound of ɜx(Fx, Gx) requires that, when some F is a G, x be one.

theorem Mandelkern2022.exists_satt_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} (F G : L.Relations 1) [Nonempty E] (c : Set (Assign V Δ E × W)) (w : W) : ∃ (g : Assign V Δ E), Formula.Satt I Order.asymmetric (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)) c g w

At every world some assignment satisfies the witness bound of ɜx(Fx, Gx).

theorem Mandelkern2022.posExt_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G : L.Relations 1) : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x))) = valuedIn x (extension I F ⊓ extension I G)

theorem Mandelkern2022.update_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G : L.Relations 1) : Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)) = c ∩ valuedIn x (extension I F ⊓ extension I G)

Updating with ɜx(Fx, Gx) keeps the points whose x is an F and a G (p. 1103).

theorem Mandelkern2022.not_univ_subset_support_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} (F G : L.Relations 1) (h : ∃ (w : W), (extension I F w ∩ extension I G w).Nonempty) : ¬Set.univ ⊆ Function.support (Formula.toTrivalent I Order.asymmetric Set.univ (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)))

The null context does not admit ɜx(Fx, Gx) in Stalnaker's sense once some world has an F that is G, since the point of the empty assignment there violates the witness bound. This is why updating keeps the points where a sentence is satt instead of requiring all of them to be (p. 1103).

theorem Mandelkern2022.posExt_iota_after_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric (Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x))) (Formula.iota x (Formula.atom₁ F x) (Formula.atom₁ H x))) = valuedIn x (extension I F ⊓ extension I H)

After ɜx(Fx, Gx), the definite ιx(Fx, Hx) is familiar, and true and satt where x is an F and an H (p. 1104).

theorem Mandelkern2022.posExt_iota_top_after_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric (Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x))) (Formula.iota x (Formula.top x) (Formula.atom₁ H x))) = valuedIn x (extension I H)

After ɜx(Fx, Gx), the pronoun ιx(⊤x, Hx) is familiar, and true and satt where x is an H (p. 1104).

theorem Mandelkern2022.satt_iota_top_after_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} (F G H : L.Relations 1) : Formula.Satt I Order.asymmetric (Formula.iota x (Formula.top x) (Formula.atom₁ H x)) (Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x))) g w

After ɜx(Fx, Gx), the bounds of the pronoun ιx(⊤x, Hx) hold at every point, its local context valuing x throughout.

theorem Mandelkern2022.update_indef_then_the {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Formula.update I Order.asymmetric (Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x))) (Formula.iota x (Formula.atom₁ F x) (Formula.atom₁ H x)) = c ∩ valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

There is a cat. The cat is tabby. keeps the points whose x is a cat that exists and is tabby (p. 1104).

theorem Mandelkern2022.update_indef_then_it {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Formula.update I Order.asymmetric (Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x))) (Formula.iota x (Formula.top x) (Formula.atom₁ H x)) = c ∩ valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

There is a cat. It is tabby. keeps the same points (p. 1104).

Negated indefinites (§5.5)

theorem Mandelkern2022.posExt_neg_indef_atom₁ {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G : L.Relations 1) [Nonempty E] : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)).neg) = {i : Assign V Δ E × W | extension I F i.2 ∩ extension I G i.2 = ∅}

A negated indefinite is true and satt where the negated existential is true, at the worlds with no F that is G (pp. 1106–1107).

theorem Mandelkern2022.update_null_neg_indef_then_it {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} (F G H : L.Relations 1) (h : ∃ (w : W), extension I F w ∩ extension I G w = ∅) : Formula.update I Order.asymmetric (Formula.update I Order.asymmetric Set.univ (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)).neg) (Formula.iota x (Formula.top x) (Formula.atom₁ H x)) = ∅

(19) We don't have a cat. # She is a tabby. Updating the null context with a negated indefinite and then a pronoun on its variable leaves no point, once some world has no F that is G (p. 1106).

Bound entailment (§5.6)

def Mandelkern2022.BoundEntails {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (o : Order) (p q : Formula L V Δ) : Prop

p bound-entails q when at every context p Strawson-entails q, with the bounds in the role of presuppositions, so that q is true wherever both are satt and p is true (p. 1108).

Equations

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

def Mandelkern2022.BoundEquiv {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (o : Order) (p q : Formula L V Δ) : Prop

Bound entailment in both directions.

Equations

• Mandelkern2022.BoundEquiv I o p q = AntisymmRel (Mandelkern2022.BoundEntails I o) p q

def Mandelkern2022.LogicallyEntails {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] (I : W → L.Structure E) (p q : Formula L V Δ) : Prop

p logically entails q when q is true wherever p is (p. 1108).

Equations

• Mandelkern2022.LogicallyEntails I p q = ∀ (g : Mandelkern2022.Assign V Δ E) (w : W), Mandelkern2022.Formula.Realize I p g w → Mandelkern2022.Formula.Realize I q g w

theorem Mandelkern2022.boundEntails_iff {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {p q : Formula L V Δ} : BoundEntails I o p q ↔ ∀ (c : Set (Assign V Δ E × W)) (g : Assign V Δ E) (w : W), Formula.Satt I o p c g w → Formula.Satt I o q c g w → Formula.Realize I p g w → Formula.Realize I q g w

theorem Mandelkern2022.BoundEntails.refl {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} (o : Order) (p : Formula L V Δ) : BoundEntails I o p p

instance Mandelkern2022.instReflFormulaBoundEntails {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} (o : Order) : Std.Refl (BoundEntails I o)

theorem Mandelkern2022.LogicallyEntails.boundEntails {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {p q : Formula L V Δ} (h : LogicallyEntails I p q) (o : Order) : BoundEntails I o p q

The bounded logic extends the logic (p. 1109).

Open scope (§5.6)

def Mandelkern2022.ex20a {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (x : V) (F G H : Formula L V Δ) : Formula L V Δ

(20-a) ɜx(F, G & H), some F is G and H.

Equations

• Mandelkern2022.ex20a x F G H = Mandelkern2022.Formula.indef x F (G.conj H)

def Mandelkern2022.ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (x : V) (F G H : Formula L V Δ) : Formula L V Δ

(20-b) ɜx(F, G) & ιx(F, H), some F is G, and the F is H.

Equations

• Mandelkern2022.ex20b x F G H = (Mandelkern2022.Formula.indef x F G).conj (Mandelkern2022.Formula.iota x F H)

def Mandelkern2022.ex20c {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (x : V) (F G H : Formula L V Δ) : Formula L V Δ

(20-c) ɜx(F, G) & ιx(⊤x, H), some F is G, and it is H.

Equations

• Mandelkern2022.ex20c x F G H = (Mandelkern2022.Formula.indef x F G).conj (Mandelkern2022.Formula.iota x (Mandelkern2022.Formula.top x) H)

theorem Mandelkern2022.boundEntails_ex20a_ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} : BoundEntails I Order.asymmetric (ex20a x F G H) (ex20b x F G H)

theorem Mandelkern2022.boundEntails_ex20c_ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} : BoundEntails I Order.asymmetric (ex20c x F G H) (ex20b x F G H)

theorem Mandelkern2022.boundEntails_ex20c_ex20a {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} : BoundEntails I Order.asymmetric (ex20c x F G H) (ex20a x F G H)

theorem Mandelkern2022.boundEntails_ex20b_ex20a {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} (hF : ∀ (g : Assign V Δ E) (w : W), Formula.Realize I F g w → g.ind x ≠ ⊥) : BoundEntails I Order.asymmetric (ex20b x F G H) (ex20a x F G H)

theorem Mandelkern2022.boundEntails_ex20b_ex20c {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} (hF : ∀ (g : Assign V Δ E) (w : W), Formula.Realize I F g w → g.ind x ≠ ⊥) : BoundEntails I Order.asymmetric (ex20b x F G H) (ex20c x F G H)

theorem Mandelkern2022.boundEntails_ex20a_ex20c {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} (hF : ∀ (g : Assign V Δ E) (w : W), Formula.Realize I F g w → g.ind x ≠ ⊥) : BoundEntails I Order.asymmetric (ex20a x F G H) (ex20c x F G H)

theorem Mandelkern2022.boundEquiv_ex20a_ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} (hF : ∀ (g : Assign V Δ E) (w : W), Formula.Realize I F g w → g.ind x ≠ ⊥) : BoundEquiv I Order.asymmetric (ex20a x F G H) (ex20b x F G H)

(20-a) and (20-b) are bound-equivalent when the restrictor's truth values x (p. 1108).

theorem Mandelkern2022.boundEquiv_ex20b_ex20c {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} (hF : ∀ (g : Assign V Δ E) (w : W), Formula.Realize I F g w → g.ind x ≠ ⊥) : BoundEquiv I Order.asymmetric (ex20b x F G H) (ex20c x F G H)

(20-b) and (20-c) are bound-equivalent when the restrictor's truth values x (p. 1108).

theorem Mandelkern2022.boundEquiv_ex20a_ex20c {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} {F G H : Formula L V Δ} (hF : ∀ (g : Assign V Δ E) (w : W), Formula.Realize I F g w → g.ind x ≠ ⊥) : BoundEquiv I Order.asymmetric (ex20a x F G H) (ex20c x F G H)

(20-a) and (20-c) are bound-equivalent when the restrictor's truth values x (p. 1108).

theorem Mandelkern2022.realize_ex20c_of_realize_ex20a {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} {F G H : Formula L V Δ} (hc : (g, w) ∈ c) (hs : Formula.Satt I Order.asymmetric (ex20a x F G H) c g w) (hs' : Formula.Satt I Order.asymmetric (ex20c x F G H) c g w) (hr : Formula.Realize I (ex20a x F G H) g w) : Formula.Realize I (ex20c x F G H) g w

At a point of its context, (20-a) bound-entails (20-c) for any formulae, since the pronoun's familiarity bound values x throughout the local context of the indefinite, which contains the point.

theorem Mandelkern2022.realize_ex20c_of_realize_ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {x : V} {F G H : Formula L V Δ} (hc : (g, w) ∈ c) (hs : Formula.Satt I Order.asymmetric (ex20b x F G H) c g w) (hs' : Formula.Satt I Order.asymmetric (ex20c x F G H) c g w) (hr : Formula.Realize I (ex20b x F G H) g w) : Formula.Realize I (ex20c x F G H) g w

At a point of its context, (20-b) bound-entails (20-c) for any formulae.

theorem Mandelkern2022.posExt_ex20a {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric c (ex20a x (Formula.atom₁ F x) (Formula.atom₁ G x) (Formula.atom₁ H x))) = valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

(20-a) is true and satt exactly where x is an F, a G and an H (p. 1108).

theorem Mandelkern2022.posExt_ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric c (ex20b x (Formula.atom₁ F x) (Formula.atom₁ G x) (Formula.atom₁ H x))) = valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

So is (20-b) (p. 1108).

theorem Mandelkern2022.posExt_ex20c {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric c (ex20c x (Formula.atom₁ F x) (Formula.atom₁ G x) (Formula.atom₁ H x))) = valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

So is (20-c) (p. 1108). Hence, as footnote 23 has it, any one of (20-a)–(20-c) is satt and true where all three are, and updating with any of them has the same effect.

theorem Mandelkern2022.realize_ex20a_and_not_realize_ex20b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {x : V} (F G H : L.Relations 1) (h : (extension I F w ∩ extension I G w ∩ extension I H w).Nonempty) {b : E} (hb : g.ind x = ↑b) (hH : b ∉ extension I H w) : Formula.Realize I (ex20a x (Formula.atom₁ F x) (Formula.atom₁ G x) (Formula.atom₁ H x)) g w ∧ ¬Formula.Realize I (ex20b x (Formula.atom₁ F x) (Formula.atom₁ G x) (Formula.atom₁ H x)) g w

The formulations of (20) are not logically equivalent, since at a point whose world has an F that is G and H but whose x is not an H, (20-a) is true and (20-b) is false (p. 1108).

Classicality (§5.7)

theorem Mandelkern2022.boundEquiv_neg_neg {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {p : Formula L V Δ} : BoundEquiv I o p.neg.neg p

¬¬p and p are logically, hence bound-, equivalent (p. 1109).

theorem Mandelkern2022.boundEquiv_disj_neg_conj {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {p q : Formula L V Δ} : BoundEquiv I o (p.neg.disj q) (p.neg.disj (p.conj q))

¬p ∨ q and ¬p ∨ (p & q) are logically, hence bound-, equivalent (p. 1109).

theorem Mandelkern2022.update_neg_neg_indef_then_the {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) : Formula.update I Order.asymmetric (Formula.update I Order.asymmetric c (Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)).neg.neg) (Formula.iota x (Formula.atom₁ F x) (Formula.atom₁ H x)) = c ∩ valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

A doubly negated indefinite licenses a subsequent definite as the indefinite does, as in It's not the case that Susie doesn't have a child. The child is at boarding school. (p. 1109).

theorem Mandelkern2022.posExt_bathroom {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {c : Set (Assign V Δ E × W)} {x : V} (F G H : L.Relations 1) [Nonempty E] : Trivalent.posExt (Formula.toTrivalent I Order.asymmetric c ((Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)).neg.disj (Formula.iota x (Formula.atom₁ F x) (Formula.atom₁ H x)))) = {i : Assign V Δ E × W | extension I F i.2 ∩ extension I G i.2 = ∅} ∪ valuedIn x (extension I F ⊓ extension I G ⊓ extension I H)

The bathroom disjunction Either Susie doesn't have a child, or the child is at boarding school is true and satt exactly where Susie is childless or x is Susie's child and at boarding school (p. 1109).

theorem Mandelkern2022.felicitous_bathroom {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {x : V} (F G H : L.Relations 1) [Nonempty W] [Nonempty E] : Formula.Felicitous I Order.asymmetric Set.univ ((Formula.indef x (Formula.atom₁ F x) (Formula.atom₁ G x)).neg.disj (Formula.iota x (Formula.top x) (Formula.atom₁ H x)))

(16-a) Either there isn't a bathroom, or it is upstairs, ¬ɜx(Fx, Gx) ∨ ιx(⊤x, Hx), is felicitous in the null context, since the pronoun's local context is the update with the doubly negated indefinite, which values x throughout (p. 1105).

Order (§5.5)

theorem Mandelkern2022.felicitous_ex15a_asymmetric {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} (S M C : L.Relations 1) (x : V) [Nonempty W] [Nonempty E] : Formula.Felicitous I Order.asymmetric Set.univ ((Formula.indef x (Formula.atom₁ M x) (Formula.atom₁ C x)).conj (Formula.iota x (Formula.top x) (Formula.atom₁ S x)))

With asymmetric local contexts (15-a) A man came in and he sat down, ɜx(Mx, Cx) & ιx(⊤x, Sx), is felicitous in the null context, since the pronoun's local context is the update with the indefinite, which values x throughout (p. 1105).

def Mandelkern2022.ex15b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (S M C : L.Relations 1) (x : V) : Formula L V Δ

(15-b) He sat down and a man came in, ιx(⊤x, Sx) & ɜx(Mx, Cx).

Equations

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

theorem Mandelkern2022.not_felicitous_ex15b_asymmetric {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} (S M C : L.Relations 1) (x : V) [Nonempty W] : ¬Formula.Felicitous I Order.asymmetric Set.univ (ex15b S M C x)

With asymmetric local contexts (15-b) is infelicitous in the null context, since its pronoun's familiarity bound fails at the points not valuing x (p. 1106).

theorem Mandelkern2022.satt_ex15b_symmetric {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} (S M C : L.Relations 1) (x : V) (hM : Formula.Realize I (Formula.atom₁ M x) g w) (hC : Formula.Realize I (Formula.atom₁ C x) g w) : Formula.Satt I Order.symmetric (ex15b S M C x) Set.univ g w

With symmetric local contexts (15-b) is satt in the null context wherever x is a man who came in, the pronoun's local context being the update with the indefinite (p. 1106).

Logically equivalent, differently updating (§2)

def Mandelkern2022.hasChild {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (Ch Sues : L.Relations 1) (x : V) : Formula L V Δ

Sue has a child, ɜx(child(x), Sue's(x)).

Equations

• Mandelkern2022.hasChild Ch Sues x = Mandelkern2022.Formula.indef x (Mandelkern2022.Formula.atom₁ Ch x) (Mandelkern2022.Formula.atom₁ Sues x)

def Mandelkern2022.isParent {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (Par : L.Relations 0) : Formula L V Δ

Sue is a parent, an atom with no variable.

Equations

• Mandelkern2022.isParent Par = Mandelkern2022.Formula.atom Par ![]

theorem Mandelkern2022.logicallyEquivalent_hasChild_isParent {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {Ch Sues : L.Relations 1} {Par : L.Relations 0} {x : V} (hPar : ∀ (w : W), FirstOrder.Language.Structure.RelMap Par ![] ↔ ∃ (b : E), FirstOrder.Language.Structure.RelMap Ch ![b] ∧ FirstOrder.Language.Structure.RelMap Sues ![b]) : LogicallyEntails I (hasChild Ch Sues x) (isParent Par) ∧ LogicallyEntails I (isParent Par) (hasChild Ch Sues x)

Where being a parent is having a child, Sue has a child and Sue is a parent are logically equivalent ((2), p. 1093).

theorem Mandelkern2022.update_isParent_then_it {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {B : L.Relations 1} {Par : L.Relations 0} {x : V} (c : Set (Assign V Δ E × W)) (h : ∃ i ∈ Formula.update I Order.asymmetric c (isParent Par), i.1.ind x = ⊥) : Formula.update I Order.asymmetric (Formula.update I Order.asymmetric c (isParent Par)) (Formula.iota x (Formula.top x) (Formula.atom₁ B x)) = ∅

But only the indefinite licenses a pronoun. After Sue is a parent, she is … empties any context with a point not valuing x, while after Sue has a child it keeps the points where x is Sue's child ((2), (9), pp. 1093 and 1104).

Quantifiers (§5.8)

def Mandelkern2022.ex21b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (Pa : L.Relations 1) (Lv : L.Relations 2) (x y : V) (δ : Δ) (Q : Quantifier.NumberTree) : Formula L V Δ

(21-b) Every parent loves them, Q x^δ (parent(x), ιy(⊤y, loves(x, y))).

Equations

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

def Mandelkern2022.hasChildOf {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (Ch : L.Relations 1) (Of : L.Relations 2) (x y : V) : Formula L V Δ

Has a child, ɜy(child(y), of(y, x)).

Equations

• Mandelkern2022.hasChildOf Ch Of x y = Mandelkern2022.Formula.indef y (Mandelkern2022.Formula.atom₁ Ch y) (Mandelkern2022.Formula.atom₂ Of y x)

def Mandelkern2022.ex22b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} (Ch : L.Relations 1) (Of Lv : L.Relations 2) (x y : V) (δ : Δ) (Q : Quantifier.NumberTree) : Formula L V Δ

(22-b) Everyone who has a child loves them, Q x^δ (ɜy(child(y), of(y, x)), ιy(⊤y, loves(x, y))).

Equations

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

theorem Mandelkern2022.familiar_of_satt_ex21b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {Pa : L.Relations 1} {Lv : L.Relations 2} {x y : V} {δ : Δ} {Q : Quantifier.NumberTree} (a : E) (h : Formula.Satt I o (ex21b Pa Lv x y δ Q) c g w) (j : Assign V Δ E × W) : j ∈ c → Formula.Realize I (Formula.atom₁ Pa x) j.1 j.2 → j.1.ind y ≠ ⊥

(21-b) is satt only if y is valued at every point of the context where x is a parent, since the pronoun finds no witness in the restrictor (p. 1111).

theorem Mandelkern2022.not_felicitous_ex21b {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {Pa : L.Relations 1} {Lv : L.Relations 2} {x y : V} {δ : Δ} {Q : Quantifier.NumberTree} (hxy : x ≠ y) (hP : ∃ (w : W) (a : E), FirstOrder.Language.Structure.RelMap Pa ![a]) : ¬Formula.Felicitous I o Set.univ (ex21b Pa Lv x y δ Q)

So in the null context (21-b) is infelicitous once some world has a parent (p. 1111).

theorem Mandelkern2022.realize_ex21b_iff_of_familiar {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {Pa : L.Relations 1} {Lv : L.Relations 2} {x y : V} {δ : Δ} {Q : Quantifier.NumberTree} (hxy : x ≠ y) (hs : Formula.Satt I o (ex21b Pa Lv x y δ Q) c g w) (hy : Familiar c y) : Formula.Realize I (ex21b Pa Lv x y δ Q) g w ↔ Q.toGQ (fun (a : E) => FirstOrder.Language.Structure.RelMap Pa ![a]) fun (a : E) => FirstOrder.Language.Structure.RelMap Pa ![a] ∧ ∃ (b : E), g.ind y = ↑b ∧ FirstOrder.Language.Structure.RelMap Lv ![a, b]

Where y is familiar the pairing must keep it fixed, so (21-b) has only the reading on which every parent loves one particular individual (p. 1111).

theorem Mandelkern2022.satt_hasChildOf_iff {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {Ch : L.Relations 1} {Of : L.Relations 2} {x y : V} [Nonempty E] : Formula.Satt I o (hasChildOf Ch Of x y) c g w ↔ Formula.Realize I (hasChildOf Ch Of x y) g w → Formula.Realize I (Formula.atom₁ Ch y) g w ∧ Formula.Realize I (Formula.atom₂ Of y x) g w

theorem Mandelkern2022.satt_ex22b_iff {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {o : Order} {c : Set (Assign V Δ E × W)} {g : Assign V Δ E} {w : W} {Ch : L.Relations 1} {Of Lv : L.Relations 2} {x y : V} {δ : Δ} {Q : Quantifier.NumberTree} [Nonempty E] : Formula.Satt I o (ex22b Ch Of Lv x y δ Q) c g w ↔ ∀ (a : E), (Formula.Realize I (hasChildOf Ch Of x y) (g.pair δ x a) w → Formula.Realize I (Formula.atom₁ Ch y) (g.pair δ x a) w ∧ Formula.Realize I (Formula.atom₂ Of y x) (g.pair δ x a) w) ∧ ∀ (z : V), Familiar c z → g.dom δ a z = g.ind z

(22-b) is satt, even with y novel, exactly where its pairing gives every individual with a child one of its children and keeps the familiar variables fixed (p. 1110).

theorem Mandelkern2022.realize_ex22b_iff {L : FirstOrder.Language} {V : Type u_1} {Δ : Type u_2} {W : Type u_3} {E : Type u_4} [DecidableEq V] {I : W → L.Structure E} {g : Assign V Δ E} {w : W} {Ch : L.Relations 1} {Of Lv : L.Relations 2} {x y : V} {δ : Δ} {Q : Quantifier.NumberTree} (hxy : x ≠ y) : Formula.Realize I (ex22b Ch Of Lv x y δ Q) g w ↔ Q.toGQ (fun (a : E) => ∃ (b : E), FirstOrder.Language.Structure.RelMap Ch ![b] ∧ FirstOrder.Language.Structure.RelMap Of ![b, a]) fun (a : E) => (∃ (b : E), FirstOrder.Language.Structure.RelMap Ch ![b] ∧ FirstOrder.Language.Structure.RelMap Of ![b, a]) ∧ ∃ (b : E), g.dom δ a y = ↑b ∧ FirstOrder.Language.Structure.RelMap Lv ![a, b]

Where (22-b) is satt it is true exactly when the number tree relates the individuals with a child to those who love the child paired with them, which is the covarying reading (p. 1111).

Footnote 20

@[reducible, inline]

abbrev Mandelkern2022.L₂ : FirstOrder.Language

A language with two relation symbols of each arity, false and true.

Equations

• Mandelkern2022.L₂ = { Functions := fun (x : ℕ) => Empty, Relations := fun (x : ℕ) => Bool }

@[reducible]

def Mandelkern2022.I₂ (w : Bool) : L₂.Structure Unit

Two worlds over a one-element domain, at both of which the relation false is empty, while the relation true is full at world true and empty at world false.

Equations

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

@[simp]

theorem Mandelkern2022.relMap_I₂ {w : Bool} {n : ℕ} {r : L₂.Relations n} {es : Fin n → Unit} : FirstOrder.Language.Structure.RelMap r es ↔ r = true ∧ w = true

def Mandelkern2022.bearsNothing (r : Bool) : Formula L₂ ℕ Empty

The formula ¬ɜy(⊤y, r(x, y)) with x = 0 and y = 1, saying that x bears r to nothing; it is free in x, yet true when x is unvalued.

Equations

• Mandelkern2022.bearsNothing r = (Mandelkern2022.Formula.indef 1 (Mandelkern2022.Formula.top 1) (Mandelkern2022.Formula.atom (have this := r; this) ![0, 1])).neg

theorem Mandelkern2022.realize_bearsNothing_false (g : Assign ℕ Empty Unit) (w : Bool) : Formula.Realize I₂ (bearsNothing false) g w

theorem Mandelkern2022.realize_bearsNothing_bot (r w : Bool) : Formula.Realize I₂ (bearsNothing r) ⊥ w

theorem Mandelkern2022.realize_bearsNothing_true_iff (a : Unit) (w : Bool) : Formula.Realize I₂ (bearsNothing true) (⊥.update 0 a) w ↔ w = false

theorem Mandelkern2022.satt_bearsNothing_false (c : Set (Assign ℕ Empty Unit × Bool)) (g : Assign ℕ Empty Unit) (w : Bool) : Formula.Satt I₂ Order.asymmetric (bearsNothing false) c g w

theorem Mandelkern2022.satt_bearsNothing_bot (r : Bool) (c : Set (Assign ℕ Empty Unit × Bool)) (w : Bool) : Formula.Satt I₂ Order.asymmetric (bearsNothing r) c ⊥ w

theorem Mandelkern2022.holds_ex20b (c : Set (Assign ℕ Empty Unit × Bool)) (w : Bool) : Formula.Satt I₂ Order.asymmetric (ex20b 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) c ⊥ w ∧ Formula.Realize I₂ (ex20b 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) ⊥ w

(20-b) is satt and true at every context and the empty assignment.

theorem Mandelkern2022.realize_ex20a_iff (w : Bool) : Formula.Realize I₂ (ex20a 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) ⊥ w ↔ w = false

theorem Mandelkern2022.satt_ex20a (c : Set (Assign ℕ Empty Unit × Bool)) (w : Bool) : Formula.Satt I₂ Order.asymmetric (ex20a 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) c ⊥ w

theorem Mandelkern2022.satt_ex20c (w : Bool) : Formula.Satt I₂ Order.asymmetric (ex20c 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) ∅ ⊥ w

(20-c) is satt but false at the empty context and assignment, where its pronoun's variable is unvalued.

theorem Mandelkern2022.not_realize_ex20c (w : Bool) : ¬Formula.Realize I₂ (ex20c 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) ⊥ w

theorem Mandelkern2022.not_boundEntails_ex20b_ex20a : ¬BoundEntails I₂ Order.asymmetric (ex20b 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) (ex20a 0 (bearsNothing false) (bearsNothing false) (bearsNothing true))

(20-b) does not bound-entail (20-a) when the restrictor is ¬ɜy(⊤y, R(x, y)), since at the null context, the empty assignment, and a world where something bears S to something, (20-b) is satt and true and (20-a) satt and false.

theorem Mandelkern2022.not_boundEntails_ex20a_ex20c : ¬BoundEntails I₂ Order.asymmetric (ex20a 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) (ex20c 0 (bearsNothing false) (bearsNothing false) (bearsNothing true))

(20-a) does not bound-entail (20-c) for the same restrictor. The refuting index is a point outside its context, the empty one; at points of the context the entailment holds (realize_ex20c_of_realize_ex20a).

theorem Mandelkern2022.not_boundEntails_ex20b_ex20c : ¬BoundEntails I₂ Order.asymmetric (ex20b 0 (bearsNothing false) (bearsNothing false) (bearsNothing true)) (ex20c 0 (bearsNothing false) (bearsNothing false) (bearsNothing true))

Nor does (20-b) bound-entail (20-c), again at a point outside the empty context (realize_ex20c_of_realize_ex20b).