Generalized Conjunction

@cite{partee-rooth-1983}

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 Core.Logic.Intensional.Conjunction.genConj (τ : Ty) (F : Frame) : F.Denot τ → F.Denot τ → F.Denot τ

Generalized conjunction (@cite{partee-rooth-1983} Definition 5). At intension types, conjunction is pointwise over indices.

Equations

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

def Core.Logic.Intensional.Conjunction.genDisj (τ : Ty) (F : Frame) : F.Denot τ → F.Denot τ → F.Denot τ

Generalized disjunction.

Equations

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

theorem Core.Logic.Intensional.Conjunction.genConj_at_t (F : Frame) (p q : Prop) : genConj Ty.t F p q = (p ∧ q)

theorem Core.Logic.Intensional.Conjunction.genConj_at_et (F : Frame) (f g : F.Entity → Prop) : genConj (Ty.e ⇒ Ty.t) F f g = fun (x : F.Entity) => f x ∧ g x

theorem Core.Logic.Intensional.Conjunction.genConj_at_eet (F : Frame) (f g : F.Entity → F.Entity → Prop) : genConj (Ty.e ⇒ Ty.e ⇒ Ty.t) F f g = fun (x y : F.Entity) => f x y ∧ g x y

theorem Core.Logic.Intensional.Conjunction.genConj_at_intens (F : Frame) {a : Ty} (f g : F.Denot a.intens) : genConj a.intens F f g = fun (i : F.Index) => genConj a F (f i) (g i)

At intension types, conjunction is pointwise over indices.

theorem Core.Logic.Intensional.Conjunction.genConj_comm_t (F : Frame) (p q : Prop) : genConj Ty.t F p q = genConj Ty.t F q p

theorem Core.Logic.Intensional.Conjunction.genConj_assoc_t (F : Frame) (p q r : Prop) : genConj Ty.t F (genConj Ty.t F p q) r = genConj Ty.t F p (genConj Ty.t F q r)

theorem Core.Logic.Intensional.Conjunction.genDisj_comm_t (F : Frame) (p q : Prop) : genDisj Ty.t F p q = genDisj Ty.t F q p

@cite{partee-rooth-1983} Key Facts

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

theorem Core.Logic.Intensional.Conjunction.genConj_pointwise {F : Frame} {σ τ : Ty} (f g : F.Denot (σ ⇒ τ)) : genConj (σ ⇒ τ) F f g = fun (x : F.Denot σ) => genConj τ F (f x) (g x)

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

theorem Core.Logic.Intensional.Conjunction.genConj_distributes_over_app {F : Frame} {σ τ : Ty} (f g : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : genConj (σ ⇒ τ) F f g x = genConj τ F (f x) (g x)

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

theorem Core.Logic.Intensional.Conjunction.genConj_lambda_distribution {F : Frame} {σ τ : Ty} (f g : F.Denot σ → F.Denot τ) : genConj (σ ⇒ τ) F f g = fun (v : F.Denot σ) => genConj τ F (f v) (g v)

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

theorem Core.Logic.Intensional.Conjunction.genDisj_distributes_over_app {F : Frame} {σ τ : Ty} (f g : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : genDisj (σ ⇒ τ) F f g x = genDisj τ F (f x) (g x)

theorem Core.Logic.Intensional.Conjunction.genDisj_lambda_distribution {F : Frame} {σ τ : Ty} (f g : F.Denot σ → F.Denot τ) : genDisj (σ ⇒ τ) F f g = fun (v : F.Denot σ) => genDisj τ F (f v) (g v)

def Core.Logic.Intensional.Conjunction.typeRaise {F : Frame} (e : F.Denot Ty.e) : F.Denot ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

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

Equations

• Core.Logic.Intensional.Conjunction.typeRaise e p = p e

def Core.Logic.Intensional.Conjunction.coordEntities {F : Frame} (e1 e2 : F.Denot Ty.e) : F.Denot ((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 Core.Logic.Intensional.Conjunction.typeRaise_preserves {F : Frame} (e : F.Denot Ty.e) (p : F.Denot (Ty.e ⇒ Ty.t)) : typeRaise e p = p e

theorem Core.Logic.Intensional.Conjunction.coordEntities_both_satisfy {F : Frame} (e1 e2 : F.Denot Ty.e) (p : F.Denot (Ty.e ⇒ Ty.t)) : coordEntities e1 e2 p = (p e1 ∧ p e2)

@cite{mitrovic-sauerland-2014} @cite{mitrovic-sauerland-2016} 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 Core.Logic.Intensional.Conjunction.msShift {F : Frame} (x : F.Denot Ty.e) : F.Denot (Ty.e ⇒ Ty.t)

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

Equations

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

@[reducible, inline]

abbrev Core.Logic.Intensional.Conjunction.inclFunc {F : Frame} (x : F.Denot Ty.e) : F.Denot ((Ty.e ⇒ Ty.t) ⇒ Ty.t)

MU particle semantics = typeRaise.

Equations

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

theorem Core.Logic.Intensional.Conjunction.ms_full_derivation {F : Frame} (e1 e2 : F.Denot Ty.e) : genConj ((Ty.e ⇒ Ty.t) ⇒ Ty.t) F (typeRaise e1) (typeRaise e2) = coordEntities e1 e2

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