Chatzikyriakidis & Luo (2017): On the interpretation of common nouns

Montague semantics interprets common nouns as predicates over a single type of entities, while the semantics of modern type theories, following Ranta, interprets them as types. The chapter argues that only types are compatible with the subtyping that copredication needs, as in "John picked up and mastered three books in the library". It turns judgements such as "John is a man" into propositions through a trivial predicate on each noun and a negation operator NOT governed by two laws, and checks the account in Coq. Gradable nouns such as idiot are Σ-types indexed by degree, which makes small idiot contradictory.

Main definitions

• p A: the trivial predicate on the noun A, the propositional form of a judgement a : A.
• NegOperator Obj: a negation operator NOT satisfying the laws (L1) and (L2).
• Idiot Human STND: the gradable noun idiot, a Σ-type indexed by degree.

Main statements

• standardNeg Obj: a model of the laws (L1) and (L2).
• man_and_not_man, not_not_man, notll, nothl, not_human_not_man: the chapter's Coq examples, proved from the laws.
• no_aspect_map: in general no map adds an informational aspect to a physical object.
• small_idiot_contradictory: no degree is both above and below the standard.

Implementation notes

• A noun is an object A of Over Obj, a type A.left with an embedding A.hom into the type Obj of all objects, the chapter's top type. A coercion from A to B is a morphism A ⟶ B of Over Obj.
• The chapter introduces NOT through Coq parameters without exhibiting a model; standardNeg is our model.

References

• S. Chatzikyriakidis and Z. Luo, On the Interpretation of Common Nouns: Types Versus Predicates (2017)
• R. Montague, The Proper Treatment of Quantification in Ordinary English (1973)
• A. Ranta, Type-Theoretical Grammar (1994)
• N. Asher, Lexical Meaning in Context: A Web of Words (2011)

@[simp]

theorem ChatzikyriakidisLuo2017.over_w_apply {Obj : Type u} {A B : CategoryTheory.Over Obj} (s : A ⟶ B) (a : A.left) : (CategoryTheory.ConcreteCategory.hom B.hom) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left s)) a) = (CategoryTheory.ConcreteCategory.hom A.hom) a

A coercion commutes with the embeddings of the two nouns.

def ChatzikyriakidisLuo2017.p {Obj : Type u} (A : CategoryTheory.Over Obj) : A.left → Prop

The trivial predicate on a noun, true of all its objects, the propositional form of a judgement a : A (Definition 1).

Equations

• ChatzikyriakidisLuo2017.p A x✝ = True

structure ChatzikyriakidisLuo2017.NegOperator (Obj : Type u) : Type (u + 1)

A negation operator NOT, saying that an object does not satisfy a predicate on a noun, with the laws (L1) and (L2) for the trivial predicates.

• not (A : CategoryTheory.Over Obj) : (A.left → Prop) → Obj → Prop

  The negation operator.

• l1 (A : CategoryTheory.Over Obj) (a : A.left) : self.not A (p A) ((CategoryTheory.ConcreteCategory.hom A.hom) a) ↔ ¬p A a

  An object of A does not satisfy p A exactly when it is not an A, law (L1).

• l2 {A B : CategoryTheory.Over Obj} : ∀ (a : A ⟶ B) (c : Obj), self.not B (p B) c → self.not A (p A) c

  What is not a B is not an A, along a coercion from A to B, law (L2).

def ChatzikyriakidisLuo2017.NegOperator.bigP {Obj : Type u} (N : NegOperator Obj) (A : CategoryTheory.Over Obj) (o : Obj) : Prop

The predicate P_A of a hypothetical judgement, the negation of NOT at p A, as in "if John is a student, he is happy" (Definition 2).

Equations

• N.bigP A o = ¬N.not A (ChatzikyriakidisLuo2017.p A) o

def ChatzikyriakidisLuo2017.standardNeg (Obj : Type u) : NegOperator Obj

The operator under which an object does not satisfy P when no object of A located at it does.

Equations

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

The Coq examples

Each theorem is one of the chapter's Coq examples, proved from the laws of NOT.

theorem ChatzikyriakidisLuo2017.man_and_not_man {Obj : Type u} (N : NegOperator Obj) (Man : CategoryTheory.Over Obj) (j : Man.left) : ¬(p Man j ∧ N.not Man (p Man) ((CategoryTheory.ConcreteCategory.hom Man.hom) j))

"John is a man and John is not a man" is contradictory ((25)–(27)).

theorem ChatzikyriakidisLuo2017.not_not_man {Obj : Type u} (N : NegOperator Obj) (Man : CategoryTheory.Over Obj) (j : Man.left) : ¬N.not Man (p Man) ((CategoryTheory.ConcreteCategory.hom Man.hom) j)

It is not the case that John, a man, is not a man ((34)–(36)).

theorem ChatzikyriakidisLuo2017.tables_dont_talk_red {Obj : Type u} (N : NegOperator Obj) (Human Table : CategoryTheory.Over Obj) (Red : Obj → Prop) (talk : Human.left → Prop) (h : ∀ (x : Table.left), N.not Human talk ((CategoryTheory.ConcreteCategory.hom Table.hom) x)) (y : { x : Table.left // Red ((CategoryTheory.ConcreteCategory.hom Table.hom) x) }) : N.not Human talk ((CategoryTheory.ConcreteCategory.hom Table.hom) ↑y)

"Tables do not talk" entails "red tables do not talk", by the coercion from red tables to tables alone ((31)–(33)).

theorem ChatzikyriakidisLuo2017.notll {Obj : Type u} (N : NegOperator Obj) (Linguist Logician : CategoryTheory.Over Obj) (h : ¬∀ (l : Linguist.left), N.bigP Logician ((CategoryTheory.ConcreteCategory.hom Linguist.hom) l)) : ∃ (l : Linguist.left), N.not Logician (p Logician) ((CategoryTheory.ConcreteCategory.hom Linguist.hom) l)

"It is not the case that every linguist is a logician" entails "some linguist is not a logician" ((47)–(49)).

theorem ChatzikyriakidisLuo2017.nothl {Obj : Type u} (N : NegOperator Obj) (Human Linguist Logician : CategoryTheory.Over Obj) (s : Linguist ⟶ Human) (h : ¬∀ (l : Linguist.left), N.bigP Logician ((CategoryTheory.ConcreteCategory.hom Linguist.hom) l)) : ¬∀ (x : Human.left), N.bigP Logician ((CategoryTheory.ConcreteCategory.hom Human.hom) x)

"Not every linguist is a logician" entails "not every human is a logician", along a coercion from linguists to humans ((50)–(52)).

theorem ChatzikyriakidisLuo2017.not_human_not_man {Obj : Type u} (N : NegOperator Obj) (Man Human : CategoryTheory.Over Obj) (s : Man ⟶ Human) (c : Obj) (h : N.not Human (p Human) c) : N.not Man (p Man) c

"If John is not a human, then John is not a man", which is law (L2) ((53)–(55)).

theorem ChatzikyriakidisLuo2017.some_man_walks {Obj : Type u} (Man Human : CategoryTheory.Over Obj) (s : Man ⟶ Human) (walk : Human.left → Prop) (j : Man.left) (h : walk ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left s)) j)) : ∃ (x : Man.left), walk ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left s)) x)

"John walks" entails "some man walks", for John a man.

Copredication

Interpreting book as a predicate over the dot type Phy • Info would need Phy ≤ Phy • Info, the wrong direction. With nouns as types, Book ≤ Phy • Info gives both aspects of a book.

theorem ChatzikyriakidisLuo2017.no_aspect_map {Phy : Type u_1} {Info : Type u_2} (hp : Nonempty Phy) (hi : IsEmpty Info) : IsEmpty (Phy → Phy × Info)

When some physical object exists and no informational one does, no map adds an informational aspect to a physical object (§2.2).

def ChatzikyriakidisLuo2017.copredication {Phy : Type u_1} {Info : Type u_2} {Book : Type u_3} (toPhy : Book → Phy) (toInfo : Book → Info) (pickUp : Phy → Prop) (master : Info → Prop) (b : Book) : Prop

The copredication "picked up and mastered" of a book, through its physical and informational aspects (5).

Equations

• ChatzikyriakidisLuo2017.copredication toPhy toInfo pickUp master b = (pickUp (toPhy b) ∧ master (toInfo b))

Gradable nouns

Nouns may be families indexed by degrees (58), whose order the chapter axiomatizes as a dense linear order.

structure ChatzikyriakidisLuo2017.Idiot {Idiocy : Type u_1} [LinearOrder Idiocy] (Human : Idiocy → Type u_2) (STND : Idiocy) : Type (max u_1 u_2)

An idiot is a human together with an idiocy degree above the standard (62).

• degree : Idiocy

  The idiocy degree.

• human : Human self.degree

  The human indexed at that degree.

• above : STND < self.degree

  The degree exceeds the standard.

theorem ChatzikyriakidisLuo2017.small_idiot_contradictory {Idiocy : Type u_1} [LinearOrder Idiocy] (STND : Idiocy) : ¬∃ (i : Idiocy), STND < i ∧ i < STND

No degree is both above and below the standard, so small idiot is contradictory.