コラム 形式言語
ここでは私達が普段の会話で用いる言語であるところの自然言語と対になる概念として、数学の命題等の記述に用いられる言語である「形式言語」という概念を導入します。言語を定義することの重要性については、ベリーのパラドックスを思い出して下さい。使用する言語を定義せずに好き勝手に意味のある文字列を考えてしまうと真偽の問えない文章が作れてしまい、命題として機能しなくなってまいます。そのような自体を避けるためにも、きちんと言語を定義しておくと良いのです。
| 定義1（形式言語の定義） |
| \( \Sigma \)を記号の集まりとする。\( \Sigma \)上の形式言語（formal language）とは、\( \Sigma \)に属する記号を文字として用いて表せる有限長*1の文字列の集まりのことである。 |
つまり形式言語とは、\( \Sigma \)に属する記号を文字として用いる時、どんな文字列が文章として許容されるかを指定したものということになります。自然言語で例えるなら、平仮名とカタカナと漢字の全体を\( \Sigma \)と置いて、日本語の文章として意味を持つ文字列の全体、を考えていることになります。ただしこれはあくまで例えで、日本語は自然言語ですので「どのような文字列が日本語として意味を持つか」が時々刻々と、しかも人によって異なる判断基準で、移り変わってしまうので実際にはこのような定義で形式言語を与えることは出来ません。文章として許容される文字列を固定する、という発想自体が既に自然言語とはかけ離れた形式的なものというわけです。
ただし、形式言語を指定することはあくまで「どのような文字列が文章として許容されるか」を指定するだけで、「どのような文章が誤りのない文章か」については何ら指定していないということに注意して下さい。それらを規定するために必要なものは「形式推論体系」と呼ばれます。与えられた形式言語の上の形式演繹体系（formal deductive system）とは大雑把に、仮定なく演繹できる命題である公理（axiom）や、与えられた命題から新たな命題を導く演繹規則（deduction rule）または推論規則（inference rule）という、追加の情報を形式言語に与えたものです。ここでは形式演繹体系の詳細を述べることは避けます。
形式言語の構成
さて、形式言語を構成することはとても簡単です。例えば\( \Sigma \)を記号の集まりとした時、\( \Sigma \)に属する記号を文字として用いて表せる有限長の文字列の全体の集まりは\( \Sigma \)上の形式言語になりますし、逆に何ら要素を持たない空の集まりもまた\( \Sigma \)上の形式言語となります。これらの自明な形式言語は理論の記述にはあまり役に立たないので、もう少し役に立つ例を上げようと思います。
そのために少し丁寧に準備をします。自然言語に品詞分解が考えられるように、形式言語にも名詞や動詞に相当する抽象的な概念を導入します。ここだけの用語として、それらの情報を「品詞データ」と呼ぶことにしましょう。
| 定義2（品詞データの定義） |
| \( \Sigma \)をカッコ記号\( (,) \)を含む記号の集まりとする。\( \Sigma \)上の品詞データ（data of parts of speech）とは、７つ組\( (\textrm{T},\textrm{VT},\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)であって以下を満たすものである。 |
| (1) \( \textrm{T} \)は、\( \Sigma \)に属する記号であってカッコ記号\( (,) \)ではなくかつ\( \textrm{R} \)と\( \textrm{PF} \)と\( \textrm{L}^1 \)と\( \textrm{L}^2 \)と\( \textrm{Q} \)のいずれにも属さないようなものを文字として用いて表せる有限長の文字列の集まりである。 |
| (2) \( \textrm{VT} \)は、\( \textrm{T} \)に属する文字列の集まりである。 |
| (3) \( \textrm{R} \)と\( \textrm{PF} \)と\( \textrm{L}^1 \)と\( \textrm{L}^2 \)と\( \textrm{Q} \)はいずれも、\( \Sigma \)に属する記号であってカッコ記号\( (,) \)ではないものの集まりであり、互いに交わらない。 |
品詞データの定義自体は非常に抽象的で分かりにくいと思いますので、イメージしやすいようにここだけの約束として品詞データの各成分に品詞らしい名前を付けようと思います。\( \Sigma \)上の品詞データ\( \textrm{WC} = (\textrm{T},\textrm{VT},\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)に対して、ここでは\( \textrm{T} \)に属する文字列を\( \textrm{WC} \)の名詞記号（noun symbol）と呼び、\( \textrm{VT} \)に属する文字列を\( \textrm{WC} \)の可変名詞記号（variable noun symbol）と呼び、\( \textrm{R} \)に属する記号を\( \textrm{WC} \)の動詞記号（verb symbol）と呼び、\( \textrm{PF} \)に属する記号を\( \textrm{WC} \)の文記号（sentence symbol）と呼び、\( \textrm{L}^1 \)に属する記号を\( \textrm{WC} \)の引数１の論理記号（1-ary logical symbol）と呼び、\( \textrm{L}^2 \)に属する記号を\( \textrm{WC} \)の引数２の論理記号（2-ary logical symbol）と呼び、\( \textrm{Q} \)に属する記号を\( \textrm{WC} \)の量化記号（quantifier symbol）と呼ぶことにします。また\( \textrm{WC} \)の引数１の論理記号と引数２の論理記号をまとめて\( \textrm{WC} \)の論理記号（logical symbol）と呼ぶことにします。
その言葉遣いを踏まえて品詞データの定義を見直してみると、例えば(1)から「名詞記号は動詞記号とは異なる」、つまり「名詞を表す文字列は動詞を表す文字列と区別できる」ということが従います。これは文章を品詞分解するために当然成り立って欲しい性質に見えるかもしれませんが、自然言語では基本的に成り立たないことに注意しましょう。例えば日本語だと「はる」という文字列が「春」という名詞と「張る」という動詞の両方に用いられてしまいますし、英語でも「spring」という文字列が「春」という意味の名詞と「跳ねる」という意味の動詞の両方に用いられてしまいます。つまり、文字列のレベルで品詞が確定してしまうのも非常に形式化された制約と言えます。
さて、品詞データをあたかも品詞のように用いて形式言語を構成することが出来ます。
| 定義3（品詞データの付随する形式言語の定義） |
| \( \Sigma \)をカッコ記号\( (,) \)を含む記号の集まりとし、\( \textrm{WC} \)を\( \Sigma \)上の品詞データとする。この時、以下のように定まる\( \Sigma \)上の形式言語\( L_{\textrm{WC}} \)を\( \textrm{WC} \)に付随する形式言語と呼ぶ。 |
| (1) \( \textrm{WC} \)の名詞記号であるような文字列は\( L_{\textrm{WC}} \)に属する。 |
| (2) \( \textrm{WC} \)の名詞記号であるような２つの文字列\( x \)と\( y \)*2及び\( \textrm{WC} \)の動詞記号\( \sim \)に対し、文字列\( x \sim y \)は\( L_{\textrm{WC}} \)に属する。 |
| (3) \( \textrm{WC} \)の文記号１節からなる文字列は\( L_{\textrm{WC}} \)に属する。 |
| (4) \( L_{\textrm{WC}} \)に属する文字列\( s \)及び\( \textrm{WC} \)の引数１の論理記号\( \surd \)に対し、文字列\( \surd (s) \)は\( L_{\textrm{WC}} \)に属する。 |
| (5) \( L_{\textrm{WC}} \)に属する２つの文字列\( s \)と\( t \)及び\( \textrm{WC} \)の引数２の論理記号\( \Rightarrow \)に対し、文字列\( (s) \Rightarrow (t) \)は\( L_{\textrm{WC}} \)に属する。 |
| (6) \( L_{\textrm{WC}} \)に属する文字列\( s \)及び\( \textrm{WC} \)の量化記号\( \nabla \)及び\( \textrm{WC} \)の変項記号\( x \)に対し、文字列\( \nabla x (s) \)は\( L_{\textrm{WC}} \)に属する。 |
| (7) 以上の規則によって\( L_{\textrm{WC}} \)に属することが保証される文字列以外は\( L_{\textrm{WC}} \)に属さない。 |
\( \textrm{WC} \)の名詞記号を\( L_{\textrm{WC}} \)の項（term）と呼び、\( \textrm{WC} \)の可変名詞記号を\( L_{\textrm{WC}} \)の変項（variable term）または変数（variable number）と呼び、\( \textrm{WC} \)の動詞記号を\( L_{\textrm{WC}} \)の述語（predicate）または関係（relation）と呼び、\( \textrm{WC} \)の論理記号を\( L_{\textrm{WC}} \)の論理演算子（logical operator）または論理結合子（logical connective）と呼び、\( \textrm{WC} \)の量化記号を\( L_{\textrm{WC}} \)の量化子（quantifier）と呼びます。(2)で\( L_{\textrm{WC}} \)に属することが保証される「項 述語記号 項」の形の文字列と、(3)で\( L_{\textrm{WC}} \)に属することが保証される\( \textrm{WC} \)の文記号を、まとめて\( L_{\textrm{WC}} \)の原子式（primitive formula）と呼びます。更に(4)～(6)を繰り返し適用して原子式と論理演算子と量化子を適切に組み合わせることで得られる文字列を\( L_{\textrm{WC}} \)の論理式（logical formula）と呼びます。(7)によって、\( L_{\textrm{WC}} \)に属する文字列が「\( L_{\textrm{WC}} \)の項」か「\( L_{\textrm{WC}} \)の論理式」の２種類に限られることが保証されます。与えられた文字列が\( L_{\textrm{WC}} \)に属するか否かを判定するアルゴリズムを計算機に実装させることもできますので、余力のある人はそのような方法を考えてみましょう。
それでは品詞データと形式言語の例を見てみましょう。
| 例4（\( 2 \)進法表記された自然数の等式を記述する命題論理に用いる形式言語の例） |
| 記号の集まり\( \Sigma_2 \)と\( \Sigma_2 \)上の品詞データ\( D_2 = (\textrm{T}_2,\textrm{VT}_2,\textrm{R}_2,\textrm{PF}_2,\textrm{L}^1_2,\textrm{L}^2_2,\textrm{Q}_2) \)を以下のように定める。 |
| (1) \( \Sigma_2 \)は記号\( 0, 1, =, (, ), \vee, \wedge, \neg, \to \)からなる集まりである。 |
| (2) \( \textrm{T}_2 \)は、記号\( 0{} \)の１文字からなる文字列と、\( 0{} \)と\( 1 \)のみからなる文字列であって左端が\( 0{} \)でない文字列の、全体からなる集まりである。 |
| (3) \( \textrm{VT}_2 \)は要素を持たない。 |
| (4) \( \textrm{R}_2 \)は記号\( = \)のみからなる集まりである。 |
| (5) \( \textrm{PF}_2 \)は要素を持たない。 |
| (6) \( \textrm{L}^1_2 \)は記号\( \neg \)のみからなる。 |
| (7) \( \textrm{L}^2_2 \)は記号\( \vee, \wedge, \to \)のみからなる。 |
| (8) \( \textrm{Q}_2 \)は要素を持たない。 |
| この時\( 10110 \)や\( 110=101 \)や\( (10=1) \to (\neg ( (11 = 101) \vee (11101 = 1011) ) ) \)は\( L_{D_2} \)に属すが、\( 01 \)や\( 10 = 11 = 101 \)や\( (11) \vee (10 = 111) \)は\( L_{D_2} \)に属さない。 |
要するに\( L_{D_2} \)における項とは\( 2 \)進法表記された自然数のことに他なりません。ただし自然数という概念は後で公理的集合論の中でも定義するので、公理的集合論の外で扱うメタな自然数概念である「\( L_{D_2} \)における項」のことは自然数と呼ばないことにします。
品詞データの構成
以上により、（ある程度役に立つ）形式言語を構成する手段として、品詞データを構成すれば良いことが分かりました。更に、品詞データのうち特に項記号の集まりを構成する方法として、定項記号と関数記号という概念を使うものを紹介します。ここだけの用語として、定数記号と変数記号と関数記号のデータのことを「項データ」と呼ぶことにします。
| 定義5（項データの定義） |
| \( \Sigma \)をカッコ記号\( (,) \)を含む記号の集まりとする。\( \Sigma \)上の項データ（data of terms）とは、\( \Sigma \)に属する記号であってカッコ記号\( (,) \)でないものを文字として用いて表せる有限長の文字列の集まりの４つ組\( (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2) \)であって、互いに交わらないものである。また\( \Sigma \)上の詳細な品詞データ（detailed data of parts of speech）とは、９つ組\( (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2,\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)であって以下を満たすものである。 |
| (1) \( (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2) \)は、\( \Sigma \)上の項データである。 |
| (2) \( \textrm{CT} \)と\( \textrm{VT} \)と\( \textrm{F}^1 \)と\( \textrm{F}^2) \)はいずれも、\( \Sigma \)に属する記号であってカッコ記号\( (,) \)ではなくかつ\( \textrm{PF} \)と\( \textrm{RS} \)と\( \textrm{L}^1 \)と\( \textrm{L}^2 \)と\( \textrm{Q} \)のいずれにも属さないようなものを文字として用いて表せる有限長の文字列の集まりである。 |
| (3) \( \textrm{R} \)と\( \textrm{PF} \)と\( \textrm{L}^1 \)と\( \textrm{L}^2 \)と\( \textrm{Q} \)はいずれも、\( \Sigma \)に属する記号であってカッコ記号\( (,) \)ではないものの集まりであり、互いに交わらない。 |
項データの定義も抽象的で分かりにくいと思いますので、イメージしやすいように各成分に名前を付けておきます。\( \Sigma \)上の項データ\( D = (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2) \)に対し、ここでは\( \textrm{CT} \)を\( D \)の定項記号（constant term symbol）または定数記号（constant number symbol）と呼び、\( \textrm{VT} \)を\( D \)の変項記号または変数記号と呼び、\( \textrm{F}^1 \)を\( D \)の引数１の関数記号（1-ary function symbol）と呼び、\( \textrm{F}^2 \)を\( D \)の引数２の関数記号（2-ary function symbol）と呼ぶことにします。また\( D \)の１項関数記号と２項関数記号をまとめて\( D \)の関数記号（fuction symbol）と呼ぶことにします。
それでは項データから項を構成しましょう。
| 定義6（項データに付随する項の集まり） |
| \( \Sigma \)をカッコ記号\( (,) \)を含む記号の集まりとし、\( D \)を\( \Sigma \)上の項データとする。この時、以下のように定まる文字列の集まり\( \textrm{T}_D \)を\( D \)に付随する名詞記号の集まりと呼ぶ。 |
| (1) \( D \)の定項記号か変項記号であるような文字列は、\( \textrm{T}_D \)に属する。 |
| (2) \( \textrm{T}_D \)に属する文字列\( x \)及び\( D \)の引数１の関数記号であるような文字列\( F \)に対し、文字列\( F(x) \)は\( \textrm{T}_D \)に属する。 |
| (3) \( \textrm{T}_D \)に属する２つの文字列\( x \)と\( y \)及び\( D \)の引数２の関数記号であるような文字列\( \triangle \)に対し、文字列\( (x) \triangle (y) \)は\( \textrm{T}_D \)に属する。 |
項データに付随する名詞記号の集まりを実際に品詞データの成分としての名詞記号の集まりとして用います。つまり、\( \Sigma \)上の詳細な品詞データ\( D = (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2,\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)に対して７つ組\( (\textrm{T}_{(\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2)},\textrm{VT},\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)は\( \Sigma \)上の品詞データをなすので、その品詞データに付随する形式言語が意味を持ちます。ここではそれを\( L^D \)と表記し、\( D \)に付随する形式言語と呼ぶことにします。
それでは詳細な品詞データに付随する形式言語の例を見てみましょう。
| 例7（自然数論を記述する述語論理に用いる形式言語の例） |
| 記号の集まり\( \Sigma_{\textrm{Peano}} \)と\( \Sigma_{\textrm{Peano}} \)上の詳細な品詞データ\( D_{\textrm{Peano}} = (\textrm{CT}_{\textrm{Peano}},\textrm{VT}_{\textrm{Peano}},\textrm{F}^1_{\textrm{Peano}},\textrm{F}^2_{\textrm{Peano}},\textrm{R}_{\textrm{Peano}},\textrm{PF}_{\textrm{Peano}},\textrm{L}^1_{\textrm{Peano}},\textrm{L}^2_{\textrm{Peano}},\textrm{Q}_{\textrm{Peano}}) \)を以下のように定める。 |
| (1) 記号\( n \)*3は\( \Sigma_{\textrm{Peano}} \)に属する。 |
| (2) \( 0{} \)を１文字以上並べて得られる記号\( i \)*4に対し、記号\( n_i \)は\( \Sigma_{\textrm{Peano}} \)に属する。 |
| (3) 記号\( 0, S, (, ), +, \times, =, T, F, \vee, \wedge, \neg, \to, \forall, \exists \)は\( \Sigma_{\textrm{Peano}} \)に属する。 |
| (4) 以上の規則によって\( \Sigma_{\textrm{Peano}} \)に属することが保証される記号以外は\( \Sigma_{\textrm{Peano}} \)に属さない。 |
| (5) \( \textrm{CT}_{\textrm{Peano}} \)は、記号\( 0{} \)の１文字からなる文字列のみからなる集まりである。 |
| (6) \( \textrm{VT}_{\textrm{Peano}} \)は、記号\( n \)の１文字からなる文字列と、\( 0{} \)を１文字以上並べて得られる記号\( i \)を用いて\( n_i \)と表せる記号１文字からなる文字列の、全体の集まりである。 |
| (7) \( \textrm{F}^1_{\textrm{Peano}} \)は、記号\( S \)の１文字からなる文字列のみからなる集まりである。 |
| (8) \( \textrm{F}^2_{\textrm{Peano}} \)は、記号\( + \)の１文字からなる文字列と記号\( \times \)１文字からなる文字列からなる集まりである。 |
| (9) \( \textrm{R}_{\textrm{Peano}} \)は、記号\( = \)のみからなる集まりである。 |
| (10) \( \textrm{PF}_{\textrm{Peano}} \)は、記号\( T \)と\( F \)からなる集まりである。 |
| (11) \( \textrm{L}^1_{\textrm{Peano}} \)は、記号\( \neg \)のみからなる集まりである。 |
| (12) \( \textrm{L}^2_{\textrm{Peano}} \)は、記号\( \vee \)と\( \wedge \)と\( \to \)からなる集まりである。 |
| (13) \( \textrm{Q}_{\textrm{Peano}} \)は、記号\( \forall \)と\( \exists \)からなる集まりである。 |
| この時\( S(S(0) ) \)や\( (S(n) ) + (n_0) = n_{000} \)や\( (n_0=S(n_{00}) ) \to \forall n_{0000}(\neg ( (S(S(n_{00}) ) = S(n)) \vee ( (S(S(S(n_0) ) ) \times (S(0) ) = 0) ) ) \)は\( L^{D_{\textrm{Peano}}} \)に属すが、\( S)S0() ( \)や\( (S(n) ) + + = n_0 \)や\( (n) \vee (0 = n_{00}) \)は\( L^{D_{\textrm{Peano}}} \)に属さない。 |
ここでは一般の述語論理で用いられる形式言語を定義することは避けますが、大雑把には以下のような性質を満たす記号の集まり\( \Sigma \)と\( \Sigma \)上の詳細な品詞データ\( D = (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2,\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)を用いて、\( D \)に付随する形式言語として与えられると考えて下さい*5。
| (1) \( \Sigma \)は無限個の記号の集まりであり、特に記号\( \perp, \in, (, ), \vee, \wedge, \neg, \to, \forall, \exists \)は\( \Sigma \)に属する。 |
| (6) \( \textrm{CT} \)は無限個の定項記号の集まりである。 |
| (7) \( \textrm{VT} \)は無限個の変項記号の集まりである。 |
| (8) \( \textrm{F}^1 \)は無限個の引数１の関数記号の集まりである。 |
| (9) \( \textrm{F}^2 \)は無限個の引数２の関数記号の集まりである。 |
| (10) \( \textrm{R} \)は、等号記号\( = \)を含む無限個の関係記号の集まりである。 |
| (11) \( \textrm{PF} \)は、矛盾記号\( \perp \)のみからなる集まりである。 |
| (12) \( \textrm{L}^1 \)は、否定記号\( \neg \)のみからなる集まりである。 |
| (13) \( \textrm{L}^2 \)は、論理記号\( \vee \)と\( \wedge \)と\( \to \)からなる集まりである。 |
| (14) \( \textrm{Q} \)は、量化記号\( \forall \)と\( \exists \)からなる集まりである。 |
しかしながら、個別の理論を記述するために述語論理を用いる上ではそこまで多くの記号を導入する必要はありません。Encyclopedia of \( P \)-adic Numbersでは公理的集合論やそれを記述するための述語論理を展開するために、以下のように定まる記号の集まり\( \Sigma \)と\( \Sigma \)上の詳細な品詞データ\( D = (\textrm{CT},\textrm{VT},\textrm{F}^1,\textrm{F}^2,\textrm{R},\textrm{PF},\textrm{L}^1,\textrm{L}^2,\textrm{Q}) \)を用います*6。
| (1) 英語のアルファベットの大文字と小文字のローマン体とイタリック体とボールド体、及びギリシャ語のアルファベットの大文字と小文字は\( \Sigma \)に属する。 |
| (2) 記号\( \perp, \in, (, ), \vee, \wedge, \neg, \to, \forall, \exists \)は\( \Sigma \)に属する。 |
| (3) \( \Sigma \)に属する２つの記号\( x \)と\( y \)であって\( \perp, \in, (, ), \vee, \wedge, \neg, \to, \forall, \exists \)のいずれでもないものに対し、記号\( (x)_y \)と\( (x)^y \)は\( \Sigma \)に属する。 |
| (4) \( \Sigma \)に属する記号\( x \)であって\( \perp, \in, (, ), \vee, \wedge, \neg, \to, \forall, \exists \)のいずれでもないものと\( L_{D_2} \)の項\( n \)に対し、\( (x)_n \)と\( (x)^n \)は\( \Sigma \)に属する。 |
| (5) 以上の規則によって\( \Sigma \)に属することが保証される記号以外は、\( \Sigma \)に属さない。 |
| (6) \( \textrm{CT} \)は要素を持たない。 |
| (7) \( \textrm{VT} \)は、\( \Sigma \)に属する記号であって\( \perp, \in, (, ), \vee, \wedge, \neg, \to, \forall, \exists \)のいずれでもないものの全体の集まりである。 |
| (8) \( \textrm{F}^1 \)は要素を持たない。 |
| (9) \( \textrm{F}^2 \)は要素を持たない。 |
| (10) \( \textrm{R} \)は、記号\( \in \)のみからなる集まりである。 |
| (11) \( \textrm{PF} \)は、記号\( \perp \)のみからなる集まりである。 |
| (12) \( \textrm{L}^1 \)は、記号\( \neg \)のみからなる集まりである。 |
| (13) \( \textrm{L}^2 \)は、記号\( \vee \)と\( \wedge \)と\( \to \)からなる集まりである。 |
| (14) \( \textrm{Q} \)は、記号\( \forall \)と\( \exists \)からなる集まりである。 |
ちなみに、このままだと\( = \)も\( \emptyset \)も\( + \)もないので公理的集合論の記述がしにくいことは間違いないです。代わりに、\( \in \)を用いて\( = \)や\( \emptyset \)や\( + \)を具体的な略記として導入します*7。略記で新たな項や述語を導入することの詳細な意味については、次を参照して下さい。
以上でEncylopedia of \( P \)-adic Numbersにおける形式言語の導入を行いました。
- 述語論理へ戻る。
*1 ここでは断りなく長さが１以上であることを要請します。
*2 これは&mathjax{x};という記号や&mathjax{y};というアルファベットそのものが&mathjax{\textrm{WC}};の名詞記号であるという意味ではなく、&mathjax{\textrm{WC}};の項記号を表すメタな変数としての&mathjax{x};と&mathjax{y};です。
*3 これは記号を表すメタな変数ではなく、&mathjax{n};というアルファベットそのもののことです。
*4 これは記号を表すメタな変数であり、&mathjax{i};というアルファベットそのもののことではありません。例えば&mathjax{i};は&mathjax{0{}};や&mathjax{00};や&mathjax{000};や&mathjax{0000000000};です。
*5 ここでは高々２個の引数を持つ関数記号しか考えていませんが、実際の述語論理では任意有限個の引数を持つ関数記号を考えます。
*6 もちろん述語論理の展開以外では、つまり地の文では、メタな言語として日本語や英語を用います。
*7 cf. 等号の定義