述語論理も圏論内部に作れる
それから述語論理じゃなくて様相論理ベースの集合論もある
圏論的論理学ってのもある
ＮＦという型付集合論のモデルとして圏論を構成することもできる
述語論理は唯一無二の論理学の展開方法ではない
さまざまな述語論理に対応する型付ラムダ計算が常に存在する
あまり特定の形式体系を絶対視する必要はないと思う