Documentation

Studies.AbneyKeshet2025

Abney & Keshet (2025): Plural Intensional Presuppositional semantics #

The paper gives PIP (Logic/PIP/) its formal definition and a compositional fragment recasting the textbook rules of interpretation as semantic operations. Indefinites, tense and the traces of determiners are restricted variables, a variable paired with an assertion; FX lifts a predicate to take one, conjoining its assertion (lift); quantifier raising inserts a summation operator labeled with the quantifier's restriction or reference set (SA); modals and negation store their prejacent in a label through intensional functional application (IFA). The fragment is Tree and interp over the typed metalanguage Sem, and the paper's worked trees (47), (56), (59), (66), (93), (99) and (121) are derived (interp_aRedDogBarked, …, interp_mostOfThemUsedIt), the last reading the preceding sentence's labels through PA; value_aRedDogBarked checks intersubstitutability with the paper's abbreviated form, and value_bvar_ne_var that bracketing is not a matter of truth.

The applications are stated as PIP translations and their truth and felicity conditions proved on scenario models (Scenario.model) at a world of evaluation w₀: the paycheck pronoun's value follows its external variable (realize_sigma_indefOwned), (139) is felicitous only where its first sentence is false (felicitous_shop139_iff), the bathroom disjunction needs at most one bathroom (felicitous_bathroom143_iff), modal subordination quantifies over the accessible worlds where a wolf enters (realize_wolfDiscourse_iff), and a nuclear-scope presupposition is satisfied pointwise by the restriction within a sentence and across quantificational subordination (felicitous_everyMonarchy_iff, felicitous_discourse150a_iff). Variables of the formal system range over all pluralities, so where the paper reads a summation variable as a world that is a hypothesis on the assignment, and singular restricted variables carry SG as in the paper's (143); for negation as summation over worlds the two readings come apart, and the double negation of (138b) is false in any model with a second atom (not_realize_shop138).

References #

inductive AbneyKeshet2025.Var :

The variables of the fragment: the world w, the modal-base world u, and the indices of the paper's trees.

w : Var
u : Var
d : Var
b : Var
c : Var
x : Var
z : Var
o : Var
g : Var
p : Var
s : Var
s' : Var
e : Var
t : Var
m : Var
k : Var

Instances For

@[instance_reducible]

instance AbneyKeshet2025.instDecidableEqVar :

DecidableEq Var

Equations

AbneyKeshet2025.instDecidableEqVar x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive AbneyKeshet2025.Lab :

Formula labels, as in the paper's trees and translations.

G : Lab
P : Lab
B : Lab
D : Lab
S : Lab
M : Lab
U : Lab
W : Lab
E : Lab
O : Lab
X : Lab
Y : Lab
R : Lab
K : Lab
C : Lab

Instances For

@[instance_reducible]

instance AbneyKeshet2025.instDecidableEqLab :

DecidableEq Lab

Equations

AbneyKeshet2025.instDecidableEqLab x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive AbneyKeshet2025.Lex :

ℕ → Type

Lexical relation symbols, by number of non-world arguments: the word senses of the paper's examples.

Instances For

inductive AbneyKeshet2025.Sym :

ℕ → Type

Relation symbols: the lexical ones, accessibility between worlds, and the proportional quantifier most.

lex {n : ℕ} (c : Lex n) : Sym n
acc : Sym 1
most : Sym 2

Instances For

@[reducible, inline]

abbrev AbneyKeshet2025.Tm :

Terms of the fragment.

Equations

AbneyKeshet2025.Tm = PIP.Term AbneyKeshet2025.Var AbneyKeshet2025.Lab AbneyKeshet2025.Sym

Instances For

@[reducible, inline]

abbrev AbneyKeshet2025.Fm :

Formulas of the fragment.

Equations

AbneyKeshet2025.Fm = PIP.Formula AbneyKeshet2025.Var AbneyKeshet2025.Lab AbneyKeshet2025.Sym

Instances For

def AbneyKeshet2025.pred₁ (c : Lex 1) (x : Tm) :

A one-place lexical predicate at the world w.

Equations

AbneyKeshet2025.pred₁ c x = PIP.Expr.atom (AbneyKeshet2025.Sym.lex c) (PIP.Expr.var AbneyKeshet2025.Var.w) ![x]

Instances For

def AbneyKeshet2025.pred₂ (c : Lex 2) (x y : Tm) :

A two-place lexical predicate at the world w.

Equations

AbneyKeshet2025.pred₂ c x y = PIP.Expr.atom (AbneyKeshet2025.Sym.lex c) (PIP.Expr.var AbneyKeshet2025.Var.w) ![x, y]

Instances For

def AbneyKeshet2025.restricted (v : Var) (P : Tm → Fm) :

A restricted variable: [x] = x ∧ P(x), the common denotation of the indefinite article, tense and the trace of a determiner (50).

Equations

AbneyKeshet2025.restricted v P = ((PIP.Expr.bvar v).eq (PIP.Expr.var v)).conj (P (PIP.Expr.var v))

Instances For

def AbneyKeshet2025.modalBase :

β_w = Σu acc(w, u): the modal base.

Equations

AbneyKeshet2025.modalBase = PIP.Expr.sigma AbneyKeshet2025.Var.u (PIP.Expr.atom AbneyKeshet2025.Sym.acc (PIP.Expr.var AbneyKeshet2025.Var.w) ![PIP.Expr.var AbneyKeshet2025.Var.u])

Instances For

The metalanguage and the semantic operations #

inductive AbneyKeshet2025.Ty :

Semantic types: individuals, worlds, truth values, functions.

e : Ty
s : Ty
t : Ty
fn (σ τ : Ty) : Ty

Instances For

def AbneyKeshet2025.Sem :

The metalanguage of the fragment: PIP terms at e and s, formulas at t, and functions between them, as which the paper's λ-expressions are read.

Equations

Instances For

def AbneyKeshet2025.lift {τ : Ty} :

Sem τ → Fm → Sem τ

↑-lifting (84): a function whose result is a formula takes an additional assertion, conjoined to its result; the lift is the identity on terms.

Equations

AbneyKeshet2025.lift x_3 x✝ = x_3
AbneyKeshet2025.lift x_3 x✝ = x_3
AbneyKeshet2025.lift ψ x✝ = PIP.Expr.conj ψ x✝
AbneyKeshet2025.lift f x✝ = fun (a : AbneyKeshet2025.Sem σ) => AbneyKeshet2025.lift (f a) x✝

Instances For

def AbneyKeshet2025.NN {τ : Ty} (φ : Sem τ) :

Sem τ

Nonbranching nodes.

Equations

AbneyKeshet2025.NN φ = φ

Instances For

def AbneyKeshet2025.FA {σ τ : Ty} (φ : Sem (σ.fn τ)) (ψ : Sem σ) :

Sem τ

Functional application.

Equations

AbneyKeshet2025.FA φ ψ = φ ψ

Instances For

def AbneyKeshet2025.AF {σ τ : Ty} (φ : Sem σ) (ψ : Sem (σ.fn τ)) :

Sem τ

Reverse functional application.

Equations

AbneyKeshet2025.AF φ ψ = ψ φ

Instances For

def AbneyKeshet2025.IFA (Z : Lab) (φ : Tm → Fm) (ψ : Fm) :

Intensional functional application (82): the body is stored in the label Z and the set of worlds satisfying it is the argument.

Equations

AbneyKeshet2025.IFA Z φ ψ = PIP.Expr.conj (φ (PIP.Expr.sigma AbneyKeshet2025.Var.w (PIP.Expr.label Z))) (PIP.Expr.labelDef Z ψ)

Instances For

def AbneyKeshet2025.FX {τ : Ty} (P : Sem (Ty.e.fn τ)) (v : Var) (φ : Fm) :

Sem τ

Application to a restricted variable: the lifted predicate takes the index and the assertion.

Equations

AbneyKeshet2025.FX P v φ = AbneyKeshet2025.lift (P (PIP.Expr.var v)) φ

Instances For

def AbneyKeshet2025.PM (φ ψ : Tm → Fm) :

Tm → Fm

Predicate modification.

Equations

AbneyKeshet2025.PM φ ψ a = PIP.Expr.conj (φ a) (ψ a)

Instances For

def AbneyKeshet2025.PA (A : List (Lab × Fm)) (v : Var) (φ : Fm) :

Tm → Fm

Predicate abstraction λxφ, reading through the labels A of the preceding discourse before substituting for x (123).

Equations

AbneyKeshet2025.PA A v φ t = PIP.Expr.subst v t (PIP.Formula.expand A φ)

Instances For

def AbneyKeshet2025.SA (v : Var) (Z : Lab) (φ : Fm) :

Summation with a label: ΣxZ where Z ≡ φ, the definition attached to the use.

Equations

AbneyKeshet2025.SA v Z φ = PIP.Expr.sigma v ((PIP.Expr.label Z).conj (PIP.Expr.labelDef Z φ))

Instances For

The lexicon #

inductive AbneyKeshet2025.Word :

Terminals: lexical predicates, thematic roles, determiners, pronouns, and the defined constants (88) with their indices and labels.

pred (c : Lex 1) : Word
role (c : Lex 2) : Word
every : Word
most : Word
a (v : Var) : Word
tense (v : Var) : Word
dTrace (v : Var) : Word
dpTrace (v : Var) : Word
core (v : Var) : Word
ldpTrace (Z : Lab) : Word
she : Word
it : Word
they : Word
not (Z : Lab) : Word
might (Z : Lab) : Word
must (Z : Lab) : Word
base : Word

Instances For

def AbneyKeshet2025.Word.ty :

The semantic type of a terminal.

Equations

Instances For

def AbneyKeshet2025.Word.sem (α : Word) :

The meaning of a terminal (87)–(88): a thematic role λxλe(HAS-ROLE(e, x)), EVERY as inclusion, the restricted variables A_x, T_x, D-T_x, the simple variables DP-T_x and E_x, the label of a labeled trace, pronouns λz(z|Q(z)), negation λψ(w ∉ ψ), the modals as relations to the modal base, and the base β_w.

Equations

(AbneyKeshet2025.Word.pred c).sem = fun (a : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => AbneyKeshet2025.pred₁ c a
(AbneyKeshet2025.Word.role c).sem = fun (a e : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => AbneyKeshet2025.pred₂ c e a
AbneyKeshet2025.Word.every.sem = fun (a b : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => PIP.Expr.subset a b
AbneyKeshet2025.Word.most.sem = fun (a b : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => PIP.Expr.atom AbneyKeshet2025.Sym.most (PIP.Expr.var AbneyKeshet2025.Var.w) ![a, b]
(AbneyKeshet2025.Word.a v).sem = AbneyKeshet2025.restricted v
(AbneyKeshet2025.Word.tense v).sem = AbneyKeshet2025.restricted v
(AbneyKeshet2025.Word.dTrace v).sem = AbneyKeshet2025.restricted v
(AbneyKeshet2025.Word.dpTrace v).sem = PIP.Expr.var v
(AbneyKeshet2025.Word.core v).sem = PIP.Expr.var v
(AbneyKeshet2025.Word.ldpTrace Z).sem = PIP.Expr.label Z
AbneyKeshet2025.Word.she.sem = fun (z : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => PIP.Expr.presup z (PIP.Expr.conj (AbneyKeshet2025.pred₁ AbneyKeshet2025.Lex.fem z) (PIP.Expr.sg z))
AbneyKeshet2025.Word.it.sem = fun (z : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => PIP.Expr.presup z (PIP.Expr.sg z)
AbneyKeshet2025.Word.they.sem = fun (z : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.e) => PIP.Expr.presup z (PIP.Expr.pl z)
(AbneyKeshet2025.Word.not Z).sem = fun (ψ : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.s) => ((PIP.Expr.var AbneyKeshet2025.Var.w).mem ψ).neg
(AbneyKeshet2025.Word.might Z).sem = fun (β ψ : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.s) => PIP.Formula.some_ β ψ
(AbneyKeshet2025.Word.must Z).sem = fun (β ψ : AbneyKeshet2025.Sem AbneyKeshet2025.Ty.s) => PIP.Expr.subset β ψ
AbneyKeshet2025.Word.base.sem = AbneyKeshet2025.modalBase

Instances For

Trees and their interpretation #

inductive AbneyKeshet2025.Tree :

An LF tree annotated with the semantic operation at each node (86), with the index of a restricted variable and the label of a summation or intensional operator as data.

lex (α : Word) : Tree α.ty
nn {τ : Ty} (β : Tree τ) : Tree τ
fa {σ τ : Ty} (β : Tree (σ.fn τ)) (γ : Tree σ) : Tree τ
af {σ τ : Ty} (β : Tree σ) (γ : Tree (σ.fn τ)) : Tree τ
ifa (Z : Lab) (β : Tree (Ty.s.fn Ty.t)) (γ : Tree Ty.t) : Tree Ty.t
fx {τ : Ty} (β : Tree (Ty.e.fn τ)) (v : Var) (γ : Tree Ty.t) : Tree τ
pm (β γ : Tree (Ty.e.fn Ty.t)) : Tree (Ty.e.fn Ty.t)
pa (v : Var) (γ : Tree Ty.t) : Tree (Ty.e.fn Ty.t)
sa (v : Var) (Z : Lab) (γ : Tree Ty.t) : Tree Ty.e

Instances For

def AbneyKeshet2025.interp (A : List (Lab × Fm)) {τ : Ty} :

Tree τ → Sem τ

The meaning of a tree, relative to the label definitions A of the preceding discourse.

Equations

AbneyKeshet2025.interp A (AbneyKeshet2025.Tree.lex α) = α.sem
AbneyKeshet2025.interp A β.nn = AbneyKeshet2025.NN (AbneyKeshet2025.interp A β)
AbneyKeshet2025.interp A (β.fa γ) = AbneyKeshet2025.FA (AbneyKeshet2025.interp A β) (AbneyKeshet2025.interp A γ)
AbneyKeshet2025.interp A (β.af γ) = AbneyKeshet2025.AF (AbneyKeshet2025.interp A β) (AbneyKeshet2025.interp A γ)
AbneyKeshet2025.interp A (AbneyKeshet2025.Tree.ifa Z β γ) = AbneyKeshet2025.IFA Z (AbneyKeshet2025.interp A β) (AbneyKeshet2025.interp A γ)
AbneyKeshet2025.interp A (β.fx v γ) = AbneyKeshet2025.FX (AbneyKeshet2025.interp A β) v (AbneyKeshet2025.interp A γ)
AbneyKeshet2025.interp A (β.pm γ) = AbneyKeshet2025.PM (AbneyKeshet2025.interp A β) (AbneyKeshet2025.interp A γ)
AbneyKeshet2025.interp A (AbneyKeshet2025.Tree.pa v γ) = AbneyKeshet2025.PA A v (AbneyKeshet2025.interp A γ)
AbneyKeshet2025.interp A (AbneyKeshet2025.Tree.sa v Z γ) = AbneyKeshet2025.SA v Z (AbneyKeshet2025.interp A γ)

Instances For

The paper's trees #

def AbneyKeshet2025.aRedDogBarked :

(47): "a red dog barked".

Equations

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

Instances For

theorem AbneyKeshet2025.interp_aRedDogBarked :

interp [] aRedDogBarked = (PIP.Expr.conj (pred₂ Lex.hasAgent (PIP.Expr.var Var.b) (PIP.Expr.var Var.d)) (restricted Var.d fun (x : Tm) => PIP.Expr.conj (pred₁ Lex.red x) (pred₁ Lex.dog x))).conj (restricted Var.b (pred₁ Lex.barkEvt))

(91)–(92): the meaning of (47).

def AbneyKeshet2025.form92 :

(92) abbreviated: HAS-AGENT(b, d) ∧ RED([d]) ∧ DOG(d) ∧ BARK-EVT([b]).

Equations

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

Instances For

theorem AbneyKeshet2025.value_aRedDogBarked {W E : Type} (M : PIP.Model Sym (PIP.Atom W E)) (g : Var → Set (PIP.Atom W E)) :

PIP.Formula.value M g (interp [] aRedDogBarked) = PIP.Formula.value M g form92

The meaning of (47) is intersubstitutable with its abbreviation (92): same truth, felicity, local variables and label definitions.

theorem AbneyKeshet2025.realize_bvar_iff_var {W E : Type} (M : PIP.Model Sym (PIP.Atom W E)) (g : Var → Set (PIP.Atom W E)) (c : Lex 1) (v : Var) :

PIP.Formula.Realize M g (pred₁ c (PIP.Expr.bvar v)) ↔ PIP.Formula.Realize M g (pred₁ c (PIP.Expr.var v))

DOG([d]) and DOG(d) are truth-equivalent.

theorem AbneyKeshet2025.value_bvar_ne_var {W E : Type} (M : PIP.Model Sym (PIP.Atom W E)) (g : Var → Set (PIP.Atom W E)) (c : Lex 1) (v : Var) :

PIP.Formula.value M g (pred₁ c (PIP.Expr.bvar v)) ≠ PIP.Formula.value M g (pred₁ c (PIP.Expr.var v))

DOG([d]) and DOG(d) are not intersubstitutable: their local variables differ.

def AbneyKeshet2025.chasedACat :

Tree (Ty.e.fn Ty.t)

(56): "chased a cat", a VP.

Equations

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

Instances For

theorem AbneyKeshet2025.interp_chasedACat :

interp [] chasedACat = fun (e : Sem Ty.e) => PIP.Expr.conj (pred₁ Lex.chaseEvt e) (PIP.Expr.conj (pred₂ Lex.hasPatient e (PIP.Expr.var Var.c)) (restricted Var.c (pred₁ Lex.cat)))

(57): λe(CHASE-EVT(e) ∧ HAS-PATIENT(e, c) ∧ CAT([c])).

def AbneyKeshet2025.aFarmerWhoOwnsADonkey :

(59): "a farmer who owns a donkey", with the relative pronoun's trace a simple variable combined by FA and the clause abstracted by PA.

Equations

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

Instances For

theorem AbneyKeshet2025.interp_aFarmerWhoOwnsADonkey :

interp [] aFarmerWhoOwnsADonkey = restricted Var.x fun (y : Tm) => PIP.Expr.conj (pred₁ Lex.farmer y) (PIP.Expr.conj (pred₂ Lex.hasGoal (PIP.Expr.var Var.o) (PIP.Expr.var Var.x)) (restricted Var.o fun (e : Tm) => PIP.Expr.conj (pred₁ Lex.ownEvt e) (PIP.Expr.conj (pred₂ Lex.hasPatient e (PIP.Expr.var Var.d)) (restricted Var.d (pred₁ Lex.donkey)))))

(65): FARMER([x]) ∧ DONKEY([d]) ∧ OWNS([o], x, d), the relative pronoun's variable replaced by the indefinite's index.

def AbneyKeshet2025.everyGirlWroteAPaper :

(66): "every girl wrote a paper", quantifier raising leaving a restricted-variable trace in the restriction and a labeled trace in the scope.

Equations

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

Instances For

theorem AbneyKeshet2025.interp_everyGirlWroteAPaper :

interp [] everyGirlWroteAPaper = PIP.Expr.subset (SA Var.g Lab.G (restricted Var.g (pred₁ Lex.girl))) (SA Var.g Lab.P ((PIP.Expr.conj (pred₂ Lex.hasAgent (PIP.Expr.var Var.u) (PIP.Expr.var Var.g)) (PIP.Expr.label Lab.G)).conj (restricted Var.u fun (e : Tm) => PIP.Expr.conj (pred₁ Lex.writeEvt e) (PIP.Expr.conj (pred₂ Lex.hasPatient e (PIP.Expr.var Var.p)) (restricted Var.p (pred₁ Lex.paper))))))

(79): EVERY(ΣgG, ΣgP) where G ≡ GIRL([g]), P ≡ (G ∧ PAPER([p]) ∧ WROTE([u], g, p)).

def AbneyKeshet2025.sheX :

(93): the simple pronoun "she_x".

Equations

AbneyKeshet2025.sheX = (AbneyKeshet2025.Tree.lex AbneyKeshet2025.Word.she).fa (AbneyKeshet2025.Tree.lex (AbneyKeshet2025.Word.core AbneyKeshet2025.Var.x))

Instances For

theorem AbneyKeshet2025.interp_sheX :

interp [] sheX = (PIP.Expr.var Var.x).presup (PIP.Expr.conj (pred₁ Lex.fem (PIP.Expr.var Var.x)) (PIP.Expr.var Var.x).sg)

(94c): x | FEM(x) ∧ SG(x).

def AbneyKeshet2025.theyP :

(99): the summation pronoun "they^P_p" after (66).

Equations

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

Instances For

theorem AbneyKeshet2025.interp_theyP :

interp [] theyP = PIP.Expr.presup (SA Var.p Lab.Y (PIP.Expr.label Lab.P)) (PIP.Expr.pl (SA Var.p Lab.Y (PIP.Expr.label Lab.P)))

(100): (ΣpP) | PL(ΣpP), the label Y of the pronoun's summation defined as P.

def AbneyKeshet2025.defs118 :

List (Lab × Fm)

(118): the label definitions of "Almost every student brought an umbrella today", S ≡ STUDENT([s]), B ≡ (S ∧ UMBRELLA([u]) ∧ BROUGHT([b], s, u)).

Equations

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

Instances For

def AbneyKeshet2025.mostOfThemUsedIt :

(121): "Most of them used it", the subordinate quantifier's restriction a labeled trace of the preceding sentence abstracted by PA (122).

Equations

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

Instances For

theorem AbneyKeshet2025.interp_mostOfThemUsedIt :

interp defs118 mostOfThemUsedIt = PIP.Expr.atom Sym.most (PIP.Expr.var Var.w) ![SA Var.s' Lab.M (restricted Var.s' fun (y : Tm) => (((PIP.Expr.bvar Var.s').eq y).conj (pred₁ Lex.student y)).conj (PIP.Expr.conj (restricted Var.u (pred₁ Lex.umbrella)) (PIP.Expr.atom (Sym.lex Lex.brought) (PIP.Expr.var Var.w) ![PIP.Expr.bvar Var.b, y, PIP.Expr.var Var.u]))), SA Var.s' Lab.U ((PIP.Expr.conj (pred₂ Lex.hasAgent (PIP.Expr.var Var.e) (PIP.Expr.var Var.s')) (PIP.Expr.label Lab.M)).conj (restricted Var.e fun (e : Tm) => PIP.Expr.conj (pred₁ Lex.useEvt e) (pred₂ Lex.hasPatient e ((PIP.Expr.var Var.u).presup (PIP.Expr.var Var.u).sg))))]

(128): MOST(Σs′M, Σs′U) with M the definition of B under s ↦ s′ (127) and U ≡ M ∧ USED([e], s′, u).

Scenarios #

structure AbneyKeshet2025.Scenario (W E : Type) :

A scenario: accessibility between worlds, the proportional relation interpreting most, and the lexical relations at each world, by arity.

acc : W → W → Prop
most : Set (PIP.Atom W E) → Set (PIP.Atom W E) → Prop
rel₁ : Lex 1 → W → E → Prop
rel₂ : Lex 2 → W → E → E → Prop
rel₃ : Lex 3 → W → E → E → E → Prop

Instances For

def AbneyKeshet2025.Scenario.rel {W E : Type} (S : Scenario W E) {n : ℕ} :

Lex n → W → (Fin n → PIP.Atom W E) → Prop

The lexical relations of a scenario on tuples of atoms: true of entities only.

Equations

S.rel c x✝ as = ∃ (e : E), as 0 = Sum.inr e ∧ S.rel₁ c x✝ e
S.rel c x✝ as = ∃ (e : E) (e' : E), as 0 = Sum.inr e ∧ as 1 = Sum.inr e' ∧ S.rel₂ c x✝ e e'
S.rel c x✝ as = ∃ (e : E) (e' : E) (e'' : E), as 0 = Sum.inr e ∧ as 1 = Sum.inr e' ∧ as 2 = Sum.inr e'' ∧ S.rel₃ c x✝ e e' e''
S.rel x_4 x✝ x_6 = False
S.rel x_4 x✝ x_6 = False

Instances For

def AbneyKeshet2025.Scenario.model {W E : Type} (S : Scenario W E) :

PIP.Model Sym (PIP.Atom W E)

The model of a scenario: lexical symbols distributively over pluralities of entities, accessibility between worlds, and most as the scenario's proportional relation.

Equations

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

Instances For

theorem AbneyKeshet2025.felicitous_pred₁ {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c : Lex 1) (t : Tm) :

PIP.Expr.Felicitous S.model h (pred₁ c t) ↔ PIP.Expr.Felicitous S.model h t

theorem AbneyKeshet2025.felicitous_pred₂ {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c : Lex 2) (s t : Tm) :

PIP.Expr.Felicitous S.model h (pred₂ c s t) ↔ PIP.Expr.Felicitous S.model h s ∧ PIP.Expr.Felicitous S.model h t

theorem AbneyKeshet2025.realize_mem_world {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) (t : Tm) :

PIP.Formula.Realize S.model h ((PIP.Expr.var Var.w).mem t) ↔ Sum.inl w₀ ∈ PIP.Term.realize S.model h t

w ∈ τ at the world w₀.

theorem AbneyKeshet2025.realize_modalBase {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) :

PIP.Term.realize S.model h modalBase = Sum.inl '' {u : W | S.acc w₀ u}

The modal base at the world w₀: the worlds accessible from it.

Singular indefinites #

def AbneyKeshet2025.sgIndef (c : Lex 1) (v : Var) :

SG(v) ∧ c_w([v]): a singular indefinite [v] of kind c.

Equations

AbneyKeshet2025.sgIndef c v = (PIP.Expr.var v).sg.conj (AbneyKeshet2025.pred₁ c (PIP.Expr.bvar v))

Instances For

def AbneyKeshet2025.sgIndefWith (c c' : Lex 1) (v : Var) :

SG(v) ∧ c_w([v]) ∧ c′_w(v): a singular indefinite with a further predicate.

Equations

AbneyKeshet2025.sgIndefWith c c' v = PIP.Expr.conj (AbneyKeshet2025.sgIndef c v) (AbneyKeshet2025.pred₁ c' (PIP.Expr.var v))

Instances For

theorem AbneyKeshet2025.locals_sgIndef (c : Lex 1) (v : Var) :

PIP.Expr.locals (sgIndef c v) = [v]

theorem AbneyKeshet2025.locals_sgIndefWith (c c' : Lex 1) (v : Var) :

PIP.Expr.locals (sgIndefWith c c' v) = [v]

theorem AbneyKeshet2025.felicitous_sgIndef {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c : Lex 1) (v : Var) :

PIP.Expr.Felicitous S.model h (sgIndef c v)

theorem AbneyKeshet2025.felicitous_sgIndefWith {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c c' : Lex 1) (v : Var) :

PIP.Expr.Felicitous S.model h (sgIndefWith c c' v)

theorem AbneyKeshet2025.realize_sgIndef {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c : Lex 1) (v : Var) :

PIP.Formula.Realize S.model h (sgIndef c v) ↔ ∃ (w : W), h Var.w = PIP.world w ∧ ∃ (e : E), h v = {Sum.inr e} ∧ S.rel₁ c w e

theorem AbneyKeshet2025.realize_sgIndefWith {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c c' : Lex 1) (v : Var) :

PIP.Formula.Realize S.model h (sgIndefWith c c' v) ↔ ∃ (w : W), h Var.w = PIP.world w ∧ ∃ (e : E), h v = {Sum.inr e} ∧ S.rel₁ c w e ∧ S.rel₁ c' w e

theorem AbneyKeshet2025.realize_sgIndef_world {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (c : Lex 1) (v : Var) (hw : h Var.w = PIP.world w₀) :

PIP.Formula.Realize S.model h (sgIndef c v) ↔ ∃ (e : E), h v = {Sum.inr e} ∧ S.rel₁ c w₀ e

theorem AbneyKeshet2025.realize_sgIndefWith_world {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (c c' : Lex 1) (v : Var) (hw : h Var.w = PIP.world w₀) :

PIP.Formula.Realize S.model h (sgIndefWith c c' v) ↔ ∃ (e : E), h v = {Sum.inr e} ∧ S.rel₁ c w₀ e ∧ S.rel₁ c' w₀ e

theorem AbneyKeshet2025.realize_sigma_sgIndef {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (c : Lex 1) {v : Var} (hv : v ≠ Var.w) (hw : h Var.w = PIP.world w₀) :

PIP.Term.realize S.model h (PIP.Expr.sigma v (sgIndef c v)) = Sum.inr '' {e : E | S.rel₁ c w₀ e}

The summation over a singular indefinite at w₀: the entities of its kind there.

theorem AbneyKeshet2025.realize_sigma_sgIndefWith {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (c c' : Lex 1) {v : Var} (hv : v ≠ Var.w) (hw : h Var.w = PIP.world w₀) :

PIP.Term.realize S.model h (PIP.Expr.sigma v (sgIndefWith c c' v)) = Sum.inr '' {e : E | S.rel₁ c w₀ e ∧ S.rel₁ c' w₀ e}

Paycheck pronouns and negation #

def AbneyKeshet2025.indefOwned (c₁ : Lex 1) (c₂ : Lex 2) (y : Var) :

c₁_w([y]) ∧ c₂_w(x, y): an indefinite [y] of kind c₁ standing in the relation c₂ to the external variable x — D ≡ DIORAMA([d]) ∧ MADE(x, d) (112), O ≡ CAR([c]) ∧ OWNS(x, c) (137).

Equations

AbneyKeshet2025.indefOwned c₁ c₂ y = PIP.Expr.conj (AbneyKeshet2025.pred₁ c₁ (PIP.Expr.bvar y)) (AbneyKeshet2025.pred₂ c₂ (PIP.Expr.var AbneyKeshet2025.Var.x) (PIP.Expr.var y))

Instances For

theorem AbneyKeshet2025.locals_indefOwned (c₁ : Lex 1) (c₂ : Lex 2) {y : Var} :

PIP.Expr.locals (indefOwned c₁ c₂ y) = [y]

theorem AbneyKeshet2025.felicitous_indefOwned {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) (c₁ : Lex 1) (c₂ : Lex 2) {y : Var} :

PIP.Expr.Felicitous S.model h (indefOwned c₁ c₂ y)

theorem AbneyKeshet2025.realize_indefOwned {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {x₀ : E} (c₁ : Lex 1) (c₂ : Lex 2) {y : Var} (hx : h Var.x = {Sum.inr x₀}) :

PIP.Formula.Realize S.model h (indefOwned c₁ c₂ y) ↔ ∃ (w : W), h Var.w = PIP.world w ∧ (h y).Nonempty ∧ h y ⊆ Sum.inr '' {e : E | S.rel₁ c₁ w e ∧ S.rel₂ c₂ w x₀ e}

theorem AbneyKeshet2025.realize_sigma_indefOwned {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} {x₀ : E} (c₁ : Lex 1) (c₂ : Lex 2) {y : Var} (hw : h Var.w = PIP.world w₀) (hx : h Var.x = {Sum.inr x₀}) (hyw : y ≠ Var.w) (hyx : y ≠ Var.x) :

PIP.Term.realize S.model h (PIP.Expr.sigma y (indefOwned c₁ c₂ y)) = Sum.inr '' {e : E | S.rel₁ c₁ w₀ e ∧ S.rel₂ c₂ w₀ x₀ e}

The summation over the indefinite takes its value from the external variable: the paycheck pronoun ΣdD denotes the dioramas made by whatever x is (112).

theorem AbneyKeshet2025.realize_sigmaW_indefOwned {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {x₀ : E} (c₁ : Lex 1) (c₂ : Lex 2) {y : Var} (hx : h Var.x = {Sum.inr x₀}) (hyw : y ≠ Var.w) (hyx : y ≠ Var.x) :

PIP.Term.realize S.model h (PIP.Expr.sigma Var.w (indefOwned c₁ c₂ y)) = Sum.inl '' {w : W | ∃ (e : E), S.rel₁ c₁ w e ∧ S.rel₂ c₂ w x₀ e}

The summation over worlds of the indefinite's description: the worlds where x has such a thing.

theorem AbneyKeshet2025.felicitous_sgPronoun_indefOwned_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} {x₀ : E} (c₁ : Lex 1) (c₂ : Lex 2) {y : Var} (hw : h Var.w = PIP.world w₀) (hx : h Var.x = {Sum.inr x₀}) (hyw : y ≠ Var.w) (hyx : y ≠ Var.x) :

PIP.Expr.Felicitous S.model h (PIP.Term.sgPronoun y (indefOwned c₁ c₂ y)) ↔ ∃! e : E, S.rel₁ c₁ w₀ e ∧ S.rel₂ c₂ w₀ x₀ e

def AbneyKeshet2025.ownCar :

O ≡ CAR_w([c]) ∧ OWNS_w(x, c) (137).

Equations

AbneyKeshet2025.ownCar = AbneyKeshet2025.indefOwned AbneyKeshet2025.Lex.car AbneyKeshet2025.Lex.owns AbneyKeshet2025.Var.c

Instances For

def AbneyKeshet2025.notOwn :

NOT^O: w ∉ ΣwO (136)–(137), "he doesn't own a car".

Equations

AbneyKeshet2025.notOwn = ((PIP.Expr.var AbneyKeshet2025.Var.w).mem (PIP.Expr.sigma AbneyKeshet2025.Var.w (PIP.Expr.label AbneyKeshet2025.Lab.O))).neg

Instances For

def AbneyKeshet2025.shop139 :

(139): "He doesn't own a car. #It is in the shop."

Equations

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

Instances For

def AbneyKeshet2025.shop138 :

(138b): "It's not like he doesn't own a car. It is just in the shop."

Equations

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

Instances For

theorem AbneyKeshet2025.felicitous_shop139_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} {x₀ : E} (hw : h Var.w = PIP.world w₀) (hx : h Var.x = {Sum.inr x₀}) :

PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf shop139) ↔ ∃ (c : E), S.rel₁ Lex.car w₀ c ∧ S.rel₂ Lex.owns w₀ x₀ c

(139) is felicitous at w₀ iff he owns a car there — iff its first sentence is false.

theorem AbneyKeshet2025.not_realize_shop138 {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) (a₁ : PIP.Atom W E) (ha : a₁ ≠ Sum.inl w₀) :

¬PIP.Formula.Realize S.model h (PIP.Formula.expandSelf shop138)

The double negation of (138b) sums w over all pluralities, of which every non-world fails w ∈ ΣwO; so w ∉ Σw(w ∉ ΣwO) is false at any world once the model has a second atom.

Negation and disjunction #

def AbneyKeshet2025.bathroomX :

X ≡ SG(b) ∧ BATHROOM_w([b]) ∧ HERE_w(b) (143).

Equations

AbneyKeshet2025.bathroomX = AbneyKeshet2025.sgIndefWith AbneyKeshet2025.Lex.bathroom AbneyKeshet2025.Lex.here AbneyKeshet2025.Var.b

Instances For

def AbneyKeshet2025.bathroom143 :

(143): "Either there is no bathroom here or it's in a funny place", (w ∉ ΣwX ∨ FUNNY-PLACE_w(ΣbX | SG(ΣbX))) ∧ X ≡ ….

Equations

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

Instances For

theorem AbneyKeshet2025.felicitous_bathroomX {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Expr.Felicitous S.model h bathroomX

theorem AbneyKeshet2025.realize_sigmaB_bathroomX {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) :

PIP.Term.realize S.model h (PIP.Expr.sigma Var.b bathroomX) = Sum.inr '' {e : E | S.rel₁ Lex.bathroom w₀ e ∧ S.rel₁ Lex.here w₀ e}

theorem AbneyKeshet2025.realize_sigmaW_bathroomX {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Term.realize S.model h (PIP.Expr.sigma Var.w bathroomX) = Sum.inl '' {w : W | ∃ (e : E), S.rel₁ Lex.bathroom w e ∧ S.rel₁ Lex.here w e}

theorem AbneyKeshet2025.felicitous_bathroom143_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) :

PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf bathroom143) ↔ (∃ (e : E), S.rel₁ Lex.bathroom w₀ e ∧ S.rel₁ Lex.here w₀ e) → ∃! e : E, S.rel₁ Lex.bathroom w₀ e ∧ S.rel₁ Lex.here w₀ e

(145): the bathroom disjunction is felicitous at w₀ iff, if there is a bathroom here, there is exactly one.

def AbneyKeshet2025.wolfW :

W ≡ WOLF_w([x]) ∧ ENTERS_w(x) (133a).

Equations

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

Instances For

def AbneyKeshet2025.wolfE :

E ≡ W ∧ TIM_w([t]) ∧ EATS_w(x, t) (133b).

Equations

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

Instances For

def AbneyKeshet2025.wolfDiscourse :

(133): "A wolf might enter. It would eat Tasty Tim first.", MIGHT(β_w, ΣwW) ∧ MUST(β_w, ΣwW, ΣwE) (129) with the second modal's restriction the first's nuclear scope.

Equations

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

Instances For

def AbneyKeshet2025.wolfE' :

E with W expanded.

Equations

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

Instances For

theorem AbneyKeshet2025.locals_wolfE' :

PIP.Expr.locals wolfE' = [Var.x, Var.t]

theorem AbneyKeshet2025.realize_wolfW {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Formula.Realize S.model h wolfW ↔ ∃ (w : W), h Var.w = PIP.world w ∧ (h Var.x).Nonempty ∧ h Var.x ⊆ Sum.inr '' {e : E | S.rel₁ Lex.wolf w e ∧ S.rel₁ Lex.enters w e}

theorem AbneyKeshet2025.realize_wolfE' {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Formula.Realize S.model h wolfE' ↔ ∃ (w : W), h Var.w = PIP.world w ∧ (h Var.x).Nonempty ∧ (h Var.t).Nonempty ∧ h Var.x ⊆ Sum.inr '' {e : E | S.rel₁ Lex.wolf w e ∧ S.rel₁ Lex.enters w e} ∧ (∀ b ∈ h Var.t, ∃ (t : E), b = Sum.inr t ∧ S.rel₁ Lex.tim w t) ∧ ∀ a ∈ h Var.x, ∀ b ∈ h Var.t, ∃ (e : E) (t : E), a = Sum.inr e ∧ b = Sum.inr t ∧ S.rel₂ Lex.eats w e t

theorem AbneyKeshet2025.realize_sigmaW_wolfW {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Term.realize S.model h (PIP.Expr.sigma Var.w wolfW) = Sum.inl '' {w : W | ∃ (e : E), S.rel₁ Lex.wolf w e ∧ S.rel₁ Lex.enters w e}

theorem AbneyKeshet2025.realize_sigmaW_wolfE' {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Term.realize S.model h (PIP.Expr.sigma Var.w wolfE') = Sum.inl '' {w : W | ∃ (e : E) (t : E), (S.rel₁ Lex.wolf w e ∧ S.rel₁ Lex.enters w e) ∧ S.rel₁ Lex.tim w t ∧ S.rel₂ Lex.eats w e t}

theorem AbneyKeshet2025.realize_wolfDiscourse_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) :

PIP.Formula.Realize S.model h (PIP.Formula.expandSelf wolfDiscourse) ↔ (∃ (u : W) (e : E), S.acc w₀ u ∧ S.rel₁ Lex.wolf u e ∧ S.rel₁ Lex.enters u e) ∧ ∀ (u : W), S.acc w₀ u → (∃ (e : E), S.rel₁ Lex.wolf u e ∧ S.rel₁ Lex.enters u e) → ∃ (e : E) (t : E), (S.rel₁ Lex.wolf u e ∧ S.rel₁ Lex.enters u e) ∧ S.rel₁ Lex.tim u t ∧ S.rel₂ Lex.eats u e t

(133) at w₀: some accessible world has a wolf entering, and in every accessible world where a wolf enters, a wolf that enters eats Tim.

Summation pronouns #

def AbneyKeshet2025.theyLoud :

(102)–(103): "Most dogs bark. They are loud.", MOST(ΣdD, ΣdB) ∧ LOUD(ΣdB) with D ≡ DOG([d]), B ≡ (D ∧ BARKS(d)).

Equations

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

Instances For

(104): the pronoun denotes the sum of the barking dogs.

Presupposition under quantification #

def AbneyKeshet2025.monarchK :

K ≡ MONARCH-OF_w([k], m); ΣkK | SG(ΣkK) is "its monarch".

Equations

AbneyKeshet2025.monarchK = AbneyKeshet2025.pred₂ AbneyKeshet2025.Lex.monarchOf (PIP.Expr.bvar AbneyKeshet2025.Var.k) (PIP.Expr.var AbneyKeshet2025.Var.m)

Instances For

def AbneyKeshet2025.cherishBody (Z : Lab) :

Z ∧ CHERISH_w(m, ΣkK | SG(ΣkK)): the nuclear scope of "cherishes its monarch" over the restriction Z, the pronoun's presupposition to be satisfied by Z.

Equations

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

Instances For

def AbneyKeshet2025.monarchyR :

R ≡ SG(m) ∧ MONARCHY_w([m]).

Equations

AbneyKeshet2025.monarchyR = AbneyKeshet2025.sgIndef AbneyKeshet2025.Lex.monarchy AbneyKeshet2025.Var.m

Instances For

def AbneyKeshet2025.everyMonarchy :

(146a): "Every monarchy cherishes its monarch", EVERY(ΣmR, ΣmS) with S ≡ R ∧ CHERISH(m, ΣkK | SG(ΣkK)).

Equations

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

Instances For

def AbneyKeshet2025.countryC :

C ≡ SG(m) ∧ COUNTRY_w([m]).

Equations

AbneyKeshet2025.countryC = AbneyKeshet2025.sgIndef AbneyKeshet2025.Lex.country AbneyKeshet2025.Var.m

Instances For

def AbneyKeshet2025.monarchyM :

M ≡ C ∧ MONARCHY_w(m): the reference set of "every European country was a monarchy".

Equations

AbneyKeshet2025.monarchyM = (PIP.Expr.label AbneyKeshet2025.Lab.C).conj (AbneyKeshet2025.pred₁ AbneyKeshet2025.Lex.monarchy (PIP.Expr.var AbneyKeshet2025.Var.m))

Instances For

def AbneyKeshet2025.discourse150a :

(150a): "Every European country was a monarchy. Most of them cherished their monarchs.", the subordinate quantifier's restriction the first sentence's reference-set label M.

Equations

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

Instances For

def AbneyKeshet2025.cherishBody' (ρ : Fm) :

The nuclear scope with the restriction and the pronoun's label expanded.

Equations

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

Instances For

def AbneyKeshet2025.monarchyM' :

M with C expanded.

Equations

AbneyKeshet2025.monarchyM' = AbneyKeshet2025.sgIndefWith AbneyKeshet2025.Lex.country AbneyKeshet2025.Lex.monarchy AbneyKeshet2025.Var.m

Instances For

theorem AbneyKeshet2025.felicitous_monarchK {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Expr.Felicitous S.model h monarchK

theorem AbneyKeshet2025.realize_monarchK {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) :

PIP.Formula.Realize S.model h monarchK ↔ ∃ (w : W), h Var.w = PIP.world w ∧ (h Var.k).Nonempty ∧ (h Var.m).Nonempty ∧ ∀ a ∈ h Var.k, ∀ b ∈ h Var.m, ∃ (e : E) (e' : E), a = Sum.inr e ∧ b = Sum.inr e' ∧ S.rel₂ Lex.monarchOf w e e'

theorem AbneyKeshet2025.realize_sigmaK_monarchK {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} {m₀ : E} (hw : h Var.w = PIP.world w₀) (hm : h Var.m = {Sum.inr m₀}) :

PIP.Term.realize S.model h (PIP.Expr.sigma Var.k monarchK) = Sum.inr '' {e : E | S.rel₂ Lex.monarchOf w₀ e m₀}

"Its monarch" at a singular m₀: the monarchs of m₀.

theorem AbneyKeshet2025.felicitous_sgPronoun_monarchK_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} {m₀ : E} (hw : h Var.w = PIP.world w₀) (hm : h Var.m = {Sum.inr m₀}) :

PIP.Expr.Felicitous S.model h (PIP.Term.sgPronoun Var.k monarchK) ↔ ∃! e : E, S.rel₂ Lex.monarchOf w₀ e m₀

theorem AbneyKeshet2025.felicitous_sigmaM_cherishBody'_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} {ρ : Fm} {Q : E → Prop} (hw : h Var.w = PIP.world w₀) (hlw : Var.w ∉ PIP.Expr.locals ρ) (hρf : ∀ (g : Var → Set (PIP.Atom W E)), PIP.Expr.Felicitous S.model g ρ) (hρ : ∀ (g : Var → Set (PIP.Atom W E)), g Var.w = PIP.world w₀ → (PIP.Formula.Realize S.model g ρ ↔ ∃ (m₀ : E), g Var.m = {Sum.inr m₀} ∧ Q m₀)) :

PIP.Expr.Felicitous S.model h (PIP.Expr.sigma Var.m (cherishBody' ρ)) ↔ ∀ (m₀ : E), Q m₀ → ∃! e : E, S.rel₂ Lex.monarchOf w₀ e m₀

Felicity of the nuclear-scope summation over a restriction ρ true exactly of the singular m satisfying Q: the pronoun's presupposition, for each of them.

theorem AbneyKeshet2025.felicitous_everyMonarchy_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) :

PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf everyMonarchy) ↔ ∀ (m₀ : E), S.rel₁ Lex.monarchy w₀ m₀ → ∃! e : E, S.rel₂ Lex.monarchOf w₀ e m₀

(146a) is felicitous at w₀ iff every monarchy there has exactly one monarch: the restriction satisfies the presupposition of the nuclear scope pointwise.

theorem AbneyKeshet2025.felicitous_discourse150a_iff {W E : Type} (S : Scenario W E) (h : Var → Set (PIP.Atom W E)) {w₀ : W} (hw : h Var.w = PIP.world w₀) :

PIP.Expr.Felicitous S.model h (PIP.Formula.expandSelf discourse150a) ↔ (∀ (e : E), S.rel₁ Lex.country w₀ e → S.rel₁ Lex.monarchy w₀ e) → ∀ (m₀ : E), S.rel₁ Lex.country w₀ m₀ ∧ S.rel₁ Lex.monarchy w₀ m₀ → ∃! e : E, S.rel₂ Lex.monarchOf w₀ e m₀

(150a) is felicitous at w₀ iff, granted its first sentence, every country that is a monarchy has exactly one monarch: the label incorporated into the subordinate quantifier's restriction satisfies the presupposition of its nuclear scope.