Semantics of PIP

This file defines the value of a term and the truth of a formula of PIP in a model, relative to an assignment of pluralities to variables. Pluralities are sets of atoms. A variable denotes its assignment; set abstraction ⋃{x : φ} and summation Σxφ denote the union of the values of x over the assignments that agree with the current one outside the bound variables (for summation, also outside the local variables of φ) and satisfy φ. Presuppositions and label definitions do not affect truth, and an unexpanded label is false. A discourse φ₁, …, φₙ means Σw(φ₁ ∧ … ∧ φₙ) and is true iff that plurality of worlds is nonempty.

Both kinds of expression are realized by one recursion, Expr.Realize, as a relation to a point: an atom for a term, nothing for a formula.

Main definitions

• Model — the interpretation of relation symbols over pluralities.
• Expr.Realize, Term.realize, Formula.Realize — value and truth relative to a model and an assignment.

Main statements

• Formula.realize_atom, Formula.realize_conj, … — the clauses of truth, as simp lemmas; Formula.realize_disj, …, Formula.realize_some — the derived connectives.
• Formula.realize_exists_iff_abs_nonempty — ∃xφ is true iff ⋃{x : φ} is nonempty, when φ is false of the null plurality.
• Term.realize_sigma_eq — the value of a summation from a characterization of its body.
• Expr.realize_elim — the PIP constructs are eliminable: the translation preserves values and truth.

References

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

structure PIP.Model (P : ℕ → Type w) (α : Type u) : Type (max u w)

A model: pluralities are sets of atoms α, and each n-ary relation symbol is interpreted over a world plurality and a tuple of n pluralities.

• I {n : ℕ} : P n → Set α → (Fin n → Set α) → Prop

  The interpretation of relation symbols.

def PIP.Kind.Point (α : Type u) : Kind → Type u

The point at which an expression of a kind is realized: an atom, whose membership in a term's value is at stake, or nothing for a formula.

Equations

• PIP.Kind.Point α PIP.Kind.term = α
• PIP.Kind.Point α PIP.Kind.formula = PUnit.{?u.2 + 1}

def PIP.Expr.Realize {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) {k : Kind} : Expr V L P k → Kind.Point α k → Prop

Realization: membership of an atom in the value of a term, and truth of a formula. A variable denotes its assignment, abstraction and summation the union of the values of the bound variable over assignments agreeing outside the bound variables; a formula is true classically, with presuppositions and label definitions transparent and an unexpanded label false.

Equations

• PIP.Expr.Realize M g (PIP.Expr.var x_3) a = (a ∈ g x_3)
• PIP.Expr.Realize M g (PIP.Expr.bvar x_3) a = (a ∈ g x_3)
• PIP.Expr.Realize M g (PIP.Expr.abs x_3 φ) a = ∃ (g' : V → Set α), Set.EqOn g' g {x_3}ᶜ ∧ a ∈ g' x_3 ∧ PIP.Expr.Realize M g' φ PUnit.unit
• PIP.Expr.Realize M g (PIP.Expr.sigma x_3 φ) a = ∃ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ φ.locals ∧ y ≠ x_3} ∧ a ∈ g' x_3 ∧ PIP.Expr.Realize M g' φ PUnit.unit
• PIP.Expr.Realize M g (s.inter t) a = (PIP.Expr.Realize M g s a ∧ PIP.Expr.Realize M g t a)
• PIP.Expr.Realize M g PIP.Expr.empty x_3 = False
• PIP.Expr.Realize M g PIP.Expr.top x_3 = True
• PIP.Expr.Realize M g (PIP.Expr.atom r w ts) x_3 = M.I r {a : α | PIP.Expr.Realize M g w a} fun (i : Fin n) => {a : α | PIP.Expr.Realize M g (ts i) a}
• PIP.Expr.Realize M g (s.eq t) x_3 = ({a : PIP.Kind.Point α PIP.Kind.term | PIP.Expr.Realize M g s a} = {a : PIP.Kind.Point α PIP.Kind.term | PIP.Expr.Realize M g t a})
• PIP.Expr.Realize M g (s.subset t) x_3 = ({a : PIP.Kind.Point α PIP.Kind.term | PIP.Expr.Realize M g s a} ⊆ {a : PIP.Kind.Point α PIP.Kind.term | PIP.Expr.Realize M g t a})
• PIP.Expr.Realize M g (s.mem t) x_3 = ∃ (a : PIP.Kind.Point α PIP.Kind.term), {b : PIP.Kind.Point α PIP.Kind.term | PIP.Expr.Realize M g s b} = {a} ∧ PIP.Expr.Realize M g t a
• PIP.Expr.Realize M g t.sg x_3 = ∃ (a : PIP.Kind.Point α PIP.Kind.term), {b : PIP.Kind.Point α PIP.Kind.term | PIP.Expr.Realize M g t b} = {a}
• PIP.Expr.Realize M g t.pl x_3 = ∃ (a : PIP.Kind.Point α PIP.Kind.term) (b : PIP.Kind.Point α PIP.Kind.term), a ≠ b ∧ PIP.Expr.Realize M g t a ∧ PIP.Expr.Realize M g t b
• PIP.Expr.Realize M g φ.neg x_3 = ¬PIP.Expr.Realize M g φ PUnit.unit
• PIP.Expr.Realize M g (φ.conj ψ) x_3 = (PIP.Expr.Realize M g φ PUnit.unit ∧ PIP.Expr.Realize M g ψ PUnit.unit)
• PIP.Expr.Realize M g (PIP.Expr.exists_ x_3 φ) x_4 = ∃ (g' : V → Set α), Set.EqOn g' g {x_3}ᶜ ∧ PIP.Expr.Realize M g' φ PUnit.unit
• PIP.Expr.Realize M g (PIP.Expr.labelDef X φ) x_3 = True
• PIP.Expr.Realize M g (PIP.Expr.label X) x_3 = False
• PIP.Expr.Realize M g (e.presup ψ) x✝ = PIP.Expr.Realize M g e x✝

def PIP.Term.realize {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (t : Term V L P) : Set α

The value of a term.

Equations

• PIP.Term.realize M g t = {a : α | PIP.Expr.Realize M g t a}

def PIP.Formula.Realize {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ : Formula V L P) : Prop

Truth of a formula.

Equations

• PIP.Formula.Realize M g φ = PIP.Expr.Realize M g φ PUnit.unit

@[simp]

theorem PIP.Term.mem_realize {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) {t : Term V L P} {a : α} : a ∈ realize M g t ↔ Expr.Realize M g t a

@[simp]

theorem PIP.Term.realize_var {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) : realize M g (Expr.var x) = g x

@[simp]

theorem PIP.Term.realize_bvar {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) : realize M g (Expr.bvar x) = g x

@[simp]

theorem PIP.Term.realize_inter {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (s t : Term V L P) : realize M g (Expr.inter s t) = realize M g s ∩ realize M g t

@[simp]

theorem PIP.Term.realize_empty {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) : realize M g Expr.empty = ∅

@[simp]

theorem PIP.Term.realize_presup {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (t : Term V L P) (ψ : Formula V L P) : realize M g (Expr.presup t ψ) = realize M g t

theorem PIP.Term.mem_realize_abs {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) (φ : Formula V L P) (a : α) : a ∈ realize M g (Expr.abs x φ) ↔ ∃ (g' : V → Set α), Set.EqOn g' g {x}ᶜ ∧ a ∈ g' x ∧ Formula.Realize M g' φ

theorem PIP.Term.mem_realize_sigma {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) (φ : Formula V L P) (a : α) : a ∈ realize M g (Expr.sigma x φ) ↔ ∃ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ Expr.locals φ ∧ y ≠ x} ∧ a ∈ g' x ∧ Formula.Realize M g' φ

@[simp]

theorem PIP.Formula.realize_top {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) : Realize M g Expr.top ↔ True

@[simp]

theorem PIP.Formula.realize_atom {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) {n : ℕ} (r : P n) (w : Term V L P) (ts : Fin n → Term V L P) : Realize M g (Expr.atom r w ts) ↔ M.I r (Term.realize M g w) fun (i : Fin n) => Term.realize M g (ts i)

@[simp]

theorem PIP.Formula.realize_eq {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (s t : Term V L P) : Realize M g (Expr.eq s t) ↔ Term.realize M g s = Term.realize M g t

@[simp]

theorem PIP.Formula.realize_subset {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (s t : Term V L P) : Realize M g (Expr.subset s t) ↔ Term.realize M g s ⊆ Term.realize M g t

@[simp]

theorem PIP.Formula.realize_mem {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (s t : Term V L P) : Realize M g (Expr.mem s t) ↔ ∃ (a : α), Term.realize M g s = {a} ∧ a ∈ Term.realize M g t

@[simp]

theorem PIP.Formula.realize_sg {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (t : Term V L P) : Realize M g (Expr.sg t) ↔ ∃ (a : α), Term.realize M g t = {a}

@[simp]

theorem PIP.Formula.realize_pl {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (t : Term V L P) : Realize M g (Expr.pl t) ↔ ∃ (a : α) (b : α), a ≠ b ∧ a ∈ Term.realize M g t ∧ b ∈ Term.realize M g t

@[simp]

theorem PIP.Formula.realize_neg {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ : Formula V L P) : Realize M g (Expr.neg φ) ↔ ¬Realize M g φ

@[simp]

theorem PIP.Formula.realize_conj {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ ψ : Formula V L P) : Realize M g (Expr.conj φ ψ) ↔ Realize M g φ ∧ Realize M g ψ

theorem PIP.Formula.realize_exists {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) (φ : Formula V L P) : Realize M g (Expr.exists_ x φ) ↔ ∃ (g' : V → Set α), Set.EqOn g' g {x}ᶜ ∧ Realize M g' φ

@[simp]

theorem PIP.Formula.realize_presup {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ ψ : Formula V L P) : Realize M g (Expr.presup φ ψ) ↔ Realize M g φ

@[simp]

theorem PIP.Formula.realize_labelDef {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (X : L) (φ : Formula V L P) : Realize M g (Expr.labelDef X φ) ↔ True

@[simp]

theorem PIP.Formula.realize_label {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (X : L) : Realize M g (Expr.label X) ↔ False

Derived clauses

theorem PIP.Formula.realize_disj {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ ψ : Formula V L P) : Realize M g (φ.disj ψ) ↔ Realize M g φ ∨ Realize M g ψ

theorem PIP.Formula.realize_impl {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ ψ : Formula V L P) : Realize M g (φ.impl ψ) ↔ Realize M g φ → Realize M g ψ

theorem PIP.Formula.realize_iff {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ ψ : Formula V L P) : Realize M g (φ.iff_ ψ) ↔ (Realize M g φ ↔ Realize M g ψ)

theorem PIP.Formula.realize_forall {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) (φ : Formula V L P) : Realize M g (forall_ x φ) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {x}ᶜ → Realize M g' φ

theorem PIP.Formula.realize_some {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (s t : Term V L P) : Realize M g (some_ s t) ↔ (Term.realize M g s ∩ Term.realize M g t).Nonempty

theorem PIP.Formula.realize_exists_iff_abs_nonempty {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (x : V) (φ : Formula V L P) (h : ∀ (g' : V → Set α), g' x = ∅ → ¬Realize M g' φ) : Realize M g (Expr.exists_ x φ) ↔ (Term.realize M g (Expr.abs x φ)).Nonempty

∃xφ is true iff ⋃{x : φ} is nonempty, provided φ is false when x is the null plurality — the standing assumption that predicates are false of the null individual.

theorem PIP.Term.realize_sigma_eq {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) {x : V} {φ : Formula V L P} {B : Set α → Prop} (hφ : ∀ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ Expr.locals φ ∧ y ≠ x} → (Formula.Realize M g' φ ↔ B (g' x))) : realize M g (Expr.sigma x φ) = {a : α | ∃ (X : Set α), a ∈ X ∧ B X}

The value of a summation whose body, on the assignments agreeing outside the summation variable and its locals, depends on the summation variable's value alone: the union of the pluralities satisfying that condition.

Eliminability

theorem PIP.Formula.realize_closeList {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (xs : List V) (φ : Formula V L P) (g : V → Set α) : Realize M g (closeList xs φ) ↔ ∃ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ xs} ∧ Realize M g' φ

theorem PIP.Expr.realize_elim {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) {k : Kind} (e : Expr V L P k) (g : V → Set α) (a : Kind.Point α k) : Realize M g e.elim a ↔ Realize M g e a

The PIP constructs are eliminable: the translation preserves values and truth.

theorem PIP.Term.realize_elim {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (t : Term V L P) : realize M g (Expr.elim t) = realize M g t

theorem PIP.Formula.realize_elim {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (φ : Formula V L P) : Realize M g (Expr.elim φ) ↔ Realize M g φ