数学の基礎

　本文第１節で、論理式を構成手続きという概念を用いて定義し、更に括弧を使わないポーランド式の記述を採用しました。
　すなわち、ある文字列が論理式であるかどうかは、構成手続きが存在するかどうかという非アルゴリズム的な方法で定義されており、また論理式の引数の組合せが一意的に定まるか、つまり一つの論理式が、異なる引数 A_i と B_i の組によって sA₁¼A_n とも sB₁¼B_n とも表されてしまう、といったことがないかどうかは自明ではありません。
　そこで、本節では与えられた文字列が論理式であるかどうかを判定し、それが論理式である場合には、その論理式の引数の組を求めるアルゴリズムの存在と、引数の組の一意性が成り立つことについて解説します。

　さて、超数学の議論では自然数をよく用いるので、超数学における自然数とは何かということを厳密に定義しておきましょう。
　今、文字 0 を用意し、これにダッシュ '  をゼロ個以上付けたものを超数学における自然数とよぶことにします。自然数 n と m は、文字列として同じであるとき n = m と書き、m に付いているダッシュの数の方が多い（少ない）とき n < m （ n > m ）、そうでないとき n ³ m （ n £ m ）と書くことにします。
　また、自然数 n に自然数 m のダッシュの部分だけを追加して得られる自然数を n + m と書き、自然数 n の中の各ダッシュ '  を自然数 m のダッシュの部分全体で一斉に置き換えて得られる自然数を nm と書き、n ³ m のとき n から m のダッシュの部分と同じ部分を取り除いて得られる自然数を n - m と書き、更に便宜上、n < m の場合は n - m は 0 を意味するものと規約することにします。
　また 0'  を 1 、1'  を 2 、等と略記し、n ³ 1 であるような自然数 n を正整数とよびます。

　さて、文字列に関する議論に先立って、扱いの煩わしい鎖の概念を用いないですむように、論理式などの定義を若干変更します。
　本文第１節の定義から明らかなように、論理式における鎖の左端は必ず量化記号と結ばれ、右端は必ず文字 £ と結ばれています。しかも、論理式に現れる £ は、必ず唯一つの鎖と結ばれています。
　そこで、£ がその i 個左方にある文字と鎖で結ばれているとき、この £ と鎖を“一体化”したものを一個の“文字” £_i で置き換えることにし、このような文字を束縛文字とよぶことにしましょう。
　すなわち £ という文字と鎖の概念を廃止して、かわりに正整数 i に対する束縛文字 £_i を新たに文字の仲間に追加するわけです。
　例えば、集合論において、省略記法で a Ì b すなわち "x ( xÎa  Þ  xÎb ) と表される文字列は、この鎖を用いない流儀では " Þ Î £₃ a Î £₆ b という文字列を意味します。

　以上のように文字や文字列の定義を変更した上で、一般に文字のことを 0 階の文字列とよび、N 階の文字列からなる列を N + 1 階の文字列とよぶことにします。文字列、特に論理式は 1 階の文字列であり、論理式の構成手続きは 2 階の文字列です。
　一般に、N + 1 階の文字列 S について、それを構成する N 階の文字列の個数をその長さとよんで | S | と書き、その第 i 番目の構成要素である N 階の文字列を S[i] と書き、S の構成要素の i 番目から j 番目までを切り出して得られる N + 1 階の文字列を S[ j : i] と書き、２つの N + 1 階の文字列 S , S' に対し、S の後ろに S' を繋げて得られる N + 1 階の文字列を S' * S と書き、N 階の文字列 A 一個のみからなる N + 1 階の文字列を { A } と書くことにします。明らかに S[ | S | : 1] は S 自身であり、S[i : i] は { S[i] } です。

　さて、文字列 A に対しては、その右から i 番目の文字を A[i] と書くことにします。
　文字列 A は、A[i] が束縛文字 £_j である場合は必ず i + j £ | A | であって、しかも A[i + j] が量化記号になっているとき、正則な文字列とよぶことにします。これは鎖を用いる流儀でいえば、各 £ が唯一つの鎖でそれより左にある量化記号と結ばれ、それ以外に鎖を持たない文字列を意味します。

　さて、n 変項記号 s と n 個の文字列 A₁ ,¼, A_n を並べて得られる文字列 { s } * A₁ * ¼ * A_n のことを単に sA₁¼A_n と略記することにします。
　また、長さ n の文字列 A と量化記号 κ と変数 x に対し、各正整数 i £ n について、A[i] が x のときは £_n+1-i を、それ以外のときは A[i] 自身を第 i 番目の文字に持ち、κ を第 n + 1 番目の文字に持つ、長さ n + 1 の文字列のことを κxA と書くことにします。
　明らかに、各 A_i が正則なら sA₁¼A_n も正則であり、A が正則なら κxA も正則です。従って特に、論理式は正則な文字列です。

　さて次に、与えられた文字列が論理式であるかどうかを判定するアルゴリズムについて考えます。
　まず、文字 a に対し、“a の引数の個数”を意味する自然数 ν(a) を次のように定義します：

(A1-1a)	a が変数又は束縛文字なら ν(a) は 0 とする。
(A1-1b)	a が量化記号以外の記号なら ν(a) は a の引数の個数とする。
(A1-1c)	a が量化記号なら ν(a) は 1 とする。

　次に、文字列 A と自然数 k £ | A | に対し、自然数 μ_A(k) を次のように順に定義していきます：

(A1-2a)  μA(0) :º 0

(A1-2b)  μA(k) :º ( μA ° pd) ν(A[k]) (k)       (  1 £ k £ | A |  )

　ただし pd k は、“k の直前の自然数”、すなわち k が 0 なら 0 を、k が l + 1 なら l を表し、μ_{A °} pd は μ_A と pd の合成関数を表し、φⁿ は関数 φ を n 回合成した関数（ただし n が 0 のときは恒等関数）を表します。このとき

(A1-3)  μA(k) £ k       (  k £ | A |  )

が成り立ちます。
　実際、k = 0 のときは (A1-2a) により明らかです。
　従って、あとは、任意の正整数 l £ | A | に対し、すべての k < l について μ_A(k) £ k が成り立つと仮定して、μ_A(l) £ l が成り立つことを証明すれば十分です。
　任意に与えられた k £ l に対し、pd k < l ですから、仮定により ( μ_{A °} pd)(k) = μ_A(pd k) £ pd k £ l となるので、これを繰り返せば、(A1-2b) により μ_A(k) £ l が得られ、特に μ_A(l) £ l が成り立つので、(A1-3) は証明されました。

　さて、与えられた論理式に対し、その一部又は全部の変数を束縛文字に置き換えて得られる文字列を準論理式とよぶことにしましょう。このとき

(A1-4)

文字列 A と 1 £ i £ k £ | A | に対し、A[k : i] が準論理式なら i = μA(k) が成り立つ。従って特に、このような i は一意的である。

という事実が成り立ちます。
　実際、| A[k : i] | = 1 の場合は、i = k であり、しかも A[k : i] は、A[k] 一文字から成る長さ１の準論理式ですから、A[k] は変数か、束縛文字か、０変項記号かのいずれかです。
　ゆえにいずれの場合でも ν(A[k]) は 0 であり、従って (A1-2b) により μ_A(k) = k となって、この場合は(A1-4) は成立します。
　次に l > 1 に対し、 | A[k : i] | < l の場合は (A1-4) が成り立つと仮定して、| A[k : i] | = l の場合にも成り立つことを証明します。
　この場合、A[k : i] は、長さ２以上の準論理式ですから、n 変項論理記号 s と n 個の準論理式 A₁ ,¼, A_n が存在して、sA₁¼A_n と書けます。
　そこで、k_i :º | A_i | と置けば、A_i は A[k - k₁ - ¼ - k_i-1 - 1 : k - k₁ - ¼ - k_i ] と書け、しかも | A_i | < l ですから、仮定により

(A1-5)  k - k1 - ¼ - ki = μA(k - k1 - ¼ - ki-1 - 1) = ( μA ° pd)(k - k1 - ¼ - ki-1 )

が成り立ち、従って k - k₁ - ¼ - k_n = ( μ_{A °} pd)ⁿ(k) が得られます。ところがこの左辺は i であり、右辺は (A1-2b) により μ_A(k) ですから、この場合も (A1-4) が成り立つことがわかります。以上で (A1-4) は証明されました。

　この (A1-4) を用いると、次の事実が証明できます：

(A1-6)

準論理式 A と 1 £ k £ | A | に対し、A[k : i] が準論理式になるような正整数 i £ k が唯一つ存在して i = μA(k) で与えられる。

　実際、| A | = 1 のときは明らかです。
　ゆえにあとは、l > 1 に対し、 | A | < l の場合は (A1-6) が成り立つと仮定して、| A | = l の場合にも成り立つことを証明すれば十分です。
　なお、k = | A | なら (A1-6) は i を 1 と置けば (A1-4) により明らかに成り立つので、k < | A | と仮定して証明すれば十分です。
　この場合、ある n 変項記号 s と準論理式 A₁ ,¼, A_n が存在して A は sA₁¼A_n の形に書け、しかも l_r :º | A_r | と置けば、

(A1-7)  lr+1 + ¼ + ln < k £ lr + ¼ + ln

となる正整数 r £ n が存在します。このとき k' :º k - l_r+1 - ¼ - l_n と置けば、0 < k' £ l_r = | A_r | < l ですから、仮定により A_r[k' : j] が準論理式となるような正整数 j £ k' が存在します。ここで i :º j + l_r+1 + ¼ + l_n と置きます。
　すると、準論理式 A_r[k' : j] は A[k : i] とも書くことができ、しかも i £ k です。ゆえにこの事実と (A1-4) により、(A1-6) は証明されました。

　この (A1-6) を、準論理式 A の分解 sA₁¼A_n について適用すれば、各 A_i の左端を A[k] とすれば、右端は A[μ(k)] でなければならないことがわかりますから、A のこのような分割の仕方が一意的に定まることがわかります。

　さて次に、A が論理式なら、次の性質が成り立つことを証明しましょう：

(A1-8a)	すべての正整数 k £ | A | に対し、μA(k) ³ 1
(A1-8b)	μA( | A | ) = 1
(A1-8c)	A[k] が関数記号、述語記号、項を引数に持つ量化記号のいずれかならば、正整数 i £ ν(A[k]) に対し、pd( ( μA ° pd)i-1(k) ) 番目の文字は、変数、束縛文字、関数記号、項型量化記号のいずれかである。
(A1-8d)	A[k] が論理接続詞、命題を引数に持つ量化記号のいずれかならば、正整数 i £ ν(A[k]) に対し、pd( ( μA ° pd)i-1(k) ) 番目の文字は、述語記号、論理接続詞、命題型量化記号のいずれかである。
(A1-8e)	i 番目の文字が £j ならば、i + j £ | A | かつ μA(i + j) £ i で A[i + j] は量化記号。

　実際、正整数 k £ | A | に対し、(A1-6) により A[k : i] が準論理式になるような正整数 i £ k が唯一つ存在し、μ_A(k) = i ³ 1 となるので (A1-8a) は明らかです。

　また、A はそれ自身、すなわち A[ | A | : 1] が準論理式ですから、(A1-4) により (A1-8b) が得られます。

　また、1 £ k £ | A | に対し、(A1-6) により、A[k : μ_A(k)] は A[k] を左端に持つ準論理式ですから、この準論理式を sA₁¼A_n の形に書けば、A_i は準論理式で、k_i :º | A_i | と置けば、A_i は A[k - k₁ - ¼ - k_i-1 - 1 : k - k₁ - ¼ - k_i ] と書けますから、(A1-5) が成り立ち、従って

(A1-9)  ( μA ° pd)i(k) = k - k1 - ¼ - ki

が得られます。ゆえに、pd( ( μ_{A °} pd)^i-1(k) ) 番目、すなわち k - k₁ - ¼ - k_i-1 - 1 番目の文字というのは A_i の左端の文字であることがわかり、また s は A[k] ですから、論理式の定義により (A1-8c),(A1-8d) は明らかです。

　最後に、i 番目の文字が £_j なら、論理式は正則な文字列ですから、i + j £ | A | かつ A[i + j] は量化記号です。しかも (A1-6) により、この量化記号が左端に来る準論理式が唯一つ存在して A[i + j : μ_A(i + j)] で与えられますから、この左端の文字と“鎖で繋がれている”第 i 番目の文字 £_j は、この連なりの中に含まれていなければなりません。従って (A1-8e) が成立します。

　以上で A が論理式なら (A1-8) が成り立つことがわかりました。

　今度は逆に、(A1-8) が成り立てば A は論理式であることを証明しましょう。

　まず、A に現れない | A | 個の相異なる変数 x_i ( 1 £ i £ | A | ) を用意し、各正整数 k £ | A | に対し、A の i £ k であるような i 番目の文字が £_j の形で i + j > k である場合にこれを変数 x_{i + j} に置き換えることによって得られる文字列を A^(k) と書くことにします。このとき明らかに A^(k) は、変数 x_l ( 1 £ l £ k ) を含まないことに注意します。
　このとき A^(k)[k : μ_A(k)] が論理式になることを、k について順に確かめていきます。
　そのためには、与えられた正整数 l £ | A | に対し、すべての k < l に対して成り立つと仮定して、k = l に対しても成り立つことを示せば十分です。そこで

(A1-10a)  s :º A(l)[l]

(A1-10b)  n :º ν(s)

(A1-10c)  l1 :º pd l

(A1-10d)  lr :º pd( μA(lr-1 ))       ( 1 < r £ n )

(A1-10e)  Ar :º A(l)[lr : μA(lr )]       ( 1 £ r £ n )

と置くと、(A1-2b) から明らかに μ_A(l) = ( μ_{A °} pd)ⁿ(l) = μ_A(( pd _° μ_A)^n-1(pd l )) = μ_A(l_n ) で、(A1-8a) により μ_A(l) ³ 1 ですから (A1-10c),(A1-10d) と (A1-3) により l > l₁ ³ ¼ ³ l_n ³ μ_A(l_n ) ³ 1 が成り立つので、仮定により B_r :º A^{(l_r )}[l_r : μ_A(l_r)] は論理式であることがわかります。
　さて、A^(l) と A^{(l_r )} を右から l_r 番目までの文字について比較すると、後者は、i £ l_r に対する前者の i 番目の文字が £_j の形でかつ l_r < i + j £ l である場合にこれを変数 x_{i + j} に置き換えたものになっています。
　ところで 1 < p £ n に対して μ_A(l_p-1 ) = l_p + 1 ですから、i + j = l となっているか、又は μ_A(l_p) £ i + j £ l_p となる正整数 p < r が存在するかどちらかです。
　ここで後者の場合、B_p は論理式ですから、(A1-6) により A^{(l_p )}[i + j : q] が準論理式であるような、すなわち A[i + j : q] が準論理式であるような自然数 q ³ μ_A(l_p ) が存在し、これは (A1-4) によれば μ_A(i + j) = q を意味し、μ_A(i + j) ³ μ_A(l_p ) > l_r ³ i となりますが、(A1-8e) によれば μ_A(i + j) £ i なので矛盾します。
　ゆえに、A^(l) と A^{(l_r )} を右から l_r 番目までの文字について比較すると、後者は、i £ l_r に対する前者の i 番目の文字が £_j の形でかつ i + j = l である場合にこれを変数 x_{i + j} すなわち x_l に置き換えたものになっていることがわかりました。
　一方、前者は変数 x_l を含みませんから、これは逆に言えば、右から l_r 番目までの文字について比較したとき、前者は、i £ l_r に対する後者の i 番目の文字が変数 x_l である場合に、これを束縛文字 £_l-i に置き換えたものになっているということを意味します。
　ところで A^(l)[l : μ_A(l)] は sA₁¼A_n と書けますから、この事実は、文字列 A^(l)[l : μ_A(l)] が、sB₁¼B_n に現れる変数 x_l をすべて（それぞれの位置から左端の s までの文字数を j として）束縛文字 £_j に置き換えることによって得られることを意味しています。
　そして、条件 (A1-8e) によれば、このような置き換えが生じている場合は必ず s が量化記号であることがわかります。
　更に、pd( ( μ_{A °} pd)^i-1(l) ) = l_i で、A^(l) の l_i 番目の文字は A_i の左端の文字ですから、条件 (A1-8c),(A1-8d) により、文字列 A^(l)[l : μ_A(l)] すなわち sA₁¼A_n は確かに論理式になっていることが確かめられました。
　さて、最後に l = | A | とすれば、(A1-8e) により A^(l) は A に一致するので、(A1-8b) により A^(l)[l : μ_A(l)] も A に一致することがわかり、これは A が論理式であることを意味しています。

　以上の議論により、与えられた文字列 A が論理式であるためには、(A1-8) が成り立つことが必要十分であることがわかりました。
　しかも上記の証明から明らかなように、与えられた論理式 A に対し、第 k 番目の要素が A^(k)[k : μ_A(k)] であるような、長さ | A | を持つ 2 階の文字列を C と書けば、C は A の一つの構成手続きになっていることもわかります。この C を A の（変数の組 x_i ( 1 £ i £ | A | ) を用いた）標準的な構成手続きとよぶことにしましょう。

　次に、与えられたsequentの列が証明文になっているかどうかを判定するアルゴリズムを考えてみましょう。

　一般に、sequent S は、® と , を無視することにより、その右から i 番目にある命題を第 i 成分に持つ 2 階の文字列とみなすことができます。
　また j < i のとき S[ j : i] は空な命題列を表すことにし、S[ | S | : i] を S[ : i] と略記し、S[i : 1] を S[i : ] と略記することにします。sequent S の右辺の命題は S[1] と書け、左辺は S[ : 2] と書けることに注意します。
　なお、証明文 P は、sequentからなる列ですから 3 階の文字列とみなすことができます。

　さて、sequentからなる 3 階の文字列 P が証明文になっているための条件を調べましょう。
　以下の議論では、一般にsequent S に対し、S[1] を S と略記し、S[2] を = 
S と略記することにし、各論理式 A に対して A に現れない | A | 個の相異なる変数 x_i ( 1 £ i £ | A | ) を用意し、 A[ | A | ] を A₀ と書き、n :º ν(A₀ ) , l₁ :º pd | A | , l_r+1 :º pd( μ_A(l_r )) ( 1 £ r < n ) と置いて A^{(l_r )}[l_r : μ_A(l_r )] を A_r と略記することにします。
　また、証明文 P の各要素、すなわち各正整数 k £ | P | に対する S :º P[k] に対し、正整数 i < k に対する S' :º P[i] は S の手前にあるということにします。

　このとき、sequentからなる列 P の要素 S が構造に関する推論規則のうち ( 同 一 ) , ( 仮 定 ) , ( 増 ) , ( 減 ) , ( 換 ) , ( 切 断 ) を適用して得られたものであるためには、順にそれぞれ次の各条件を満たすことが必要十分です：

(A1-13a)	S はその手前のある S' に一致する。
(A1-13b)	| S | ³ 2 で、S は =  S である。
(A1-13c)	| S | ³ 2 で、S の手前に S[ : 3] * { S } がある。
(A1-13d)	| S | ³ 2 で、S の手前に S[ : 2] * { =  S} * { S } がある。
(A1-13e)	2 £ i < j £ | S | を満たす i と j が存在し、S の手前に S[ : j + 1] * { S[i] } * S[ j - 1 : i + 1] * { S[ j] } * S[i - 1 : ] がある。
(A1-13f)	S の手前に S[ : 2] と S' [ : 2] が一致するような S' と S' * { S } がある。

　また、sequentからなる列 P の要素 S が論理接続詞の推論規則 (Ù 導入) , (Ù 消去) , (Ú 導入) , (Ú 消去) , (Þ 導入) , (Þ 消去) , (^ 消去) を適用して得られたものであるためには、順にそれぞれ次の各条件を満たすことが必要十分です：

(A1-14a)	S より手前に S' [ : 2] と S" [ : 2] が共に S[ : 2] に一致するような S' と S" があり、S は Ù S' S" である。
(A1-14b)	S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S'0 は Ù で、S は S'1 か S'2 のいずれかである。
(A1-14c)	S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S0 は Ú で、S' は S1 か S2 のいずれかである。
(A1-14d)	S より手前に S' [ : 2] と S" [ : 3] と S'" [ : 3] がすべて S[ : 2] に一致し、S" と S'" が共に S に一致するような S' と S" と S'" があり、 S' は Ú =   S"=    S'" である。
(A1-14e)	S より手前に S' [ : 3] が S[ : 2] に一致するような S' があり、S は Þ =  S'S' である。
(A1-14f)	S より手前に S' [ : 2] と S" [ : 2] が共に S[ : 2] に一致するような S' と S" があり、S' は Þ S" S である。
(A1-14g)	S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S' は { ^ } である。

　また、sequentからなる列 P の要素 S が (排中律) を適用して得られたものであるためには、次の条件を満たすことが必要十分です：

(A1-15)

l :º | S | - 1 , A :º S[l : μS(l)] と置くと、S は ÚAÞA^ である。

　残る構造に関する推論規則 ( 代 入 ) や量化記号の推論規則については、項の代入に関する考察が必要です。論理式 A の中の変数 x に項 T を代入する際、鎖を用いる流儀だと、ある鎖の両端の文字の間のどこかに変数 x があった場合、x に T を代入すると、この鎖は“引き伸ばされ”ます。これは、鎖を使わない流儀に翻訳すれば、£_i の i が変更されることを意味します。

　そこで、鎖を用いない流儀において、論理式 A の変数 x に項 T を代入して得られる論理式 (T | x)A を、改めて次のように定義することにします。
　まず、A にも T にも現れず、x とも異なる | A | 個の変数の組 x_i ( 1 £ i £ | A | ) を用いた A の標準的な構成手続きを C とし、C の各構成要素 B に対し、B' を次のように順に定義していきます：

(A1-16a)	B が { x } のとき、B' は T とする。
(A1-16b)	B が x 以外の変数 z により { z } と書けるとき、B' は { z } とする。
(A1-16c)	B が n 変項記号 s と B より手前に現れる論理式 Bi によって sB1¼Bn と書かれるとき、B' は sB1' ¼ Bn' とする。
(A1-16d)	B が量化記号 κ と、変数 xi と、B より手前に現れる論理式 D によって κxiD と書かれるとき、B' は κxiD' とする。

　このとき、C の最後の構成要素である A に対する A' のことを、A の変数 x に項 T を代入して得られる論理式とよんで、(T | x)A と書くことにします。
　なお、上記の定義において、変数の組を x_i ( 1 £ i £ | A | ) から別の組 y_i ( 1 £ i £ | A | ) に置き換えても、標準的な構成手続きの中の各 x_i がそれぞれ y_i に置き換わるだけなので、これらの変数を含まない A に対する A' は同一の文字列になり、(T | x)A の定義が変数の組 x_i ( 1 £ i £ | A | ) の選び方によらないことがわかります。従って特に、C に出てくる各 B に対する B' は、実は (T | x)B に他ならないことがわかります。すなわち

(A1-17a)	(T | x){ x } は T である。
(A1-17b)	z が x 以外の変数のとき、(T | x){ z } は { z } である。
(A1-17c)	s が n 変項記号で、論理式 Bi に対する (T | x)Bi を Bi' と書くとき、(T | x)(sB1¼Bn) は sB1' ¼ Bn' である。
(A1-17d)	κ が量化記号で、z が T に現れず x とも異なる変数で、論理式 D に対する (T | x)D を D' と書くとき、(T | x)(κzD) は κzD' である。

が成り立つことがわかります。
　更に、x が A に現れない場合は、A の標準的な構成手続きにおいて、その各構成要素 B に対して B' は B 自身であることがわかりますから、A' も A 自身です。
　また逆に x が A に現れる場合は、(A1-17a) により標準的な構成手続きのある段階に T が現れ、その後は、(A1-16d) の x_i は T に含まれないことから、x を含む構成手続きの要素 D に対する D' は、それが (A1-16c) により構成されたか (A1-16d) により構成されたかによらず、いずれの場合でもその一部に T を含むことがわかります。従って

(A1-18a)	x が A に現れないとき、B がある項 T によって (T | x)A と書けるならば、B は A 自身である。
(A1-18b)	x が A に現れるとき、B がある項 T によって (T | x)A と書けるならば、正整数 k £ | B | が存在して、T は B[k : μB(k)] である。

が成り立つことがわかります。

　さて、以上の議論をふまえて、sequentからなる列 P の要素 S が推論規則 ( 代 入 ) を適用して得られるための条件を求めてみましょう。
　これは、S より手前に同じ長さを持つ S' があり、変数 x と項 T が存在して、すべての正整数 i £ | S | に対して S[i] は (T | x)S' [i] と書けることと同値ですが、これをすべての正整数 i £ | S | に対して S' [i] が x を含まない場合と、いずれかの正整数 i £ | A | に対して S' [i] が x を含む場合に分けて考えることにします。
　まず前者の場合は、すべての正整数 i £ | A | に対して S[i] すなわち (T | x)S' [i] が S' [i] に一致するので、これは S' が S に一致することを意味します。
　また後者の場合は、S' [i] が x を含むような正整数 i £ | A | が存在し、そのような i に対しては S[i] すなわち (T | x)S' [i] が T を含むので、これは正整数 k £ | S[i] | が存在して S[i][k : μ_S[i](k)] が T に一致することを意味します。

　ゆえに、sequentからなる列 P の要素 S が構造に関する推論規則のうち ( 代 入 ) を適用して得られたものであるためには、次の条件を満たすことが必要十分です：

(A1-19)

S の手前に S と同一のsequentがあるか、又は S の手前に S と同じ長さを持つ S' と正整数 i £ | S' | と正整数 j £ | S' [i] | が存在して x :º S' [i][ j] は変数で、更に正整数 k £ | S[i] | が存在して T :º S[i][k : μS[i](k)] は項で、すべての正整数 r £ | S | に対して (T | x)S' [r] は S[r] に一致する。

　次に量化記号について考えます。
　まず、論理式 A に変数 x が含まれていなければ、量化記号 κ に対する κxA は { κ } * A と書けます。
　また、(" 導入) 及び ($ 消去) における変数 x に対する条件は、いずれの場合も x が下段のsequentに現れないことと同値です。

　従って、sequentからなる列 P の要素 S が量化記号の推論規則 (" 導入) , (" 消去) , ($ 導入) , ($ 消去) を適用して得られたものであるためには、順にそれぞれ次の各条件を満たすことが必要十分です：

(A1-20a)	S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S は { " } * S' であるか、又は正整数 i £ | S' | が存在して x :º S' [i] は変数であり、任意の正整数 k £ | S | と正整数 j £ | S[k] | に対して S[k][ j] は x と異なり、S は "xS' である。
(A1-20b)	S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S' は { " } * S であるか、又は T :º S[k : μS(k)] が項であるような正整数 k £ | S | が存在し、 S'0 は " で、S' に対して用意された変数の組 xi ( 1 £ i £ l :º | S' | ) を用いて S は (T | xl )S'1 と書ける。
(A1-20c)	S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S は { $ } * S' であるか、又は T :º S' [k : μS'(k)] が項であるような正整数 k £ | S' | が存在し、 S0 は $ で、S に対して用意された変数の組 xi ( 1 £ i £ l :º | S | ) を用いて S' は (T | xl )S1 と書ける。
(A1-20d)	S より手前に S' [ : 2] と S" [ : 3] が共に S[ : 2] に一致し S" が S に一致するような S' と S" があり、S' は { $ } * =   S" であるか、又は正整数 i £ | =   S"| が存在して x :º =   S"[i] は変数であり、 任意の正整数 k £ | S | と正整数 j £ | S[k] | に対して S[k][ j] は x と異なり、S' は $x=   S" である。

　さて、等号 = に関する推論規則 (= 消去) のように、論理式 A が (T | x)B の形に書けるかどうかを判定する必要が出てくる場合があります。
　この場合、もし B が x を含まなければ、A は B に一致します。
　またもし B が x を含むならば、x 以外の B の構成要素はすべて A の構成要素にもなっています。

　従って、sequentからなる列 P の要素 S が等号 º の推論規則 (º 導入) , (º 消去) を適用して得られたものであるためには、順にそれぞれ次の各条件を満たすことが必要十分です：

(A1-21a)	S0 は º で、S1 と S2 は同じ項である。
(A1-21b)	S より手前に S' [ : 2] と S" [ : 2] が共に S[ : 2] に一致し、S'0 が º であるような S' と S" があり、S が S" に一致するか又は、S にも S" にも現れない変数 x を選んだとき、| A | £ | S | であって、かつすべての正整数 i £ | A | に対し、A[i] は x であるか又はある正整数 j £ | S | に対する S[ j] であるような命題 A が存在して、 S" は (S'1 | x)A で、S は (S'2 | x)A である。

　また、sequentからなる列 P の要素 S がε量化記号の推論規則 (ε 導入) を適用して得られたものであるためには、次の条件を満たすことが必要十分です：

(A1-22)

S より手前に S' [ : 2] が S[ : 2] に一致するような S' があり、S が S' に一致するか又は、S にも S' にも現れない変数 x を選んだとき、 | A | £ | S | であって、かつすべての正整数 i £ | A | に対し、A[i] は x であるか又はある正整数 j £ | S | に対する S[ j] であるような命題 A が存在し、更に T :º S' [k : μS'(k)] が項であるような正整数 k £ | S' | が存在して、S' は (T | x)A で、S は (εxA | x)A である。

　また、sequentからなる列 P の要素 S が冪理論の推論規則 (t^P 導入) , (Î 導入) , (Î 消去) を適用して得られたものであるためには、順にそれぞれ次の各条件を満たすことが必要十分です：

(A1-23a)	l :º | S | > 2 で、S[l] は tP であり、S[l - 1] は {|} である。
(A1-23b)	S より手前に S' [ : 2] と S" [ : 2] が共に S[ : 2] に一致するような S' と S" があり、S'0 は t で、S0 は Î で、S1 は S'1 で、S2 を A と書くとき、A0 は {|} で、 A に対して用意された変数の組 xi ( 1 £ i £ l :º | A | ) を用いて S" は (S'1 | xl )A1 と書ける。
(A1-23c)	S より手前に S' [ : 2] と S" [ : 2] が共に S[ : 2] に一致するような S' と S" があり、S'0 は t で、S"0 は Î で、S"1 は S'1 で、S"2 を A と書くとき、A0 は {|} で、 A に対して用意された変数の組 xi ( 1 £ i £ l :º | A | ) を用いて S は (S'1 | xl )A1 と書ける。

　また、再帰的集合論において、sequentからなる列 P の要素 S が分出公理（本文第５節 (Set-5) 参照）を適用して得られたものであるためには、次の条件を満たすことが必要十分です：

(A1-24)

S に対して用意された変数の組 xi ( 1 £ i £ r :º | S | ) に対し、正整数 k £ r が存在して、A :º S (k)[k : μS(k)] と置くと、A は命題で、 S は "xr Þ set xr $xr-4 Ù set xr-4 "xr-8 Þ t' xr-8 Ù Þ Î xr-8 xr-4 Ù Î xr-8 xr A Þ Ù Î xr-8 xr A Î xr-8 xr-4 と書ける。

　また、定項 0 と１変項関数記号 s を持つ理論（自然数論）において、sequentからなる列 P の要素 S が、次の形の推論規則（数学的帰納法）：

(A1-25)

(0 | x)R   R├ (sx | x)R ——————   ( x¢As )      (T | x)R

を適用して得られたものであるためには、次の条件を満たすことが必要十分です：

(A1-26)

S より手前に S' [ : 2] と S" [ : 3] が共に S[ : 2] に一致するような S' と S" があり、S' と =   S" と S" がすべて S と一致するか又は、正整数 i £ | =   S"| と正整数 k £ | S | が存在して、x :º =   S"[i] 及び T :º S[k : μS(k)] と置くと、 x は変数、T は項で、すべての正整数 l £ | S' | と正整数 j £ | S' [l] | に対して S' [l][ j] が x でなく、S' が (0 | x)=   S" に、S" が (sx | x)=   S" に、S が (T | x)=   S" にそれぞれ一致する。

　最後に 3 階の文字列 P がある理論における証明文であるためには、任意の正整数 i £ | P | と j £ | P[i] | に対し、P[i][ j] は命題で、かつ任意の正整数 i £ | P | に対し、S :º P[i] が (A1-13)~(A1-15),(A1-19)~(A1-22) あるいは (A1-23),(A1-24),(A1-26) のような各理論に固有の推論規則のいずれかを満たすことが必要十分です。そして、このとき P がsequent S の証明であるための条件は、P[i] が S であるような正整数 i £ | P | が存在することです。