数学の基礎

２．推論規則の性質

　前節で、構造に関する推論規則をいくつか掲げましたが、この中のいくつかは、具体的に与えられた理論の中では、推論規則として敢えて規定しなくても、導出できてしまうことがあります。
　例えば、( 同 一 ) という推論規則は、前節で与えられた推論規則の全部又は一部のみを推論規則に持つような理論では自動的に成り立ちます。
　なぜなら、sequent Φ が既に証明されている場合、その証明をもう一度全部コピーして書き加えれば、それが同じ Φ の証明になるからです。

　本節では、推論規則に関するこのような性質を体系的に調べます。
　なお、証明文 P やsequent Φ の中の変数 x を項 T で一斉に置き換えたものに対しても (T | x) の記法を用いることにします。

メタ定理１ 　P を、前節で与えられた推論規則の全部又は一部のみを推論規則に持つ理論における証明文とし、x を変数、y を P に現れず、x と異なる変数とすれば、( y | x)P も証明文である。

　実際、P を構成する各sequent Φ に対し、( y | x)Φ が、( y | x)P において、Φ を導いたのと同じ推論規則を適用することにより得られることを順に示していきましょう。
　この主張が Φ より手前のsequentまでは成り立つものと仮定します。
　Φ が P1 ,¼, Pn ® R のとき、( y | x)Pi と ( y | x)Q をそれぞれ Pi' , Q' と書けば、( y | x)Φ は P1' ,¼, Pn' ® R' ですから、用いた推論規則が ( 代 入 ), ( " 導入), ( " 消去), ( $ 導入), ( $ 消去) 以外の場合は明らかです。

　次に、Φ が sequent Ψ に ( 代 入 ) を適用して得られる (T | z)Ψ である場合を考え、( y | x)T を T' と書き、( y | x)Ψ を Ψ' と書きます。
　ここで z が x と同じ変数なら ( y | x)Φ は (T' | z)Ψ と書け、これはまた (T' | y)Ψ' とも書けます。
　また z が x と異なり y と同じ変数なら、仮定により y すなわち z は Ψ に現れないので Φ は Ψ そのものです。ゆえに ( y | x)Φ は Ψ' であり、しかも Ψ' は変数 x を含まないので、これはまた (T' | x)Ψ' とも書けます。
　また z が x とも y とも異なる変数なら、( y | x)Φ は (T' | z)Ψ' です。
　以上で、使った推論規則が ( 代 入 ) の場合には成り立つことが確認できました。

　次に、用いた推論規則が " 又は $ に関する推論規則である場合を統一的に考察しましょう。

　まず、κ が " 又は $ で、Φ が Γ ® κzP である場合を考え、( y | x)P と ( y | x)Γ をそれぞれ を P' , Γ' と書きます。
　ここで z が x と同じ変数なら、前節の退避変換のところで述べたように、( y | x)Φ は Γ' ® κyP' です。
　また z が x と異なり y と同じ変数なら、同様に ( y | x)Φ は Γ' ® κxP' です。
　また z が x とも y とも異なる変数なら、同様に ( y | x)Φ は Γ' ® κzP' です。

　次に、Φ が Γ ® (T | z)P である場合を考え、( y | x)P と ( y | x)T と ( y | x)Γ をそれぞれ P' , T' , Γ' と書きます。
　ここで z が x と同じ変数なら、上記の ( 代 入 ) のときの議論により、( y | x)Φ は Γ' ® (T' | y)P' です。
　また z が x と異なり y と同じ変数なら、同様に ( y | x)Φ は Γ' ® (T' | x)P' です。
　また z が x とも y とも異なる変数なら、同様に ( y | x)Φ は Γ' ® (T' | z)P' です。

　次に、Φ が Γ ® P の場合は、( y | x)P と ( y | x)Γ をそれぞれ P' , Γ' と書けば、( y | x)Φ は Γ' ® P' です。

　次に、z¢Γ の場合を考え、( y | x)Γ を Γ' と書きます。
　ここで z が x と同じ変数なら、z¢Γ ですから Γ' は Γ であり、従ってこれと仮定により y¢Γ' です。
　また z が x と異なり y と同じ変数なら、x と y は異なる変数ですから x¢Γ' です。
　また z が x とも y とも異なる変数なら、しかも z¢Γ ですから z¢Γ' です。

　以上の結果と、最後から２番目の段落で P のかわりに Q としたもの、Γ のかわりに Γ, P とし、P のかわりに Q としたもの、また最後の段落で Γ のかわりに Γ, Q としたものを組み合わせれば、使った推論規則が " 又は $ に関する推論規則の場合にも成り立つことがわかり、これですべての場合について検証できました。
　このメタ定理１のような証明文の変数の置き換えを、証明文の退避変換とよぶことにしましょう。

メタ定理２ 　前節で与えられた推論規則の全部又は一部のみを推論規則に持つ理論では、構造に関する推論規則 ( 代 入 ) は導出可能である。すなわちsequent Φ が定理、x が変数、T が項なら (T | x)Φ も定理である。

　実際、P を証明文、Φ をそこに現れる任意の定理、P に、T に現れない変数への退避変換を何回か（0回でもよい）施したものを P ' とするとき、その Φ に対応する構成要素 Φ' から作った (T | x)Φ' を Φ'* と書くとき、これが必ず定理になることを、各構成要素 Φ について順に確かめていきます。
　この主張が Φ より手前のsequentまでは成り立つものと仮定します。

　まず、Φ が Γ ® P なら、Φ'* は Γ'* ® P'* ですから、用いた推論規則が ( 代 入 ) , ( " 導入) , ( " 消去) , ( $ 導入) , ( $ 消去) 以外の場合は明らかです。また、( 代 入 ) については、考えている理論がこれを推論規則に持つなら結論は自明です。ゆえにあとは、用いた推論規則が " と $ に関する推論規則である場合について確かめれば十分です。

　そこで、Φ が Γ ® P から ( " 導入) によって得られた Γ ® "zP である場合を考えます。ただし z は z¢Γ であるような変数です。
　このとき、メタ定理１により、Φ' は、z'¢Γ' であるような変数 z' によって Γ' ® "z'P' と書かれます。
　そこで、P にも T にも現れず、上記の退避変換に登場する変数とも x とも異なる変数 y を取ると、Φ'* は (T | x)( y | z')Γ' ® "y(T | x)( y | z')P' と書けます。ゆえに P ' から更に z' を y に置き換える退避変換を行ったものを " を付けて表せば、Φ'* は Γ"* ® "yP"* となります。
　一方、メタ定理１により Γ" ® P" は定理であり、仮定により Γ"* ® P"* も定理です。ところが明らかに y¢Γ"* ですから、( " 導入) により Φ'* は定理です。

　次に、κ を " 又は $ とし、Γ ® κzP を Φ 、Γ ® (S | z)P を Ψ と書くことにすれば、メタ定理１により、Φ' と Ψ' は、ある共通の変数 z' により、それぞれ Γ' ® κz'P' 及び Γ' ® (S' | z')P' と書けます。
　ゆえに、x と異なり T にも P' にも現れない変数 y を取れば、Φ'* は Γ'* ® κy(T | x)( y | z')P' と書けるので、( y | z')P' を P" 略記すれば、これは更に Γ'* ® κyP"* と書くことができます。
　一方、Ψ'* は Γ'* ® (T | x)(S' | z')P' と書けますが、これは更に Γ'* ® (S'* | y)(T | x)( y | z')P' すなわち Γ'* ® (S'* | y)P"* と書くことができます。
　ゆえに、κ が " で、Φ が既に証明されていて、用いた試論規則が ( " 消去) のときは、仮定から Φ'* は定理であり、従って ( " 消去) により Ψ'* が導かれます。
　また、κ が $ で、Ψ が既に証明されていて、用いた試論規則が ( $ 導入) のときは、仮定から Ψ'* は定理であり、従って ( $ 導入) により Φ'* が導かれます。

　最後に、Φ が Γ ® $zP と Γ, P ® Q から ( $ 消去) によって得られた Γ ® Q である場合を考えます。ただし z は z¢Q, Γ であるような変数です。
　このとき、メタ定理１により、変数 z'¢Q', Γ' が存在して、Γ' ® $z'P' と Γ', P' ® Q' は定理です。
　ゆえに、仮定により (T | x)( Γ' ® $z'P') は定理ですが、P にも T にも現れず、上記の退避変換に登場する変数とも x とも異なる変数 y を取ると、これは (T | x)Γ' ® $y(T | x)( y | z')P' と書け、更に ( y | z')P' を P" 略記すれば、これは Γ'* ® $yP"* と書くことができます。
　また、P ' から更に z' を y に置き換える退避変換を行ったものを " で表せば、仮定により (T | x)( Γ", P" ® Q") は定理ですが、z'¢Q', Γ' なので、これは更に (T | x)Γ', (T | x)( y | z')P' ® (T | x)Q' すなわち Γ'*, P"* ® Q'* と書くことができます。
　ここで y¢Q'*, Γ'* なので、これら２つの定理と ( $ 消去) により、Γ'* ® Q'* すなわち Φ'* が導かれます。

　以上でメタ定理２の成立が確かめられました。

メタ定理３ 　前節で与えられた推論規則の全部又は ( 換 ) を含む一部のみを推論規則に持つ理論では、構造に関する推論規則 ( 増 ) は導出可能である。すなわちsequent Γ ® Q が定理、P が命題なら Γ, P ® Q も定理である。

　実際、P を任意の命題、P を任意の証明文とし、P に出てくる全ての変数 x1 ,¼, xn を、P にも P にも現れない相異なる変数 z1 ,¼, zn で順次置き換えて得られる (z1 | x1)¼(zn | xn)P は、メタ定理１により証明文です。これを P ' と書くことにします。
　次に、P ' の構成要素 Γ' ® Q' をすべて Γ', P ® Q' で置き換えたものを P " と書くと、P に現れる変数は P ' に一切現れないので、Γ' ® Q' に出てくる自由変数は Γ', P ® Q' の自由変数です。
　このことを使って、証明文 P ' の構成要素 Γ' ® Q' に対する Γ', P ® Q' が定理であることを、順に示していきましょう。ただし、メタ定理２により P 従って P ' では、推論規則 ( 代 入 ) を使っていないと仮定することができます。

　まず、Γ' ® Q' が ( 代 入 ), ( " 導入), ( $ 消去) 以外の推論規則によって導かれたもである場合は、Γ', P ® Q' は、明らかに同じsequentに対応するsequentから、同じ推論規則と ( 換 ) の組み合わせによって導くことができます。

　また、Γ' ® Q' が Γ' ® R' から ( " 導入) によって導かれた Γ' ® "zR' である場合を考えると、z は Γ' に現れません。
　しかも z が R' に現れる場合は、仮定により z¢P で、そうでない場合は "zR' は "R' ですから、これは Γ' にも P にも R' にも現れない変数 z' により "z'R' と書くことができるので、いずれにせよ z¢P と仮定することができます。
　ゆえに、Γ', P ® Q' すなわち Γ', P ® "zR' は、Γ', P ® R' から ( " 導入) によって導くことができます。

　また、Γ' ® Q' が Γ' ® $zR' と Γ', R' ® Q' から ( $ 消去) によって導かれた場合を考えると、z は Γ' にも Q' にも現れません。
　しかも z が R' に現れる場合は、仮定により z¢P で、そうでない場合は $zR' は $R' ですから、これは Γ' にも P にも R' にも Q' にも現れない変数 z' により $z'R' と書くことができるので、いずれにせよ z¢P と仮定することができます。
　ゆえに、Γ', P ® Q' は、Γ', P ® $zR' と Γ', R', P ® Q' から ( 換 ) と ( $ 消去) によって導くことができます。

　以上により P " の構成要素はすべて定理であることがわかったので、メタ定理２により (x1 | z1)¼(xn | zn)P " の各構成要素はすべて定理です。これは P の構成要素 Γ ® Q に対する Γ, P ® Q がすべて定理であることを意味しています。

メタ定理４ 　前節で与えられた推論規則の全部又は ( 換 ) を含む一部のみを推論規則に持つ理論では、構造に関する推論規則 ( 切 断 ) は導出可能である。すなわちsequent Γ ® P と Γ, P ® Q が定理なら Γ ® Q も定理である。

　実際、メタ定理２とメタ定理３により、Γ, P ® Q の証明 P で、推論規則に ( 代 入 ) と ( 増 ) を使っていないものが存在します。ところがそれ以外の推論規則では、下段のsequentの仮定は、上段のsequentの仮定と順序を除いて同じか、それより少ない仮定を持っています。言い換えると、推論するたびに、仮定は減りこそすれ、増えることはありません。
　従って、P から、必要なら推論に使わないsequentをすべて削除することにより、P に現れるすべてのsequent Φ は、仮定の並べ方の順序を除いて Γ, P ,¼, P, Δ ® R という形をしていると仮定することができます（ただし P は１個以上並んでいるものとし、Δ に P が現れていてもかまわない）。
　このとき、sequent Γ, Δ ® R がすべて定理であることを順に示していきましょう。これが示せれば、仮定により Γ, P ® Q は定理なので Γ ® Q も定理であることがわかります。
　そこで、この主張が Φ より手前のsequentまでは確認できたと仮定します。

　まず Φ が推論規則 ( 仮 定 ) を使って得られたものである場合は、R は P であるか、Γ か Δ に現れるかのいずれかです。
　ここで R が P のときは、仮定により Γ ® P は定理ですから、メタ定理３と ( 換 ) により Γ, Δ ® P すなわち Γ, Δ ® R は定理です。
　また、R が Γ 又は Δ に現れるときは、推論規則 ( 換 ) と ( 仮 定 ) により Γ, Δ ® R は定理です。

　また Φ がsequent Γ, P ,¼, P, Δ, S ® R （に ( 換 ) を何回か適用したもの）から推論規則 ( 減 ) を使って得られたもの（に ( 換 ) を何回か適用したもの）である場合、S は P であるか、Γ か Δ に現れるかのいずれかです。
　ここで S が P の場合、仮定により Γ, Δ ® R は定理です。
　また、S が Γ か Δ に現れる場合は、( 仮 定 ) を用いることにより Γ, Δ ® R は導かれます。

　また Φ が推論規則 ( 同 一 ), ( 換 ), ( " 消去), ( $ 導入) 又は論理接続詞に関する推論規則を使って得られたものである場合、Φ は、それより手前にある Γ, P ,¼, P, Δ ® B 又は Γ, P ,¼, P, Δ, A ® B の形のsequentから当該推論規則を用いて得られます。
　従って、Γ, Δ ® R は、仮定により定理である Γ, Δ ® B 又は Γ, Δ, A ® B の形のsequentから当該推論規則を用いて得られます。

　次に、Φ が Φ より手前の Γ, P ,¼, P, Δ ® A から ( " 導入) により得られた Γ, P ,¼, P, Δ ® "xA である場合、x はこれの仮定に現れないので、もちろん Γ, Δ に現れません。
　従って、Γ, Δ ® R は、仮定により定理であることがわかっている Γ, Δ ® A から ( " 導入) により導かれます。

　最後に、Φ が Φ より手前の Γ, P ,¼, P, Δ ® $xA と Γ, P ,¼, P, Δ, A ® R から ( $ 消去) により得られた場合、x は前者の仮定にも R にも現れないので、もちろん Γ, Δ, R には現れません。
　従って、Γ, Δ ® R は、仮定により定理であることがわかっている Γ, Δ ® $xA と Γ, Δ, A ® R から ( $ 消去) により導かれます。

　以上でメタ定理４は証明されました。

　ところで、推論規則 ( 減 ) は、( 仮 定 ) と ( 切 断 ) から導出可能です。
　なぜなら、Γ, P, P ® Q が定理なら、( 仮 定 ) から Γ, P ® P が得られ、この２つのsequentから ( 切 断 ) により Γ, P ® Q が得られるからです。

　以上の議論により、前節で与えられた推論規則の全部又は ( 仮 定 ), ( 換 ) を含む一部のみを推論規則に持つ理論では、構造に関する他の推論規則はすべて導出可能である（従って推論規則として規定する必要がない）ことがわかります。

　今後、(P Þ Q) Ù (Q Þ P) のことを P Û Q と略記します。P Û Q が定理であるということは、( Ù 導入) と ( Ù 消去) により P Þ Q と Q Þ P が共に定理であるということであり、これはまた ( Þ 導入) と ( Þ 消去) により、P と Q の一方から他方が得られることを意味しますから、このとき、P と Q は同値であるといいます。
　また、P Þ Q が定理であるとき、Q は P の必要条件である、又は P は Q の十分条件であるともいいます。その意味で、同値であるというかわりに必要十分条件(あるいは単に条件)ともいいます。

　次の２つのメタ定理は、直観主義論理では、各論理記号の消去規則が導入規則に“共役”な推論規則であることを意味しています（付録２参照）。

メタ定理５ 　論理記号 Ù , Ú , Þ , ^ , " , $ とその消去規則のみを推論規則として与えた理論を考え、そこに新しい論理記号 Ù' , Ú' , Þ' , ^' , "' , $' を追加し、ぞれぞれに対し、Ù , Ú , Þ , ^ , " , $ の導入規則と同じ推論規則を与えるものとする。
　このとき、もし P から P' が、Q から Q' がそれぞれ導かれれば、P Ù Q から P' Ù' Q' が、P Ú Q から P' Ú' Q' が、P' Þ Q から P Þ' Q' が、^ から ^' が、それぞれ導かれる。
　また、x が自由変数なら、"xP から "' xP' が、$xP から $' xP' が、それぞれ導かれる。

　まず P Ù Q と仮定すると、( Ù 消去) により P と Q が得られ、条件により P' と Q' が得られるので、( Ù' 導入) により P' Ù' Q' が得られます。

　次に P Ú Q と仮定します。更に P を仮定すれば、条件により P' が得られるので ( Ú' 導入) により P' Ú' Q' が得られ、他方 Q を仮定すれば、条件により Q' が得られるのでやはり ( Ú' 導入) により P' Ú' Q' が得られますから、( Ú 消去) により P' Ú' Q' が得られます。

　次に P' Þ Q と仮定します。更に P と仮定すれば、条件により P' が成り立つので ( Þ 消去) により Q が得られ、条件により Q' が得られるので ( Þ' 導入) により P Þ' Q' が得られます。

　次に ^ と仮定すると、( ^ 消去) により ^' が得られます。

　次に x を自由変数とし、"xP と仮定すると、( " 消去) により P が得られ、条件により P' が得られ、( "' 導入) により "' xP' が得られます。

　最後に $xP と仮定します。更に P を仮定すると、条件により P' なので、( $' 導入) により $' xP' が得られ、( $ 消去) により $' xP' が得られます。

　このメタ定理５により、特に直観主義論理においては、いくつかの命題を論理記号で結んで作った命題の中に現れる特定の命題を同値な命題で置き換えたものは同値になることがわかります。

メタ定理６ 　直観主義論理における ^ , Ù , Ú , Þ , " , $ の各消去規則の上段の一番上の式を、対応する導入規則の上段全体で置き換えて得られる推論図は、構造に関する推論規則のみによって導出可能である。

　この証明に先立って、このメタ定理の意味するところを説明しましょう。
　各論理記号の導入規則及び消去規則は一般に複数個存在するので(例えば Ù の消去規則と Ú の導入規則はそれぞれ２個存在する）、それぞれの導入規則と消去規則の名前に、第１節で掲げた順番で添え字を付けて区別することにします。このとき、メタ定理６が主張しているのは、例えば論理記号 Ù の場合、

    ( Ù 導入1 ) ( Ù 消去1 )
    P
Q
———
P Ù Q
の上段で
P Ù Q
———
P
の P Ù Q を置き換えたもの

すなわち、次に掲げる図式 ( Ù11 ) が、構造に関する推論規則のみによって導出可能であるという主張です。
　他の組み合わせについても、論理記号 s の ( s 消去j ) の上段の最初の式を ( s 導入i ) の上段で入れ替えた図式を ( sij ) と書けば、それらの全体は次のようになります（ちなみに導入規則を持たない ^ に対するものはありません）：

( Ù11 ) ( Ù12 ) ( Ú11 ) ( Ú21 ) ( Þ11 )   ( "11 )   ( $11 )
P
Q
———
P		 P
Q
———
Q		 P
P├ R
Q├ R
———–
R		 Q
P├ R
Q├ R
———–
R		 P├ Q
P
———–
Q		       P
———– (x¢As)
 (T | x)P		  (T | x)P
  P├ Q
———— (x¢As, Q )
      Q

　さて、これらのうち、左から１〜２番目のものは ( 同 一 ) により、左から３〜５番目のものは ( 切 断 ) により導出可能です。
　また、右から２番目のものは、仮定を Γ として、sequentによる推論に書きなおせば、

Γ ® P
——————
Γ ® (T | x)P

となりますが、x¢Γ なので、下段のsequentは、上段のsequentの x を T に置き換えたものに他なりません。すなわちこの推論は、構造に関する推論規則 ( 代 入 ) により導出可能です。
　最後に一番右のものは、仮定を Γ として、sequentによる推論に書きなおせば、

Γ ® (T | x)P
Γ, P ® Q
——————
Γ ® Q

となりますが、上段の２番目の式に構造に関する推論規則 ( 代 入 ) を用いて x に T を代入すると、x¢Γ, Q なので、定理 Γ, (T | x)P ® Q が得られます。ゆえにこれと上段最初の式に ( 切 断 ) を用いれば、下段のsequentが導出可能であることがわかります。
　以上でメタ定理６は証明されました。

INDEX　　　BACK　　　NEXT