>>491のつづき

二階論理とメタ論理学の成果
https://ja.wikipedia.org/wiki/%E4%BA%8C%E9%9A%8E%E8%BF%B0%E8%AA%9E%E8%AB%96%E7%90%86#%E4%BA%8C%E9%9A%8E%E8%AB%96%E7%90%86%E3%81%A8%E3%83%A1%E3%82%BF%E8%AB%96%E7%90%86%E5%AD%A6%E3%81%AE%E6%88%90%E6%9E%9C

ゲーデルの不完全性定理の系の1つとして、
以下の3つの属性を同時に満足するような二階述語論理の推論体系は存在しない。

（健全性）証明可能な二階述語論理の文は常に真である。すなわち standard semantics に従ったあらゆるドメインで真である。
（完全性）standard semantics において常に妥当な二階述語論理の論理式は、全て証明可能である。
（実効性）与えられた論理式の並びが妥当な証明かどうかを正しく決定できる証明検証アルゴリズムが存在する。

この系を言い換えると、二階述語論理は完全な証明理論に従わない、とも言える。
この観点で、standard semantics を伴った二階述語論理は一階述語論理とは異なり、
そのせいもあって論理学者は長年、二階述語論理に関わることを避けてきた。

ウィラード・ヴァン・オーマン・クワインは二階述語論理は「論理」ではないと考える理由として上記を挙げている。

上述のように Henkin は
Henkin semantics を使えば、二階述語論理に一階述語論理の標準的な健全で完全で実効的な推論体系を適用できる
ことを証明した。