The denotation of a coordinator

A coordinator denotes an operation on the set of its coordinands, which its semantic type fixes: the infimum of the set for a conjunctive or adversative coordinator, its supremum for a disjunctive one, and the complement of its supremum for a negative one. Coordinating two constituents is the case of a two-element set, so one operation conjoins truth values, predicates and generalized quantifiers, coordinates lists of any length, and builds the quantifiers that Japanese ka and mo form from indeterminate pronouns. The composition engine applies it to two sisters of one conjoinable type in Semantics/Composition/Coordination.lean.

Main definitions

• Coordinator.denote: what a coordinator denotes on a set of coordinands.

Main results

• Coordinator.denote_of_conjunctive and its siblings: the denotation by semantic type.
• Coordinator.denote_singleton, Coordinator.denote_pair_self: coordinating a constituent alone or with itself returns it, except under negative coordination.
• Coordinator.denote_apply: the coordination of functions is computed pointwise.

Implementation notes

The denotation is the truth-conditional content only. The contrast an adversative coordinator adds to conjunction is a relation between the coordinands in discourse, and denote_of_adversative records that it is invisible here. The operation needs a complete Boolean algebra, which the domain of every conjoinable type is, since such a type ends in t.

References

• [PR83]

def Coordinator.denote {α : Type u_1} [CompleteBooleanAlgebra α] (c : Coordinator) : Set α → α

On a set of coordinands a coordinator denotes their infimum if it is conjunctive or adversative, their supremum if it is disjunctive, and the complement of their supremum if it is negative.

Equations

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

theorem Coordinator.denote_of_conjunctive {α : Type u_1} [CompleteBooleanAlgebra α] {c : Coordinator} (h : c.role = Role.conjunctive) (s : Set α) : c.denote s = sInf s

theorem Coordinator.denote_of_disjunctive {α : Type u_1} [CompleteBooleanAlgebra α] {c : Coordinator} (h : c.role = Role.disjunctive) (s : Set α) : c.denote s = sSup s

theorem Coordinator.denote_of_negative {α : Type u_1} [CompleteBooleanAlgebra α] {c : Coordinator} (h : c.role = Role.negative) (s : Set α) : c.denote s = (sSup s)ᶜ

theorem Coordinator.denote_of_adversative {α : Type u_1} [CompleteBooleanAlgebra α] {c : Coordinator} (h : c.role = Role.adversative) (s : Set α) : c.denote s = sInf s

An adversative coordinator has the truth conditions of conjunction.

theorem Coordinator.denote_singleton {α : Type u_1} [CompleteBooleanAlgebra α] {c : Coordinator} (hc : c.role ≠ Role.negative) (p : α) : c.denote {p} = p

Coordinating a constituent alone returns it, except under negative coordination.

theorem Coordinator.denote_pair_self {α : Type u_1} [CompleteBooleanAlgebra α] {c : Coordinator} (hc : c.role ≠ Role.negative) (p : α) : c.denote {p, p} = p

Coordinating a constituent with itself returns it, except under negative coordination.

theorem Coordinator.denote_apply {α : Type u_1} [CompleteBooleanAlgebra α] {ι : Type u_2} (c : Coordinator) (s : Set (ι → α)) (i : ι) : c.denote s i = c.denote ((fun (x : ι → α) => x i) '' s)

The coordination of functions is computed pointwise.