Chatzikyriakidis & Luo (2020): Formal semantics in modern type theories

In the formal semantics of modern type theories, common nouns are interpreted as types rather than predicates, and subtyping is coercive: one noun is a subtype of another when a unique coercion between them may be inserted wherever an object of the second is expected. A noun modified by a predicate is the Σ-type of its objects satisfying the predicate, a subtype of the noun through the first projection. This file formalizes the book's classification of adjectival modification, its operator NOT for the propositional forms of judgements, and its identity criteria for counting.

The book's Theorem 7.1 states that the laws (A1)–(A5) of NOT are provable once NOT is defined from the heterogeneous equality JMeq. We show that with Lean's heterogeneous equality, which validates the rules of JMeq, (A1) and (A2) hold but (A3), (A4) and (A5) fail at every proper finite Σ-subtype, such as the men among the humans. With heterogeneous equality read as equality in a common carrier, all five laws hold.

Main definitions

• sigma A P: the Σ-type of the objects of A satisfying P, a subtype of A by sigmaFst A P.
• DoesNot A P B b: the operator NOT, from which Is and Does define IS and DO.
• TypeDisjoint A B: no inhabited noun is a subtype of both A and B.
• SubSetoid A B sA sB: A is a subtype of B whose identity criterion sA is inherited from sB.

Main statements

• range_sigma_comp: intersective modification meets the noun's extension with the adjective's.
• not_forall_nonempty_hom_sigma: subsective modification need not respect subtyping.
• forall_does_iff_mono: law (A1) holds on a noun exactly when its embedding is a monomorphism.
• not_doesNot_comp_heq, not_forall_doesNot_of_sub_heq, not_exists_doesNot_of_sub_heq: laws (A3), (A4) and (A5) fail for HEq.
• three₀_iff_two_lt_card: three objects distinct under an identity criterion satisfy a predicate exactly when more than two of its identity classes do.

Implementation notes

• As in [CL17a], a noun is an object of Over Obj, a type embedded in a type Obj of all objects, and a coercion is a morphism of Over Obj. The book's universe has no such Obj; here it supplies the heterogeneous equality, under which two objects are equal when their images are. This equality identifies an object with its image under a coercion, the axiom that [XLC18] add to prove (A3)–(A5).
• Coercions are morphisms rather than Coe instances, so that statements quantify over nouns.
• By propositional extensionality every modal collection Prop → Prop respects logical equivalence, the property for which the book rejects the belief contexts of [Ran94].

TODO

• Gradable, multidimensional and adverbial modification.
• Dot-types for copredication, and counting under copredication.
• Negative occurrences (Definition 7.2) and dependent event types.
• A universe without the type Obj, with coercions along a directed order.

References

• S. Chatzikyriakidis and Z. Luo, Formal Semantics in Modern Type Theories (2020)
• S. Chatzikyriakidis and Z. Luo, On the Interpretation of Common Nouns: Types Versus Predicates (2017)
• T. Xue, Z. Luo and S. Chatzikyriakidis, Propositional Forms of Judgemental Interpretations (2018)
• H. Kamp, Two theories about adjectives (1975)
• B. H. Partee, Privative adjectives: Subsective plus coercion (2010)
• A. Ranta, Type-Theoretical Grammar (1994)

Σ-types and coercive subtyping

def ChatzikyriakidisLuo2020.sigma {Obj : Type u} (A : CategoryTheory.Over Obj) (P : A.left → Prop) : CategoryTheory.Over Obj

The Σ-type of the objects of A satisfying P, located through A ((2.41), (3.21)).

Equations

• ChatzikyriakidisLuo2020.sigma A P = CategoryTheory.Over.mk (TypeCat.ofHom fun (x : { x : A.left // P x }) => (CategoryTheory.ConcreteCategory.hom A.hom) ↑x)

def ChatzikyriakidisLuo2020.sigmaFst {Obj : Type u} (A : CategoryTheory.Over Obj) (P : A.left → Prop) : sigma A P ⟶ A

The first projection, which makes a modified noun a subtype of the noun ((2.42), (3.33)).

Equations

• ChatzikyriakidisLuo2020.sigmaFst A P = CategoryTheory.Over.homMk (TypeCat.ofHom Subtype.val) ⋯

instance ChatzikyriakidisLuo2020.mono_sigma_hom {Obj : Type u} (A : CategoryTheory.Over Obj) (P : A.left → Prop) [CategoryTheory.Mono A.hom] : CategoryTheory.Mono (sigma A P).hom

A Σ-type embeds injectively when its noun does, since by proof irrelevance two of its objects are equal when their first projections are (p. 69).

theorem ChatzikyriakidisLuo2020.subsingleton_hom {Obj : Type u} {A B : CategoryTheory.Over Obj} [CategoryTheory.Mono B.hom] : Subsingleton (A ⟶ B)

Coercions into a noun with a monic embedding are unique, as coherence requires (p. 40).

theorem ChatzikyriakidisLuo2020.mono_left {Obj : Type u} {A B : CategoryTheory.Over Obj} [CategoryTheory.Mono A.hom] (s : A ⟶ B) : CategoryTheory.Mono (CategoryTheory.Over.Hom.left s)

A coercion out of a noun with a monic embedding is monic.

Adjectival modification

def ChatzikyriakidisLuo2020.sigmaMap {Obj : Type u} {A B : CategoryTheory.Over Obj} (s : A ⟶ B) (adj : Obj → Prop) : sigma A (adj ∘ ⇑(CategoryTheory.ConcreteCategory.hom A.hom)) ⟶ sigma B (adj ∘ ⇑(CategoryTheory.ConcreteCategory.hom B.hom))

Intersective modification respects subtyping, so a black cat is a black object (3.91).

Equations

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

theorem ChatzikyriakidisLuo2020.range_sigma_comp {Obj : Type u} (A : CategoryTheory.Over Obj) (adj : Obj → Prop) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (sigma A (adj ∘ ⇑(CategoryTheory.ConcreteCategory.hom A.hom))).hom) = Modifier.intersective {o : Obj | adj o} (Set.range ⇑(CategoryTheory.ConcreteCategory.hom A.hom))

The extension of an intersectively modified noun is the meet of the noun's extension with the adjective's, the intersective class of [Kam75] ((3.92)–(3.97)).

theorem ChatzikyriakidisLuo2020.not_forall_nonempty_hom_sigma : ¬∀ (A B : CategoryTheory.Over Bool) (x : A ⟶ B) (adj : (C : CategoryTheory.Over Bool) → C.left → Prop), Nonempty (sigma A (adj A) ⟶ sigma B (adj B))

Since the instances of a Π-polymorphic adjective at two nouns are unrelated, a subtyping need not lift to the modified nouns (3.101).

Privative adjectives are subsective over the disjoint union of real and fake guns, as [Par10] proposes.

def ChatzikyriakidisLuo2020.sum {Obj : Type u} (A B : CategoryTheory.Over Obj) : CategoryTheory.Over Obj

The disjoint union of two nouns, as in the type of guns G = G_R + G_F (3.110).

Equations

• ChatzikyriakidisLuo2020.sum A B = CategoryTheory.Over.mk (TypeCat.ofHom (Sum.elim ⇑(CategoryTheory.ConcreteCategory.hom A.hom) ⇑(CategoryTheory.ConcreteCategory.hom B.hom)))

def ChatzikyriakidisLuo2020.IsReal {Obj : Type u} {GR GF : CategoryTheory.Over Obj} : (sum GR GF).left → Prop

A gun is real when it comes from the real guns (3.111).

Equations

• ChatzikyriakidisLuo2020.IsReal = Sum.elim (fun (x : GR.left) => True) fun (x : GF.left) => False

def ChatzikyriakidisLuo2020.IsFake {Obj : Type u} {GR GF : CategoryTheory.Over Obj} : (sum GR GF).left → Prop

A gun is fake when it comes from the fake guns (3.112).

Equations

• ChatzikyriakidisLuo2020.IsFake = Sum.elim (fun (x : GR.left) => False) fun (x : GF.left) => True

theorem ChatzikyriakidisLuo2020.isReal_or_isFake {Obj : Type u} {GR GF : CategoryTheory.Over Obj} (g : (sum GR GF).left) : IsReal g ∨ IsFake g

Every gun is real or fake (3.120).

theorem ChatzikyriakidisLuo2020.isReal_iff_not_isFake {Obj : Type u} {GR GF : CategoryTheory.Over Obj} (g : (sum GR GF).left) : IsReal g ↔ ¬IsFake g

A gun is real exactly when it is not fake (p. 71).

theorem ChatzikyriakidisLuo2020.not_isReal_sigmaFst {Obj : Type u} {GR GF : CategoryTheory.Over Obj} (f : (sigma (sum GR GF) IsFake).left) : ¬IsReal ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left (sigmaFst (sum GR GF) IsFake))) f)

A fake gun is not a real gun (3.121).

theorem ChatzikyriakidisLuo2020.disjoint_range_isFake {Obj : Type u} {GR GF : CategoryTheory.Over Obj} [CategoryTheory.Mono (sum GR GF).hom] : Disjoint (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (sigma (sum GR GF) IsFake).hom)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom (sigma (sum GR GF) IsReal).hom))

When no object is both a real and a fake gun, fake guns and real guns have disjoint extensions, so fake is privative relative to real gun (p. 72).

Propositional forms of judgements

def ChatzikyriakidisLuo2020.DoesNot {Obj : Type u} (A : CategoryTheory.Over Obj) (P : A.left → Prop) (B : CategoryTheory.Over Obj) (b : B.left) : Prop

The operator NOT, read "b does not P", defined from heterogeneous equality as equality of images in Obj ((7.5), (7.11)).

Equations

• ChatzikyriakidisLuo2020.DoesNot A P B b = ∀ (x : A.left), (CategoryTheory.ConcreteCategory.hom A.hom) x = (CategoryTheory.ConcreteCategory.hom B.hom) b → ¬P x

def ChatzikyriakidisLuo2020.Is {Obj : Type u} {B : CategoryTheory.Over Obj} (X : CategoryTheory.Over Obj) (y : B.left) : Prop

The operator IS, the propositional form of the judgement that y is an X (7.7).

Equations

• ChatzikyriakidisLuo2020.Is X y = ¬ChatzikyriakidisLuo2020.DoesNot X (ChatzikyriakidisLuo2017.p X) B y

def ChatzikyriakidisLuo2020.Does {Obj : Type u} {A B : CategoryTheory.Over Obj} (P : A.left → Prop) (y : B.left) : Prop

The operator DO, the propositional form of applying P to y (7.9).

Equations

• ChatzikyriakidisLuo2020.Does P y = ¬ChatzikyriakidisLuo2020.DoesNot A P B y

theorem ChatzikyriakidisLuo2020.does_iff {Obj : Type u} {A B : CategoryTheory.Over Obj} {P : A.left → Prop} {y : B.left} : Does P y ↔ ∃ (x : (fun (X : Type u) => X) A.left), (CategoryTheory.ConcreteCategory.hom A.hom) x = (CategoryTheory.ConcreteCategory.hom B.hom) y ∧ P x

theorem ChatzikyriakidisLuo2020.is_iff {Obj : Type u} {A B : CategoryTheory.Over Obj} {y : B.left} : Is A y ↔ ∃ (x : (fun (X : Type u) => X) A.left), (CategoryTheory.ConcreteCategory.hom A.hom) x = (CategoryTheory.ConcreteCategory.hom B.hom) y

theorem ChatzikyriakidisLuo2020.is_self {Obj : Type u} {A : CategoryTheory.Over Obj} (a : A.left) : Is A a

IS holds of every object of its own noun (p. 64).

theorem ChatzikyriakidisLuo2020.forall_does_iff_mono {Obj : Type u} {A : CategoryTheory.Over Obj} : (∀ (P : A.left → Prop) (x : A.left), Does P x ↔ P x) ↔ CategoryTheory.Mono A.hom

Law (A1) holds on a noun exactly when its embedding is a monomorphism (p. 153).

theorem ChatzikyriakidisLuo2020.doesNot_mono {Obj : Type u} {A B : CategoryTheory.Over Obj} {P Q : A.left → Prop} (h : ∀ (x : A.left), P x → Q x) (y : B.left) (hQ : DoesNot A Q B y) : DoesNot A P B y

If P implies Q, not doing Q implies not doing P, which is law (A2).

theorem ChatzikyriakidisLuo2020.doesNot_comp {Obj : Type u} {A B C : CategoryTheory.Over Obj} (s : A ⟶ B) (P : B.left → Prop) (z : C.left) (h : DoesNot B P C z) : DoesNot A (P ∘ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left s))) C z

Along a coercion, not doing P as a B implies not doing it as an A, which is law (A3).

theorem ChatzikyriakidisLuo2020.forall_doesNot_of_hom {Obj : Type u} {A B C : CategoryTheory.Over Obj} (s : A ⟶ B) (P : C.left → Prop) (h : ∀ (y : B.left), DoesNot C P B y) (x : A.left) : DoesNot C P A x

What no B does, no A does, which is law (A4).

theorem ChatzikyriakidisLuo2020.exists_doesNot_of_hom {Obj : Type u} {A B C : CategoryTheory.Over Obj} (s : A ⟶ B) (P : C.left → Prop) (h : ∃ (x : A.left), DoesNot C P A x) : ∃ (y : B.left), DoesNot C P B y

What some A does not do, some B does not do, which is law (A5).

theorem ChatzikyriakidisLuo2020.is_of_hom {Obj : Type u} {A B C : CategoryTheory.Over Obj} (s : A ⟶ B) {z : C.left} (h : Is A z) : Is B z

IS respects subtyping, as in the inference from "Teddy is a man" to "Teddy is a human" (p. 154).

theorem ChatzikyriakidisLuo2020.standardNeg_not_iff {Obj : Type u} {A B : CategoryTheory.Over Obj} (P : A.left → Prop) (b : B.left) : (ChatzikyriakidisLuo2017.standardNeg Obj).not A P ((CategoryTheory.ConcreteCategory.hom B.hom) b) ↔ DoesNot A P B b

The negation operator of [CL17a] is NOT with its object read in Obj.

def ChatzikyriakidisLuo2020.TypeDisjoint {Obj : Type u} (A B : CategoryTheory.Over Obj) : Prop

Two nouns are disjoint when no inhabited noun is a subtype of both (Definition 7.1).

Equations

• ChatzikyriakidisLuo2020.TypeDisjoint A B = ∀ (C : CategoryTheory.Over Obj) (a : C ⟶ A) (a : C ⟶ B), IsEmpty C.left

theorem ChatzikyriakidisLuo2020.typeDisjoint_iff {Obj : Type u} {A B : CategoryTheory.Over Obj} : TypeDisjoint A B ↔ ∀ (b : B.left), ¬Is A b

Two nouns are disjoint exactly when no object of the second is an object of the first, so that "John is not a table" holds of every man ((3.66), (3.71)).

theorem ChatzikyriakidisLuo2020.isEmpty_hom_of_typeDisjoint {Obj : Type u} {A B : CategoryTheory.Over Obj} (h : TypeDisjoint A B) [Nonempty A.left] : IsEmpty (A ⟶ B)

No coercion leads from an inhabited noun to a disjoint one, so talk(t) is ill-typed for a table t ((3.5)–(3.7)).

def ChatzikyriakidisLuo2020.Alleged {Obj : Type u} {Hum : CategoryTheory.Over Obj} (H : Hum.left → Prop → Prop) (M : CategoryTheory.Over Obj) (x : Hum.left) : Prop

An object is an alleged M when someone's collection of allegations contains that it is an M (3.125).

Equations

• ChatzikyriakidisLuo2020.Alleged H M x = ∃ (h : Hum.left), H h (ChatzikyriakidisLuo2020.Is M x)

theorem ChatzikyriakidisLuo2020.alleged_noncommittal {Obj : Type u} {Hum M : CategoryTheory.Over Obj} {x y : Hum.left} (hx : ¬Is M x) (hy : Is M y) : (∃ (H : Hum.left → Prop → Prop), Alleged H M x ∧ ¬Is M x) ∧ ∃ (H : Hum.left → Prop → Prop), Alleged H M y ∧ Is M y

An alleged M need not be an M, and an M may be alleged (3.122).

NOT with Lean's heterogeneous equality

def ChatzikyriakidisLuo2020.HDoesNot {A B : Type} (P : A → Prop) (b : B) : Prop

The operator NOT defined as in (7.11), with HEq for JMeq.

Equations

• ChatzikyriakidisLuo2020.HDoesNot P b = ∀ (x : A), x ≍ b → ¬P x

theorem ChatzikyriakidisLuo2020.not_hDoesNot_self_iff {A : Type} {P : A → Prop} {x : A} : ¬HDoesNot P x ↔ P x

Law (A1) holds for HDoesNot.

theorem ChatzikyriakidisLuo2020.hDoesNot_mono {A B : Type} {P Q : A → Prop} (h : ∀ (x : A), P x → Q x) {y : B} (hQ : HDoesNot Q y) : HDoesNot P y

Law (A2) holds for HDoesNot.

theorem ChatzikyriakidisLuo2020.hDoesNot_of_ne {A B : Type} (h : A ≠ B) (P : A → Prop) (b : B) : HDoesNot P b

NOT holds vacuously between distinct types, since HEq entails type equality.

theorem ChatzikyriakidisLuo2020.subtype_ne {α : Type} [Fintype α] {M : α → Prop} [DecidablePred M] (h : ∃ (a : α), ¬M a) : { a : α // M a } ≠ α

A proper Σ-subtype of a finite type is a different type.

theorem ChatzikyriakidisLuo2020.not_doesNot_comp_heq {α : Type} [Fintype α] {M : α → Prop} [DecidablePred M] (h : ∃ (a : α), ¬M a) (m : { a : α // M a }) : ¬∀ (P : α → Prop) (C : Type) (z : C), HDoesNot P z → HDoesNot (P ∘ Subtype.val) z

Law (A3) fails for HDoesNot at a proper finite Σ-subtype, such as the men among the humans.

theorem ChatzikyriakidisLuo2020.not_forall_doesNot_of_sub_heq {α : Type} [Fintype α] {M : α → Prop} [DecidablePred M] (h : ∃ (a : α), ¬M a) (m : { a : α // M a }) : ¬∀ (C : Type) (P : C → Prop), (∀ (y : α), HDoesNot P y) → ∀ (x : { a : α // M a }), HDoesNot P x

Law (A4) fails for HDoesNot at a proper finite Σ-subtype.

theorem ChatzikyriakidisLuo2020.not_exists_doesNot_of_sub_heq {α : Type} [Fintype α] {M : α → Prop} [DecidablePred M] (h : ∃ (a : α), ¬M a) (m : { a : α // M a }) : ¬∀ (C : Type) (P : C → Prop), (∃ (x : { a : α // M a }), HDoesNot P x) → ∃ (y : α), HDoesNot P y

Law (A5) fails for HDoesNot at a proper finite Σ-subtype.

theorem ChatzikyriakidisLuo2020.not_heq_val {α : Type} [Fintype α] {M : α → Prop} [DecidablePred M] (h : ∃ (a : α), ¬M a) (x : { a : α // M a }) : ¬x ≍ ↑x

The axiom of [XLC18] identifying an object with its image under a coercion fails for HEq at a proper finite Σ-subtype.

Identity criteria and counting

structure ChatzikyriakidisLuo2020.SubSetoid {Obj : Type u} (A B : CategoryTheory.Over Obj) (sA : Setoid A.left) (sB : Setoid B.left) : Type u

A sub-setoid is a subtype whose identity criterion is the restriction of the supertype's (Definition 5.2).

• sub : A ⟶ B

  The coercion from A to B.

• comap_eq : sA = Setoid.comap (⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left self.sub))) sB

  The identity criterion of A is that of B restricted along the coercion.

def ChatzikyriakidisLuo2020.Three₀ {Obj : Type u} (B : CategoryTheory.Over Obj) (sB : Setoid B.left) (P : B.left → Prop) : Prop

Three₀ B sB P holds when three objects of B, pairwise distinct under sB, satisfy P (Definition 5.3).

Equations

• ChatzikyriakidisLuo2020.Three₀ B sB P = ∃ (x : B.left) (y : B.left) (z : B.left), ¬sB x y ∧ ¬sB y z ∧ ¬sB x z ∧ P x ∧ P y ∧ P z

theorem ChatzikyriakidisLuo2020.three₀_of_subSetoid {Obj : Type u} {A B : CategoryTheory.Over Obj} {sA : Setoid A.left} {sB : Setoid B.left} (h : SubSetoid A B sA sB) (P : B.left → Prop) (hA : Three₀ A sA (P ∘ ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Over.Hom.left h.sub)))) : Three₀ B sB P

If men inherit the identity criterion of humans, three men who talk are three humans who talk (5.26).

theorem ChatzikyriakidisLuo2020.three₀_iff_two_lt_card {Obj : Type u} {B : CategoryTheory.Over Obj} (sB : Setoid B.left) [Fintype B.left] [DecidableRel ⇑sB] (P : B.left → Prop) [DecidablePred P] (hP : ∀ (x y : B.left), sB x y → (P x ↔ P y)) : Three₀ B sB P ↔ 2 < Fintype.card { q : Quotient sB // Quotient.lift P ⋯ q }

For a predicate respecting the identity criterion, Three₀ holds exactly when more than two identity classes satisfy it (p. 110).