>>462 補足
＞これからは、Higher-order logicを指向する時代でしょう

圏論のトポス（topos）
”トポスが高階論理の意味論を与えることもよく知られている” by Taichi Uemura  Nagoya University

(参考)
https://ja.wikipedia.org/wiki/%E3%83%88%E3%83%9D%E3%82%B9_(%E6%95%B0%E5%AD%A6)
トポス (数学)
トポス（topos）とは、位相空間上の層のなす圏を一般化した概念である。
参考文献
清水義夫『圏論による論理学 高階論理とトポス』東京大学出版会、2007年12月。

https://uemurax.github.io/
Taichi Uemura
I do type theory and category theory, I mean ∞-ones. I am currently a 特任助教 at School of Informatics, Nagoya University.

https://uemurax.github.io/pdfs/topos-and-hol.pdf
トポスと高階論理∗ Taichi Uemura 2018 年12月9日
P2
高階論理は大雑把に言うと部分集合や部分集合の集合を量化できる論理である。
トポスが高階論理の意味論を与えることもよく知られている。
P6
3 高階論理のモデル
高階論理のトポス意味論を与え、その健全性を見る。
P11
6 おわりに
トポスの内部言語を導入し、トポスのいくつかの性質を内部言語を使って証明した。しかし、これはトポスと高階論理のほんの一側面でしかない。いくつか関連する項目を挙げるが、詳しいことは[MLM92,LS86, Joh02b] あたりを読みましょう。