二階述語論理の理解を一階述語論理に弱めると、結果として得られるシステムはFOLの保守的な拡張になるでしょうか？
二階述語論理を取り、理解公理型を弱め、一階式のみを使用するようにします。あれは、$\phi(x_1,..,x_n)$参照されている記事では、一次式に制限されています。二階述語論理の他のすべての側面を保持します。
結果として得られるシステムは、一階述語論理の一種の保守的な拡張になるでしょうか？つまり、関係記号と関数記号の数量化を可能にするが、一階述語論理の公理に余分な公理を持たない論理であるため、一階述語論理のメリットを享受できます。
常に一階述語論理を追加できますが、そのスキーマをその論理の単一公理として記述できますか？したがって、たとえば、Zermeloの分離スキーマは、次のように、述語を定量化することによって単一の公理として記述されます。$$\forall P \forall A \exists X \forall y (y \in X \leftrightarrow y \in A \land P(y))$$
MathStackExchangeで同様の質問をしましたが、回答がありませんでしたか？
回答
予備的意見：コメントでいくつかの説明をした後、私は自分のコメントを回答として投稿しています。
しましょう $\varphi$ ヒルベルト流の体系で証明されている一次式である $S$。しましょう$M$一次構造である（適切な一次言語に適合）。一階述語論理の完全性から、それを示すのに十分です$M$ 満たす $\varphi$。追加$M$ すべての一次の定義可能な関係と関数、取得 $M^∗$。弱体化した2次システムのすべての公理と規則$S$ で有効です $M^∗$ （ヘンキンセマンティクス）、そう $M^∗$ 満たす $\varphi$健全性によって。以来$M$ の削減です $M^*$ の言語に適応しています $\varphi$、 $M$ 満たす $\varphi$。