Mereology of relations

Krifka states his conditions on the thematic relation between an object and an event as part-structure properties of a relation θ : α → β → Prop between two mereologies. Uniqueness of participants and of events are mathlib's Relator.LeftUnique and Relator.RightUnique, summativity is cumulativity of the graph of θ in the product order, and the mapping and uniqueness conditions relate the parts of a related object to the parts of its event. Each condition on the event side is the object-side condition of the converse relation flip θ. When the relation is the graph of a thematic function, as in [CK16], the conditions become properties of the function: summativity is preservation of sums, general uniqueness of events is injectivity, and mapping to subobjects is strict monotonicity.

Main definitions

• UP, GUE: uniqueness of participants and general uniqueness of events.
• SUM: summativity, the cumulativity of a relation.
• ME, MSE, UE: mapping to events, mapping to subevents, and uniqueness of events.
• MO, MSO, UO: mapping to objects, mapping to subobjects, and uniqueness of objects.

Main results

• UP.uo_of_mo, UE.mse_of_uo: uniqueness of participants gives uniqueness of objects, and the two uniqueness conditions give the strict mappings.
• UE.exists_orderIso_of_uo: under both uniqueness conditions a related object and event have order-isomorphic parts.
• UO.qua_of_mso: the events of a fixed object form a quantized predicate.
• gue_graph_iff, mso_graph_iff, sum_graph_iff: the conditions on the graph of a thematic function.

References

• [Kri89], [Kri98], [CK16]

Uniqueness of participants and events

@[reducible, inline]

abbrev Mereology.UP {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) : Prop

A relation has unique participants if an event has at most one θ-participant.

Equations

• Mereology.UP θ = Relator.LeftUnique θ

@[reducible, inline]

abbrev Mereology.GUE {α : Type u_1} {β : Type u_2} (θ : α → β → Prop) : Prop

A relation has general uniqueness of events if an object participates in at most one θ-event.

Equations

• Mereology.GUE θ = Relator.RightUnique θ

theorem Mereology.UP.flip {α : Type u_1} {β : Type u_2} {θ : α → β → Prop} (h : UP θ) : GUE (_root_.flip θ)

theorem Mereology.GUE.flip {α : Type u_1} {β : Type u_2} {θ : α → β → Prop} (h : GUE θ) : UP (_root_.flip θ)

Summativity

def Mereology.SUM {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (θ : α → β → Prop) : Prop

A relation is summative ([Kri89]), or cumulative in the sense of [Kri98], if related pairs sum to related pairs.

Equations

• Mereology.SUM θ = ∀ ⦃x : α⦄ ⦃e : β⦄, θ x e → ∀ ⦃y : α⦄ ⦃e' : β⦄, θ y e' → θ (x ⊔ y) (e ⊔ e')

theorem Mereology.sum_iff_cum_uncurry {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} : SUM θ ↔ CUM (Function.uncurry θ)

Summativity is cumulativity of the graph of θ in the product order.

theorem Mereology.SUM.flip {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {θ : α → β → Prop} (h : SUM θ) : SUM (_root_.flip θ)

Mapping between parts

def Mereology.ME {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (θ : α → β → Prop) : Prop

A relation maps to events if a part of a related object is related to a part of the event.

Equations

• Mereology.ME θ = ∀ ⦃x : α⦄ ⦃e : β⦄, θ x e → ∀ ⦃y : α⦄, y ≤ x → ∃ e' ≤ e, θ y e'

def Mereology.MSE {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (θ : α → β → Prop) : Prop

A relation maps to subevents if a proper part of a related object is related to a proper part of the event.

Equations

• Mereology.MSE θ = ∀ ⦃x : α⦄ ⦃e : β⦄, θ x e → ∀ ⦃y : α⦄, y < x → ∃ e' < e, θ y e'

def Mereology.UE {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (θ : α → β → Prop) : Prop

A relation has unique events if a part of a related object is related to exactly one part of the event.

Equations

• Mereology.UE θ = ∀ ⦃x : α⦄ ⦃e : β⦄, θ x e → ∀ ⦃y : α⦄, y ≤ x → ∃! e' : β, e' ≤ e ∧ θ y e'

@[reducible, inline]

abbrev Mereology.MO {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (θ : α → β → Prop) : Prop

A relation maps to objects if a part of a related event is related to a part of the object, the converse of ME.

Equations

• Mereology.MO θ = Mereology.ME (flip θ)

@[reducible, inline]

abbrev Mereology.MSO {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (θ : α → β → Prop) : Prop

A relation maps to subobjects if a proper part of a related event is related to a proper part of the object, the converse of MSE.

Equations

• Mereology.MSO θ = Mereology.MSE (flip θ)

@[reducible, inline]

abbrev Mereology.UO {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] (θ : α → β → Prop) : Prop

A relation has unique objects if a part of a related event is related to exactly one part of the object, the converse of UE.

Equations

• Mereology.UO θ = Mereology.UE (flip θ)

theorem Mereology.UE.me {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {θ : α → β → Prop} (h : UE θ) : ME θ

theorem Mereology.UO.mo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {θ : α → β → Prop} (h : UO θ) : MO θ

theorem Mereology.UP.uo_of_mo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {θ : α → β → Prop} (hU : UP θ) (hm : MO θ) : UO θ

With mapping to objects, uniqueness of participants gives uniqueness of objects.

theorem Mereology.GUE.ue_of_me {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {θ : α → β → Prop} (hG : GUE θ) (hm : ME θ) : UE θ

With mapping to events, general uniqueness of events gives uniqueness of events.

theorem Mereology.MSE.me {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {θ : α → β → Prop} (h : MSE θ) : ME θ

theorem Mereology.MSO.mo {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {θ : α → β → Prop} (h : MSO θ) : MO θ

theorem Mereology.UE.mse_of_uo {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {θ : α → β → Prop} (hE : UE θ) (hO : UO θ) : MSE θ

Uniqueness of events and of objects give mapping to subevents. The part of the event related to a proper part of the object is proper, since the whole event's unique related part of the object is the object itself.

theorem Mereology.UO.mso_of_ue {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {θ : α → β → Prop} (hO : UO θ) (hE : UE θ) : MSO θ

Uniqueness of objects and of events give mapping to subobjects.

theorem Mereology.UO.qua_of_mso {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {θ : α → β → Prop} (hO : UO θ) (hm : MSO θ) (x : α) : QUA (θ x)

With unique objects and mapping to subobjects, the events of a fixed object form a quantized predicate, since it takes the whole event to θ the object. [Kri98] draws this consequence after (50) from uniqueness of objects alone, which does not suffice, since a relation holding of one object and every event has unique objects.

The correspondence between parts

theorem Mereology.UE.exists_orderIso_of_uo {α : Type u_1} {β : Type u_2} [Preorder α] [Preorder β] {θ : α → β → Prop} {x : α} {e : β} (hE : UE θ) (hO : UO θ) (hxe : θ x e) : ∃ (f : ↑(Set.Iic x) ≃o ↑(Set.Iic e)), ∀ (y : ↑(Set.Iic x)) (e' : ↑(Set.Iic e)), θ ↑y ↑e' ↔ f y = e'

Under uniqueness of events and of objects, θ restricts, between the parts of a related object and event, to the graph of an order isomorphism.

Thematic functions

A thematic function f : β → α sends an event to its participant, and its graph (· = f ·) is the corresponding thematic relation. [CK16] require of such a function cumulativity (13.23), that it preserve sums, and distinctiveness (13.24), that distinct events have distinct participants.

theorem Mereology.up_graph {α : Type u_1} {β : Type u_2} (f : β → α) : UP fun (x1 : α) (x2 : β) => x1 = f x2

The graph of a function has unique participants.

theorem Mereology.gue_graph_iff {α : Type u_1} {β : Type u_2} (f : β → α) : (GUE fun (x1 : α) (x2 : β) => x1 = f x2) ↔ Function.Injective f

The graph of a function has general uniqueness of events iff the function is injective, the distinctiveness (13.24) of [CK16].

theorem Mereology.mo_graph_iff {α : Type u_1} {β : Type u_2} (f : β → α) [Preorder α] [Preorder β] : (MO fun (x1 : α) (x2 : β) => x1 = f x2) ↔ Monotone f

The graph of a function maps to objects iff the function is monotone.

theorem Mereology.uo_graph_iff {α : Type u_1} {β : Type u_2} (f : β → α) [Preorder α] [Preorder β] : (UO fun (x1 : α) (x2 : β) => x1 = f x2) ↔ Monotone f

The graph of a function has unique objects iff the function is monotone.

theorem Mereology.mso_graph_iff {α : Type u_1} {β : Type u_2} (f : β → α) [Preorder α] [Preorder β] : (MSO fun (x1 : α) (x2 : β) => x1 = f x2) ↔ StrictMono f

The graph of a function maps to subobjects iff the function is strictly monotone.

theorem Mereology.sum_graph_iff {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (f : β → α) : (SUM fun (x1 : α) (x2 : β) => x1 = f x2) ↔ ∀ (e e' : β), f (e ⊔ e') = f e ⊔ f e'

The graph of a function is summative iff the function preserves sums, the cumulativity (13.23) of [CK16].

theorem Mereology.sum_graph {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {F : Type u_3} [FunLike F β α] [SupHomClass F β α] (f : F) : SUM fun (x1 : α) (x2 : β) => x1 = f x2

The graph of a sum homomorphism is summative.