Introduction to higher order categorical logic を再度読み始めたけど、2ページ目の deductive system の定義で躓いてしまった。graph に indentity morphism と morphism の composition (合成)が定義されただけのものを deductive system と呼ぶとしているのだけど、これのどのあたりが deductive system っぽいのかが分からない。点々と矢印に合成定義したやつ、みたいな名前をつければ良いのにわざわざ比喩的に deductive system って名前を持ってくる意味が分からない。しかも、この定義だと morphism の合成の結合法則が成り立つ事が仮定されて居なくて(結合法則が入ると category の定義になる)射の合成が結合的でないような deductive system で考えて意味があるようなものがあるのかどうかも良くわからないし、そういう例が特に提示されないまま話が進んでいるように見える。