Felicity of PIP formulas

This file defines the felicity operator F on the terms and formulas of PIP. A presupposition φ|ψ is felicitous iff φ and ψ are and ψ is true; a conjunction φ ∧ ψ iff φ is and, whenever φ is true, ψ is; a quantifier, abstraction or summation iff its body is for every value of the variables it binds; the other connectives and relations iff their parts are. Felicity is independent of truth. The PIP-value of a formula records its truth, its felicity, its local variables and its label definitions, and two formulas are intersubstitutable iff they have the same PIP-value in every model under every assignment.

Main definitions

• Expr.Felicitous — the felicity operator F.
• Value, Formula.value — the PIP-value of a formula.

Main statements

• Formula.felicitous_atom, Formula.felicitous_conj, … — the clauses of felicity, as simp lemmas; Formula.felicitous_disj, …, Formula.felicitous_some — the derived connectives.
• Expr.felicitous_of_presupFree — every infelicity traces to a presupposition.
• Term.felicitous_sigma_conj_of_felicitous — felicity of a discourse extended by a sentence reduces to the earlier discourse strictly implying the new sentence's felicity.

References

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

def PIP.Expr.Felicitous {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 → Prop

Felicity: e|ψ needs e and ψ felicitous and ψ true; abstraction, summation and quantification need their bodies felicitous for every value; a conjunction needs its first conjunct felicitous and, if it is true, its second — the first conjunct may satisfy the presuppositions of the second.

Equations

• PIP.Expr.Felicitous M g (PIP.Expr.var x_2) = True
• PIP.Expr.Felicitous M g (PIP.Expr.bvar x_2) = True
• PIP.Expr.Felicitous M g (PIP.Expr.abs x_2 φ) = ∀ (g' : V → Set α), Set.EqOn g' g {x_2}ᶜ → PIP.Expr.Felicitous M g' φ
• PIP.Expr.Felicitous M g (PIP.Expr.sigma x_2 φ) = ∀ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ φ.locals ∧ y ≠ x_2} → PIP.Expr.Felicitous M g' φ
• PIP.Expr.Felicitous M g (s.inter t) = (PIP.Expr.Felicitous M g s ∧ PIP.Expr.Felicitous M g t)
• PIP.Expr.Felicitous M g PIP.Expr.empty = True
• PIP.Expr.Felicitous M g PIP.Expr.top = True
• PIP.Expr.Felicitous M g (PIP.Expr.atom r w ts) = (PIP.Expr.Felicitous M g w ∧ ∀ (i : Fin n), PIP.Expr.Felicitous M g (ts i))
• PIP.Expr.Felicitous M g (s.eq t) = (PIP.Expr.Felicitous M g s ∧ PIP.Expr.Felicitous M g t)
• PIP.Expr.Felicitous M g (s.subset t) = (PIP.Expr.Felicitous M g s ∧ PIP.Expr.Felicitous M g t)
• PIP.Expr.Felicitous M g (s.mem t) = (PIP.Expr.Felicitous M g s ∧ PIP.Expr.Felicitous M g t)
• PIP.Expr.Felicitous M g t.sg = PIP.Expr.Felicitous M g t
• PIP.Expr.Felicitous M g t.pl = PIP.Expr.Felicitous M g t
• PIP.Expr.Felicitous M g φ.neg = PIP.Expr.Felicitous M g φ
• PIP.Expr.Felicitous M g (φ.conj ψ) = (PIP.Expr.Felicitous M g φ ∧ (PIP.Formula.Realize M g φ → PIP.Expr.Felicitous M g ψ))
• PIP.Expr.Felicitous M g (PIP.Expr.exists_ x_2 φ) = ∀ (g' : V → Set α), Set.EqOn g' g {x_2}ᶜ → PIP.Expr.Felicitous M g' φ
• PIP.Expr.Felicitous M g (PIP.Expr.labelDef X φ) = True
• PIP.Expr.Felicitous M g (PIP.Expr.label X) = False
• PIP.Expr.Felicitous M g (e.presup ψ) = (PIP.Expr.Felicitous M g e ∧ PIP.Expr.Felicitous M g ψ ∧ PIP.Formula.Realize M g ψ)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem PIP.Term.felicitous_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) : Expr.Felicitous M g (Expr.inter s t) ↔ Expr.Felicitous M g s ∧ Expr.Felicitous M g t

@[simp]

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

theorem PIP.Term.felicitous_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) : Expr.Felicitous M g (Expr.abs x φ) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {x}ᶜ → Expr.Felicitous M g' φ

theorem PIP.Term.felicitous_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) : Expr.Felicitous M g (Expr.sigma x φ) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ Expr.locals φ ∧ y ≠ x} → Expr.Felicitous M g' φ

theorem PIP.Term.felicitous_abs_of_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} (h : ∀ (g : V → Set α), Expr.Felicitous M g φ) : Expr.Felicitous M g (Expr.abs x φ)

theorem PIP.Term.felicitous_sigma_of_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} (h : ∀ (g : V → Set α), Expr.Felicitous M g φ) : Expr.Felicitous M g (Expr.sigma x φ)

theorem PIP.Term.felicitous_sgPronoun {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) : Expr.Felicitous M g (sgPronoun x φ) ↔ Expr.Felicitous M g (Expr.sigma x φ) ∧ ∃ (a : α), realize M g (Expr.sigma x φ) = {a}

@[simp]

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

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.atom r w ts) ↔ Expr.Felicitous M g w ∧ ∀ (i : Fin n), Expr.Felicitous M g (ts i)

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.eq s t) ↔ Expr.Felicitous M g s ∧ Expr.Felicitous M g t

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.subset s t) ↔ Expr.Felicitous M g s ∧ Expr.Felicitous M g t

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.mem s t) ↔ Expr.Felicitous M g s ∧ Expr.Felicitous M g t

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.sg t) ↔ Expr.Felicitous M g t

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.pl t) ↔ Expr.Felicitous M g t

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.neg φ) ↔ Expr.Felicitous M g φ

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.conj φ ψ) ↔ Expr.Felicitous M g φ ∧ (Realize M g φ → Expr.Felicitous M g ψ)

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.exists_ x φ) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {x}ᶜ → Expr.Felicitous M g' φ

@[simp]

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (Expr.labelDef X φ)

@[simp]

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

theorem PIP.Expr.felicitous_of_presupFree {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) : e.PresupFree → ∀ (g : V → Set α), Felicitous M g e

Every infelicity traces to a presupposition: an expression without presuppositions is felicitous.

Derived clauses

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (φ.disj ψ) ↔ Expr.Felicitous M g φ ∧ (¬Realize M g φ → Expr.Felicitous M g ψ)

F(φ ∨ ψ) iff Fφ ∧ (¬φ → Fψ).

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (φ.impl ψ) ↔ Expr.Felicitous M g φ ∧ (Realize M g φ → Expr.Felicitous M g ψ)

F(φ → ψ) iff Fφ ∧ (φ → Fψ).

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (φ.iff_ ψ) ↔ Expr.Felicitous M g φ ∧ Expr.Felicitous M g ψ

F(φ ↔ ψ) iff Fφ ∧ Fψ.

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (forall_ x φ) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {x}ᶜ → Expr.Felicitous M g' φ

F(∀xφ) iff ∀x Fφ.

theorem PIP.Formula.felicitous_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) : Expr.Felicitous M g (some_ s t) ↔ Expr.Felicitous M g s ∧ Expr.Felicitous M g t

F(some(s, t)) iff Fs ∧ Ft.

theorem PIP.Term.felicitous_sigma_conj {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (w : V) (γ φ : Formula V L P) : Expr.Felicitous M g (Expr.sigma w (Expr.conj γ φ)) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ (Expr.conj γ φ).locals ∧ y ≠ w} → Expr.Felicitous M g' γ ∧ (Formula.Realize M g' γ → Expr.Felicitous M g' φ)

Felicity of a discourse extended by a sentence: F Σw(γ ∧ φ) iff, for every assignment of the world and the local variables, Fγ ∧ (γ → Fφ).

theorem PIP.Term.felicitous_sigma_conj_of_felicitous {V : Type u} {L : Type v} {P : ℕ → Type w} {α : Type u_1} [DecidableEq V] (M : Model P α) (g : V → Set α) (w : V) (γ φ : Formula V L P) (hγ : ∀ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ (Expr.conj γ φ).locals ∧ y ≠ w} → Expr.Felicitous M g' γ) : Expr.Felicitous M g (Expr.sigma w (Expr.conj γ φ)) ↔ ∀ (g' : V → Set α), Set.EqOn g' g {y : V | y ∉ (Expr.conj γ φ).locals ∧ y ≠ w} → Formula.Realize M g' γ → Expr.Felicitous M g' φ

Given that the discourse so far is felicitous for all values of the local variables, the extended discourse is felicitous iff the discourse so far strictly implies the felicity of the new sentence.

Meanings

structure PIP.Value (V : Type u) (L : Type v) (P : ℕ → Type w) : Type (max (max u v) w)

The PIP-value of a formula: its truth, its felicity, its local variables and its label definitions.

• truth : Prop

  Truth.

• felicity : Prop

  Felicity.

• locals : List V

  The free local variables.

• defs : List (L × Formula V L P)

  The label definitions.

theorem PIP.Value.ext {V : Type u} {L : Type v} {P : ℕ → Type w} {x y : Value V L P} (truth : x.truth = y.truth) (felicity : x.felicity = y.felicity) (locals : x.locals = y.locals) (defs : x.defs = y.defs) : x = y

theorem PIP.Value.ext_iff {V : Type u} {L : Type v} {P : ℕ → Type w} {x y : Value V L P} : x = y ↔ x.truth = y.truth ∧ x.felicity = y.felicity ∧ x.locals = y.locals ∧ x.defs = y.defs

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

The PIP-value of a formula. Two formulas are intersubstitutable iff they have the same value in every model under every assignment; truth-equivalent formulas need not be.

Equations

• PIP.Formula.value M g φ = { truth := PIP.Formula.Realize M g φ, felicity := PIP.Expr.Felicitous M g φ, locals := PIP.Expr.locals φ, defs := PIP.Expr.defs φ }