Intensional models of PIP

This file defines the models of PIP whose atoms are worlds and entities. A world is the singleton plurality of its atom, and a family of world-relative relations on atoms is lifted distributively to relation symbols: a symbol holds of a world and nonempty pluralities iff it holds at that world of every tuple of their members, and it holds of nothing whose world argument is not a world.

Main definitions

• Atom, world — worlds and entities as atoms; a world as a plurality.
• Model.intensional — the distributive lifting of world-relative relations.

Main statements

• Model.intensional_apply₁, Model.intensional_apply₂ — the lifting on one and two arguments.
• Term.realize_sigma_world_eq, exists_mem_distributive_iff, exists_mem_singleton_iff, exists_singleton_iff, exists_distributive_iff — the values of summations over worlds and over entities from characterizations of their bodies.
• exists_eq_singleton_iff — a plurality of entities is a singleton iff exactly one entity satisfies its description.

References

• [keshet-abney-2024]
• [abney-keshet-2025]

@[reducible, inline]

abbrev PIP.Atom (W : Type u_2) (E : Type u_3) : Type (max u_2 u_3)

The atoms of an intensional model: worlds and entities.

Equations

• PIP.Atom W E = (W ⊕ E)

def PIP.world {W : Type u_2} {E : Type u_3} (w : W) : Set (Atom W E)

A world as a singleton plurality.

Equations

• PIP.world w = {Sum.inl w}

theorem PIP.world_inj {W : Type u_2} {E : Type u_3} {w w' : W} : world w = world w' ↔ w = w'

def PIP.Model.intensional {P : ℕ → Type w} {W : Type u_2} {E : Type u_3} (rel : {n : ℕ} → P n → W → (Fin n → Atom W E) → Prop) : Model P (Atom W E)

The intensional model of a family of relations on atoms at each world: a relation symbol holds of a world and nonempty pluralities iff it holds at that world of every tuple of their members, and of nothing whose world argument is not a world.

Equations

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

theorem PIP.Model.intensional_apply₁ {P : ℕ → Type w} {W : Type u_2} {E : Type u_3} {rel : {n : ℕ} → P n → W → (Fin n → Atom W E) → Prop} (r : P 1) (Wp X : Set (Atom W E)) : (intensional fun {n : ℕ} => rel).I r Wp ![X] ↔ ∃ (w : W), Wp = world w ∧ X.Nonempty ∧ ∀ a ∈ X, rel r w ![a]

theorem PIP.Model.intensional_apply₂ {P : ℕ → Type w} {W : Type u_2} {E : Type u_3} {rel : {n : ℕ} → P n → W → (Fin n → Atom W E) → Prop} (r : P 2) (Wp X Y : Set (Atom W E)) : (intensional fun {n : ℕ} => rel).I r Wp ![X, Y] ↔ ∃ (w : W), Wp = world w ∧ X.Nonempty ∧ Y.Nonempty ∧ ∀ a ∈ X, ∀ b ∈ Y, rel r w ![a, b]

theorem PIP.Term.realize_sigma_world_eq {V : Type u} {L : Type v} {P : ℕ → Type w} {W : Type u_2} {E : Type u_3} [DecidableEq V] (M : Model P (Atom W E)) (g : V → Set (Atom W E)) {x y : V} (hxy : y ≠ x) {φ : Formula V L P} {B : Set (Atom W E) → W → Prop} (hφ : ∀ (g' : V → Set (Atom W E)), Set.EqOn g' g {z : V | z ∉ Expr.locals φ ∧ z ≠ x} → (Formula.Realize M g' φ ↔ ∃ (w : W), g' x = world w ∧ B (g' y) w)) (hy : y ∈ Expr.locals φ) : realize M g (Expr.sigma x φ) = {a : W ⊕ E | ∃ (w : W), a = Sum.inl w ∧ ∃ (X : Set (Atom W E)), B X w}

The value of a summation over a world variable whose body, on the assignments agreeing outside the summation variable and its locals, holds iff the variable is a world standing in the relation B to the value of the local y: the worlds so related to some plurality.

theorem PIP.exists_mem_distributive_iff {W : Type u_2} {E : Type u_3} {a : Atom W E} {Q : E → Prop} : (∃ (X : Set (Atom W E)), a ∈ X ∧ X.Nonempty ∧ ∀ b ∈ X, ∃ (e : E), b = Sum.inr e ∧ Q e) ↔ ∃ (e : E), a = Sum.inr e ∧ Q e

theorem PIP.exists_mem_singleton_iff {W : Type u_2} {E : Type u_3} {a : Atom W E} {Q : E → Prop} : (∃ (X : Set (Atom W E)), a ∈ X ∧ ∃ (e : E), X = {Sum.inr e} ∧ Q e) ↔ ∃ (e : E), a = Sum.inr e ∧ Q e

theorem PIP.exists_singleton_iff {W : Type u_2} {E : Type u_3} {Q : E → Prop} : (∃ (X : Set (Atom W E)) (e : E), X = {Sum.inr e} ∧ Q e) ↔ ∃ (e : E), Q e

theorem PIP.exists_distributive_iff {W : Type u_2} {E : Type u_3} {Q : E → Prop} : (∃ (X : Set (Atom W E)), X.Nonempty ∧ ∀ b ∈ X, ∃ (e : E), b = Sum.inr e ∧ Q e) ↔ ∃ (e : E), Q e

theorem PIP.exists_eq_singleton_iff {W : Type u_2} {E : Type u_3} (Q : E → Prop) : (∃ (a : Atom W E), {x : W ⊕ E | ∃ (e : E), x = Sum.inr e ∧ Q e} = {a}) ↔ ∃! e : E, Q e

A plurality of entities is a singleton iff exactly one entity satisfies its description.