Generalized Conjunction

[PR83]

Conjunction and disjunction defined recursively over the IL type structure:

• Base case (t): Boolean operations
• Function case (⟨a,b⟩): pointwise application
• Intension case (⟨s,a⟩): pointwise over indices

def Intensional.Conjunction.genConj (τ : Ty) (E W : Type) : Denot E W τ → Denot E W τ → Denot E W τ

Generalized conjunction ([PR83] Definition 5). At intension types, conjunction is pointwise over indices.

Equations

• Intensional.Conjunction.genConj Intensional.Ty.t E W = fun (x y : Intensional.Denot E W Intensional.Ty.t) => x ∧ y
• Intensional.Conjunction.genConj Intensional.Ty.e E W = fun (x x_1 : Intensional.Denot E W Intensional.Ty.e) => x
• Intensional.Conjunction.genConj (a ⇒ τ') E W = fun (f g : Intensional.Denot E W (a ⇒ τ')) (x : Intensional.Denot E W a) => Intensional.Conjunction.genConj τ' E W (f x) (g x)
• Intensional.Conjunction.genConj a.intens E W = fun (f g : Intensional.Denot E W a.intens) (i : W) => Intensional.Conjunction.genConj a E W (f i) (g i)

def Intensional.Conjunction.genDisj (τ : Ty) (E W : Type) : Denot E W τ → Denot E W τ → Denot E W τ

Generalized disjunction.

Equations

• Intensional.Conjunction.genDisj Intensional.Ty.t E W = fun (x y : Intensional.Denot E W Intensional.Ty.t) => x ∨ y
• Intensional.Conjunction.genDisj Intensional.Ty.e E W = fun (x x_1 : Intensional.Denot E W Intensional.Ty.e) => x
• Intensional.Conjunction.genDisj (a ⇒ τ') E W = fun (f g : Intensional.Denot E W (a ⇒ τ')) (x : Intensional.Denot E W a) => Intensional.Conjunction.genDisj τ' E W (f x) (g x)
• Intensional.Conjunction.genDisj a.intens E W = fun (f g : Intensional.Denot E W a.intens) (i : W) => Intensional.Conjunction.genDisj a E W (f i) (g i)

def Intensional.Conjunction.genNeg (τ : Ty) (E W : Type) : Denot E W τ → Denot E W τ

Generalized negation (pointwise complement) — the recursion form of ·ᶜ, needed for negative coordination (nor = ¬(A ∨ B)). Junk at .e.

Equations

• Intensional.Conjunction.genNeg Intensional.Ty.t E W = fun (p : Intensional.Denot E W Intensional.Ty.t) => ¬p
• Intensional.Conjunction.genNeg Intensional.Ty.e E W = fun (x : Intensional.Denot E W Intensional.Ty.e) => x
• Intensional.Conjunction.genNeg (a ⇒ τ') E W = fun (f : Intensional.Denot E W (a ⇒ τ')) (x : Intensional.Denot E W a) => Intensional.Conjunction.genNeg τ' E W (f x)
• Intensional.Conjunction.genNeg a.intens E W = fun (f : Intensional.Denot E W a.intens) (i : W) => Intensional.Conjunction.genNeg a E W (f i)

theorem Intensional.Conjunction.genConj_at_t (E W : Type) (p q : Prop) : genConj Ty.t E W p q = (p ∧ q)

theorem Intensional.Conjunction.genConj_at_et (E W : Type) (f g : E → Prop) : genConj (Ty.e ⇒ Ty.t) E W f g = fun (x : E) => f x ∧ g x

theorem Intensional.Conjunction.genConj_at_eet (E W : Type) (f g : E → E → Prop) : genConj (Ty.e ⇒ Ty.e ⇒ Ty.t) E W f g = fun (x y : E) => f x y ∧ g x y

theorem Intensional.Conjunction.genConj_at_intens (E W : Type) {a : Ty} (f g : Denot E W a.intens) : genConj a.intens E W f g = fun (i : W) => genConj a E W (f i) (g i)

At intension types, conjunction is pointwise over indices.

theorem Intensional.Conjunction.genConj_comm_t (E W : Type) (p q : Prop) : genConj Ty.t E W p q = genConj Ty.t E W q p

theorem Intensional.Conjunction.genConj_assoc_t (E W : Type) (p q r : Prop) : genConj Ty.t E W (genConj Ty.t E W p q) r = genConj Ty.t E W p (genConj Ty.t E W q r)

theorem Intensional.Conjunction.genDisj_comm_t (E W : Type) (p q : Prop) : genDisj Ty.t E W p q = genDisj Ty.t E W q p

[PR83] Key Facts

• Fact 6a: φ ∩ ψ = λz[φ(z) ∩ ψ(z)]
• Fact 6b: [φ ∩ ψ](α) = φ(α) ∩ ψ(α)
• Fact 6c: λv.φ ∩ λv.ψ = λv[φ ∩ ψ]

theorem Intensional.Conjunction.genConj_pointwise {E W : Type} {σ τ : Ty} (f g : Denot E W (σ ⇒ τ)) : genConj (σ ⇒ τ) E W f g = fun (x : Denot E W σ) => genConj τ E W (f x) (g x)

Fact 6a: φ ∩ ψ = λz[φ(z) ∩ ψ(z)]

theorem Intensional.Conjunction.genConj_distributes_over_app {E W : Type} {σ τ : Ty} (f g : Denot E W (σ ⇒ τ)) (x : Denot E W σ) : genConj (σ ⇒ τ) E W f g x = genConj τ E W (f x) (g x)

Fact 6b: [φ ∩ ψ](α) = φ(α) ∩ ψ(α)

theorem Intensional.Conjunction.genConj_lambda_distribution {E W : Type} {σ τ : Ty} (f g : Denot E W σ → Denot E W τ) : genConj (σ ⇒ τ) E W f g = fun (v : Denot E W σ) => genConj τ E W (f v) (g v)

Fact 6c: λv.φ ∩ λv.ψ = λv[φ ∩ ψ]

theorem Intensional.Conjunction.genDisj_distributes_over_app {E W : Type} {σ τ : Ty} (f g : Denot E W (σ ⇒ τ)) (x : Denot E W σ) : genDisj (σ ⇒ τ) E W f g x = genDisj τ E W (f x) (g x)

theorem Intensional.Conjunction.genDisj_lambda_distribution {E W : Type} {σ τ : Ty} (f g : Denot E W σ → Denot E W τ) : genDisj (σ ⇒ τ) E W f g = fun (v : Denot E W σ) => genDisj τ E W (f v) (g v)

def Intensional.Conjunction.typeRaise {E W : Type} (e : Denot E W Ty.e) : Denot E W ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

Type-raise an entity to a GQ: e ↦ λP.P(e)

Equations

• Intensional.Conjunction.typeRaise e p = p e

def Intensional.Conjunction.coordEntities {E W : Type} (e1 e2 : Denot E W Ty.e) : Denot E W ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

Coordinated entities: λP. P(e₁) ∧ P(e₂)

Equations

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

theorem Intensional.Conjunction.typeRaise_preserves {E W : Type} (e : Denot E W Ty.e) (p : Denot E W (Ty.e ⇒ Ty.t)) : typeRaise e p = p e

theorem Intensional.Conjunction.coordEntities_both_satisfy {E W : Type} (e1 e2 : Denot E W Ty.e) (p : Denot E W (Ty.e ⇒ Ty.t)) : coordEntities e1 e2 p = (p e1 ∧ p e2)

[MS14] [MS16] Decomposition

DP conjunction decomposes into three operations:

• ☉ (msShift): individual → singleton set (= Partee's ident)
• MU (typeRaise): singleton set → GQ via subset inclusion (INCL)
• J (genConj): generalized conjunction on GQs

def Intensional.Conjunction.msShift {E W : Type} (x : Denot E W Ty.e) : Denot E W (Ty.e ⇒ Ty.t)

☉: M&S type-shifter. Individual → singleton property.

Equations

• Intensional.Conjunction.msShift x y = (x = y)

@[reducible, inline]

abbrev Intensional.Conjunction.inclFunc {E W : Type} (x : Denot E W Ty.e) : Denot E W ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

MU particle semantics = typeRaise.

Equations

• Intensional.Conjunction.inclFunc x = Intensional.Conjunction.typeRaise x

theorem Intensional.Conjunction.ms_full_derivation {E W : Type} (e1 e2 : Denot E W Ty.e) : genConj ((Ty.e ⇒ Ty.t) ⇒ Ty.t) E W (typeRaise e1) (typeRaise e2) = coordEntities e1 e2

Full M&S derivation: J(MU(e₁), MU(e₂)) = coordEntities e₁ e₂.