>>179 追加
>近年、二階述語論理は一種の回復の途上にある。この傾向をもたらしたのは George Boolos による二階の量化の解釈であり

これ、下記のゲーデルの補足と、圏論との関連をご参照
圏論と高階論理は、結構関連があり、その影響もあっての”回復の途上”だろう

>計算複雑性理論への応用

ここは、C++さんがご専門だろう（＾＾
アロンゾ・チャーチ、ラムダ計算の創案者との関係もある

https://ja.wikipedia.org/wiki/%E4%BA%8C%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86
二階述語論理
(抜粋)
ゲーデルの不完全性定理の系の1つとして、以下の3つの属性を同時に満足するような二階述語論理の推論体系は存在しないとされた[4]。
脚注
4 ^ その系の証明とは、健全で完全で実効的な standard semantics の推論体系があったとしたとき、ペアノ算術の帰納的可算な完全な系が存在することになり、それはゲーデルの定理によって存在できないことが明らかとなっていることを示すものである。
(引用終り)

つづく