２階述語論理式の式の形

２階述語論理式というのは、形の上では１階述語論理式とどのように見分けるのでしょうか？（実際には私の学問にここまで必要はないと思うのですが、気になってしょうがありません）

例えば、下の式は何階の述語論理式ですか。１階だと認識しているのですが、宜しいですか。
∀x [[G(x)∧ ∃y [C(y) ∧ O(x, y)]] → S(x, y)]

２階述語論理式の簡単な分かりやすい代表例を示していただけると嬉しいです。

質問者からの補足コメント

• ∀x(A(x)⇒A(x)∨B(x))だけだと１階述語論理式だと思うのですが
  ∀A∀Bが左側についているので２階述語論理式になるのですか？
  ちなみに変数xがない∀Aや∀Bはそのように解釈するのでしょうか。そしてそれは最初∀Bが適用され、次に∀Aが適用される順番ですか？
  すなわち
  ∀A(∀B(∀x(A(x)⇒A(x)∨B(x))))
  ですか。

  No.2の回答に寄せられた補足コメントです。 補足日時：2015/11/07 11:15

No.3 回答者： stomachman 回答日時： 2015/11/08 02:36

ANo.2へのコメントについてです。

> ∀A∀Bが左側についているので２階述語論理式になるのですか？

はい。

> そしてそれは最初∀Bが適用され、次に∀Aが適用される順番ですか？

どちらが先でも同じです。隣接する∀と∃の順序を入れ替えることはできませんが、隣接する∀同士の（また隣接する∃同士の）入れ替えをしても意味は変わりませんから。

No.2 回答者： stomachman 回答日時： 2015/11/07 03:53

> 簡単な分かりやすい

∀A∀B∀x(A(x)⇒A(x)∨B(x))

No.1 回答者： Tacosan 回答日時： 2015/11/06 23:52

簡単に言えば

述語記号を量化できる
のが 2階述語論理. 例えば, 数学的帰納法が成り立つことをペアノの公理系で保証している式が 2階の式になっている.