数学の基礎

　第１節で、具体的な論理記号として論理接続詞と命題型量化記号を導入しましたが、本節では他の記号を導入します。

　数学では、２つの項が同じものであるということを意味する命題があると便利です。そこで、引数2個の述語記号 º を次の導入規則：

( º 導入)

T º T

及び消去規則：

( º 消去)

S º T (S | x)P ————— (T | x)P

とともに導入することにします。これらの推論規則は、S º T という命題が“項 S と T は同じものである”ということを論理式として表現したものであるということが形式化の原理により導かれます（付録２参照）。

　述語記号 º と上の２つの推論規則を持つ理論を等号を持つ理論といい、記号 º を等号とよび、S º T を“S と T は等しい”と読みます。なお、等号は = で表わすのが普通ですが、本稿では後で定義する同値関係を表わすのにしばしば記号 = を用いるので、等号には º を使うことにします。
　さて、等号についても第２節メタ定理５、メタ定理６と同様な次の性質が成り立ちます：

メタ定理41

º については消去規則のみ仮定し、º' が º の導入規則と同じ推論規則を持つ述語記号ならば、項 S と T に対し、S º T から S º' T が導かれる。 　特に、º' が º と同一の推論規則を持つ述語記号ならば、S º T と S º' T は同値。 　また、( º 導入) を ( º 導入)' S º T       ( S と T は同じ記号列 ) という条件付きの推論規則の形に書き直すと、( º 消去) の上段の一番上の式を ( º 導入)' の上段、すなわち空な式で置き換えたものは、構造に関する推論規則によって導出可能である。

　実際、S º T と仮定します。命題 S º' x を P と書くと、( º' 導入) により S º' S が成り立ちますが、これは (S | x)P と書けるので、( º 消去) により (T | x)P が導けますが、これは S º' T に他なりません。
　またメタ定理の後半は、S と T が同じ記号列ですから、この置き換えられた推論図は、推論規則 ( 同 一 ) により導出可能です。

　また、メタ定理１〜４は、等号を持つ理論においても成立します：

メタ定理42

第１節で与えられた推論規則と等号の推論規則の全部又は一部を持つ理論では、推論規則 ( 同 一 ), ( 代 入 ) は導出可能である。もし更に ( 換 ) を推論規則に持つならば、( 増 ), ( 減 ), ( 切 断 ) も導出可能である。

　実際、メタ定理１〜４の各証明において、用いた推論規則が ( º 導入) 又は ( º 消去) の場合にも成り立つことを示せばよいのですが、( º 導入) の場合は明らかですから ( º 消去) の場合のみ検証すれば十分です。

　まずメタ定理１を検証します。( y | x)S , ( y | x)T , ( y | x)P をそれぞれ S' , T' , P' と書くと、( y | x){S º T } は S' º T' です。
　また、A が (S | z)P のとき、z が x と同じ変数なら ( y | x)A は (S' | y)P' です。
　また z が x と異なり y と同じ変数なら、同様に ( y | x)A は (S' | x)P' です。
　また z が x とも y とも異なる変数なら、同様に ( y | x)A は (S' | z)P' です。
　ゆえに、用いた推論規則が ( º 消去) の場合にも成り立つことがわかります。

　次にメタ定理２を検証します。同証明における Φ が、Γ ® S º U （これを Ψ とします）と Γ ® (S | z)P （これを Ω とします）から ( º 消去) によって得られた Γ ® (U | z)P である場合を考えれば十分です。
　このとき、上記の結果を用いると、Ψ' , Ω' , Φ' は、ある共通の変数 z' により、それぞれ Γ' ® S' º U' , Γ' ® (S' | z')P' , Γ' ® (U' | z')P' と書けます。
　ゆえに、Ψ'* は Γ'* ® S'* º U'* と書けます。
　一方、Ω'* は Γ'* ® (T | x)(S' | z')P' と書けますが、これは更に Γ'* ® (S'* | y)(T | x)( y | z')P' すなわち Γ'* ® (S'* | y)P"* と書くことができます。同様に、Φ'* も Γ'* ® (U'* | y)P"* と書くことができます。
　仮定により、Ψ'* と Ω'* は定理ですから、これらに ( º 消去) を適用して得られる Φ'* も定理であることがわかります。

　メタ定理３とメタ定理４については、何の変更点もなく、用いた推論規則が ( º 消去) の場合にもそのまま通用します。
　以上でメタ定理42は証明されました。

　さて、２つの変数 x，y に関する関係 x = y が次の３条件を満たすとき、これを同値関係といいます。

(4-1a)  x = x

(4-1b)  x = y  Þ  y = x

(4-1c)  ( x = y  Ù  y = z )  Þ  x = z

　関係 x º y は同値関係です。
　実際、(4-1a) は ( º 導入) そのものです。
　また命題 u º x を P と書けば、(4-1a) により (x | u)P が成り立ち、これと x º y から ( º 消去) により ( y | u)P すなわち y º x が導かれ、これは (4-1b) に他なりません。
　最後に命題 x º u を Q と書けば、仮定 x º y は ( y | u)Q と書かれ、これと y º z から ( º 消去) により (z | u)Q すなわち x º z が導かれ、これは (4-1c) に他なりません。

　なお、等号を用いて、一意存在 $!xP を

(4-2)  $!xP :º $x(P Ù "y( ( y| x)P Þ y º x ) )

で定義します（ただし :º は左辺を右辺で定義するという意味のメタ記号です）。また、この右辺の º を同値関係 = で置き換えた場合は、これを = に対する一意存在といい、紛れのない限り、やはり $!xP で表わします。

　さて、次は項型の量化記号の導入です。

　命題 P と変数 x が与えられ、(T | x)P を満たす項 T が見つかったとき、そのような項 T の具体的な表示式には興味がなく、ただそれが P を満たすモノであるということだけがわかればよい、という場合があります。そこで、このような場合、P を満たす項のうちの任意の一つを εxP と略記することにすれば、次が成立します：

(4-3)

命題 P と変数 x と項 T に対し、(T | x)P が成り立てば、(εxP | x)P が成り立つ。

　一見、P を満たす項を具体的に特定して（例えば考察している公理系のもとで P を満たすことが証明された最初の項）、それを εxP と表わすことにすれば、そのような特定の項 T に対して εxP º T という命題が成り立つので更に便利になるように見えます。
　ところが、それだと公理系 Γ のもとで εxP が意味する項 T と、公理系 Γ, R のもとで εxP が意味する項 T' は一般に一致しないため、εxP を含んだ命題に対して、( 増 ) や ( Þ 導入) のような、異なる公理系間を跨がるタイプの推論規則を適用することができなくなり、かえって不便です。

　さて、ここで εxP という概念を形式化します。すなわち εxP を、(T | x)P を満たすある項 T を表す省略記号と考えるのではなく、引数が命題の項型量化記号 ε を新規に追加し、更に上記の (4-3) を推論規則に“翻訳”した次の推論規則：

( ε 導入)

(T | x)P ————— (εxP | x)P

を当該理論に新規に追加することにします。こうして導入された論理記号 ε をε量化記号といいます。

　論理記号 ^ とは逆に、このε量化記号には消去規則がありません。なぜなら、これ以上推論規則を追加しなくても、第２節メタ定理５に対応する次のメタ定理が成り立つからです：

メタ定理43

ε については推論規則を仮定せず、ε' が ε の導入規則と同じ推論規則を持つ項型量化記号ならば、命題 P と変数 x と項 T に対し、(εxP | x)P から (ε' xP | x)P が導かれる。 　特に、ε' が ε と同一の推論規則を持つ項型量化記号ならば、(εxP | x)P と (ε' xP | x)P は同値。

　実際、( ε' 導入) において、εxP を T とみなせば明らかです。

　ε量化記号を導入することにより、P を満たす x が存在するとき、“そのような x”を項として表わすことができるようになります。そこで、実際の推論においては、P を満たす x の存在が導かれたとき、“そのようなもの(の一つ)を ☆☆☆ と表わす”という表現で、記号列 εxP のことを ☆☆☆ という省略記号で表わすことを意味するものとします。
　さて、メタ定理１〜４はε量化記号を持つ理論においても成立します：

メタ定理44

第１節で与えられた推論規則と等号の推論規則とε量化記号の推論規則の全部又は一部を持つ理論では、推論規則 ( 同 一 ), ( 代 入 ) は導出可能である。もし更に ( 換 ) を推論規則に持つならば、( 増 ), ( 減 ), ( 切 断 ) も導出可能である。

　実際、メタ定理１〜４の各証明において、用いた推論規則が ( ε 導入) の場合のみを検証すれば十分です。

　まずメタ定理１を検証します。( y | x)S , ( y | x)P をそれぞれ S' , P' と書きます。
　まず、A が εzP のとき、z が x と同じ変数なら ( y | x)A は εyP' です。
　また z が x と異なり y と同じ変数なら、同様に ( y | x)A は εxP' です。
　また z が x とも y とも異なる変数なら、同様に ( y | x)A は εzP' です。
　一方、A が (S | z)P のとき、z が x と同じ変数なら ( y | x)A は (S' | y)P' です。
　また z が x と異なり y と同じ変数なら、同様に ( y | x)A は (S' | x)P' です。
　また z が x とも y とも異なる変数なら、同様に ( y | x)A は (S' | z)P' です。
　ゆえにこれらを組み合わせると、A が (εzP | z)P のとき、z が x と同じ変数なら ( y | x)A は (εyP' | y)P' です。
　また z が x と異なり y と同じ変数なら、同様に ( y | x)A は (εxP' | x)P' です。
　また z が x とも y とも異なる変数なら、同様に ( y | x)A は (εzP' | z)P' です。
　ゆえに、用いた推論規則が ( ε 導入) の場合にも成り立つことがわかります。

　次にメタ定理２を検証します。同証明における Φ が、Γ ® (S | z)P （これを Ψ とします）から ( ε 導入) によって得られた Γ ® (εzP | z)P である場合を考えれば十分です。
　このとき、上記の結果を用いると、Ψ' , Φ' は、ある共通の変数 z' により、それぞれ Γ' ® (S' | z')P' , Γ' ® (εz'P' | z')P' と書けます。
　ゆえに Ψ'* は、メタ定理42の証明と同様に Γ'* ® (S'* | y)P"* と書くことができます。
　一方、Φ'* は Γ'* ® (T | x)(εz'P' | z')P' と書けますが、これは更に Γ'* ® (T | x)(εyP" | y)P" すなわち Γ'* ® (εyP"* | y)P"* と書くことができます。
　仮定により、Ψ'* は定理ですから、これに ( ε 導入) を適用して得られる Φ'* も定理であることがわかります。

　メタ定理３とメタ定理４については、何の変更点もなく、用いた推論規則が ( ε 導入) の場合にもそのまま通用します。
　以上でメタ定理44は証明されました。

　さて、ε量化記号を導入すると、量化記号 $ はε量化記号によって定義することができます。具体的にいうと、直観主義論理から論理記号 $ 及び $ に関する推論規則を捨て、改めて $xP を (εxP | x)P で定義すると、( $ 導入) と ( $ 消去) は導出することができます。
　実際、( $ 導入) は ( ε 導入) そのものですし、( $ 消去) については、x が仮定 Γ と命題 Q に含まれない変数で、Γ ® $xP つまり Γ ® (εxP | x)P と Γ, P ® Q が定理なら、後者に推論規則 ( 代 入 ) を適用して x に εxP を代入すれば、仮定により Γ, (εxP | x)P ® Q が得られます。よって推論規則 ( 切 断 ) により Γ ® Q が得られます。以上で ( $ 消去) が導出できることがわかりました。
　このことから、$ と ε をどちらも持つ推論体系では、(εxP | x)P を $¢xP と書いて第２節のメタ定理５を適用すれば、

(4-4)  (εxP | x)P Û $xP

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

　ところで、εxP というのは一つの項です。ですから、ε量化記号の追加による理論拡大では新たな項が追加されたことになるわけですが、その結果として、命題の証明可能性に対しても影響が出てきます。
　例えば、P が変数 x を含まないとき、前節メタ定理40 (c) の命題：

(4-5)  $x($xR Þ R)

が証明できます。
　実際、(4-4) により、$xR Þ (εxR | x)R が成り立ちますが、$xR は x を含まないため、この命題は (εxR | x)($xR Þ R) とも書け、従って ( $ 導入) により (4-5) が得られます。
　このように、ε量化記号を導入することによって、直観主義論理のもとでは証明できなかった命題が証明可能になることがあることがわかりました。
　なぜこういうことが生じたかというと、ε量化記号導入前の理論では、命題 $xR Þ (T | x)R が成り立つような項 T は存在しなかったのに、ε量化記号を追加したとたんに、εxR という新たな項がこの命題を成り立たせる項 T になってしまったことが原因です。

　さて、ε量化記号は、それが単に新たな項を作る能力を持つというだけでなく、ひとたび形式化して理論内部の記号になってしまうと、形式化する前とは違って、(T | x)R を満たす項 T がまだ見つかっていなくても εxR という項を使うことが許されてしまいます。
　そのような場合の εxR という項は、いわば“何も表していない項”と解釈すべきものですから、一般に理論にε量化記号を追加する場合は、それに先立って、当該理論を、“何も表わしていない項”という概念を許すような理論体系に修正する必要があります。
　このことを、具体例によって説明してみましょう。

　今、ε量化記号を導入しようとしている理論が、次の性質：

(4-6)  "x ( (Ø x º a) Ú (Ø x º b) )

を満たす項 a , b を持つとします。このとき、特に x に a を代入することにより

(4-7)  Ø a º b

が成り立ちます（ちなみに、等号に対して排中律が成り立つような理論では、逆に (4-7) から (4-6) が得られます）。

　さて、この理論にε量化記号を追加し、それだけで何も手当てをしないとどういうことになるかを考察してみましょう。
　任意に２つの命題 P と Q を選び、これらに現れない自由変数 x を選んで、命題 R を次のように定義します：

(4-8)  R :º (x º a Ù P) Ú (x º b Ù Q)

　さて、ε量化記号の追加により (4-5) が成り立つので、( $ 消去) を用いるため

(4-9)  $xR Þ R

を仮定します。
　このとき、(4-8) より明らかに

(4-10a)  (R Ù Ø x º a) Þ Q

(4-10b)  (R Ù Ø x º b) Þ P

が成り立ち、また (4-7),(4-8) により

(4-11a)  (a | x)R Û P

(4-11b)  (b | x)R Û Q

が成り立ち、また (4-6) から ( " 消去) により

(4-12)  (Ø x º a) Ú (Ø x º b)

が得られます。
　ここで Ø x º a の場合は、P を仮定すると、(4-11a) により (a | x)R が得られ、従って ( $ 導入) により $xR が得られ、従って (4-9) と (4-10a) により Q が得られるので、この場合は P Þ Q が成り立ちます。
　また Ø x º b の場合は、Q を仮定すると、(4-11b) により (b | x)R が得られ、従って ( $ 導入) により $xR が得られ、従って (4-9) と (4-10b) により P が得られるので、この場合は Q Þ P が成り立ちます。
　ゆえに ( Ú 導入) と ( Ú 消去) と ( $ 消去) により

(4-13)  (P Þ Q) Ú (Q Þ P)

が成り立つことがわかりました。これは、前節で直観主義論理のもとでは証明できないと述べたメタ定理39 (i) に他なりません。
　しかも、この (4-13) で Q に ØP を代入すると、P Þ ØP が ØP と同値、(ØP) Þ P が ØØP と同値であることに注意すれば、否定命題の形に書けるような命題 ØP に関する排中律：

(4-14)  ØP Ú ØØP

が証明できてしまうことがわかりますが、これは

(4-15)  Ø(P Ù Q) Û ( (ØP) Ú (ØQ) )

が一般に証明できることと同値です。
　実際、(4-15) が成り立てば、Q に ØP を代入すると、左辺は自明に成り立つので、その右辺である (4-14) も成り立ちます。
　逆に (4-14) が成り立てば、メタ定理28により、(4-15) の左辺から P Þ ØQ が得られ、従って対偶を２回取ってメタ定理20を用いれば ØØP Þ ØQ が得られるので、(4-14) により (4-15) の右辺が得られます。また (4-15) の右辺から左辺はメタ定理30 (d) により常に成り立つので、これで (4-14) から (4-15) が得られることも証明されました。
　ちなみに (4-15) が一般に成り立つような理論では、(4-15) を P が x º a 、Q が x º b である場合に適用し、全体を "x で縛ることにより、(4-6) は "x Ø(x º a Ù x º b) すなわち Ø$x(x º a Ù x º b) すなわち (4-7) と同値になってしまいます。

　さて、上記の証明では (4-5) を用いましたが、(4-5) を使う代わりに、(4-9) 以下の議論において、変数 x の所を εxR に書き換えても証明はそのまま成立します。
　このように証明を書き換えてみればわかるように、命題 $xR 自体が証明されているわけではないので、εxR というのは“何も表わしていない項”であるはずですが、そのような項に対して (4-6) に ( " 消去) を適用して (4-12) を導いていることがわかります。
　しかし、そもそも最初に当該理論を定式化した際には、“何も表わしていない項”などというものが存在することは想定しておらず、(4-6) のような公理は、当然“何かを表わしている項”に対して成立する性質として規定されていたはずです。
　ですから、そのような公理を“何も表わしていない項”に適用するのは、その理論の趣旨から考えて“正しい推論”ではなく、そのような推論によって得られた結論 (4-13)~(4-15) も“根拠がない”ことになります。

　従って、ε量化記号を用いるのであれば、理論を構築する際に、“項というのは、それが必ずしも何かを表わしているとは限らない”ということを前提にして公理や推論規則を与えておく必要があるのです。
　具体的には、ある“対象物”に関する理論を構築するにあたり、「項 T が考察しようとしている対象物を表している」ということを t(T ) と略記することにして、この概念を形式化します。
　すなわち、理論を構築する際に、１変項述語記号 t を追加してこれを存在述語記号（existence predicate）とよび、当該理論の対象物について成り立つ性質を公理や推論規則として与える場合は、必ず“t(T ) が成り立つ項 T について〜が成り立つ”という形で与えることにします。
　その際、t(T ) を満たす項のことを t 項とよぶことにし、t という存在述語記号が当該理論を特徴付けていることことから、当該理論のことも理論 t とよぶことにします。

　さて、この作業を組織的に行うために、

(4-16a)  "t xP  :º  "x (t(x) Þ P)

(4-16b)  $t xP  :º  $x (t(x) Ù P)

(4-16c)  εt xP  :º  εx (t(x) Ù P)

と定義し、これらの省略記号 "_t , $_t , ε_t を（１変項述語記号 t に伴う）限定量化記号といいます。これらの記号は次の推論規則を満たします：

( "t 導入)	t(x)├ P ————– "t xP	( x¢As )
( "t 消去)	"t xP t(T ) ————– (T | x)P
( $t 導入)	(T | x)P t(T ) ————– $t xP
( $t 消去)	$t xP t(x), P├ Q —————– Q	( x¢As, Q )
( εt 導入)	(T | x)P t(T ) —————– (εt xP | x)P	(T | x)P t(T ) ————— t(εt xP)

　実際、( "_t 導入) の上段が成り立てば、( Þ 導入) により t(x) Þ P が得られ、( " 導入) により下段が得られます。
　また ( "_t 消去) の上段が成り立てば、( " 消去) により t(T ) Þ (T | x)P が得られ、( Þ 消去) により下段が得られます。
　また ( $_t 導入) の上段が成り立てば、( Ù 導入) により t(T ) Ù (T | x)P が得られ、( $ 導入) により下段が得られます。
　また ( $_t 消去) の上段が成り立てば、( 増 ) と ( 仮 定 ) と ( Ù 消去) により t(x), t(x) Ù P├ P が得られますが、上段第２式に ( 増 ) を適用すれば t(x), t(x) Ù P, P├ Q が得られるので、これらに ( 切 断 ) を適用すれば t(x), t(x) Ù P├ Q が得られます。
　一方、上段第２式に ( 仮 定 ) と ( Ù 消去) を適用すれば t(x) Ù P├ t(x) が得られるので、( 切 断 ) により t(x) Ù P├ Q が得られます。ゆえにここで ( $ 消去) を用いれば下段が得られます。
　最後に ( ε_t 導入) の上段が成り立てば、( Ù 導入) により t(T ) Ù (T | x)P すなわち (T | x){t(x) Ù P} が得られ、( ε 導入) により (ε_t xP | x){t(x) Ù P} すなわち t(ε_t xP) Ù (ε_t xP | x)P が得られます。ゆえに ( Ù 消去) により両図式の下段が得られます。

　さて、これらの推論規則は、順にそれぞれ次の性質を形式化したものになっています：

(4-17a)	命題 P が当該理論の対象物を表す自由変数 x に対して成り立てば、"t xP が成り立つ。
(4-17b)	"t xP が成り立てば、当該理論の対象物 T に対して (T | x)P が成り立つ。
(4-17c)	ある当該理論の対象物 T に対して (T | x)P が成り立てば、$t xP が成り立つ。
(4-17d)	$t xP が成り立ち、当該理論の対象物を表わす自由変数 x に対して P を仮定に追加すると x を含まない命題 Q が得られるならば、Q が成り立つ。
(4-17e)	命題 P と当該理論の対象物 T に対して (T | x)P が成り立てば、εt xP は当該理論の対象物で、(εt xP | x)P が成り立つ。

　すなわち、限定量化記号は、対応する（本来の）量化記号を“当該理論の対象物”に“限定”する役割を果たしていることがわかります。

　さて、当該理論が（定項を含む）関数記号として f₁ ,¼, f_n （ただし各 f_i の引数の個数を k とする）を持ち、当該理論の対象物を代入するとやはり当該理論の対象物になるということを保証したければ、それは、n 個の推論規則：

(4-18)i

t(T1 ) ¼ t(Tk ) ——————— t( fi(T1 ,¼, Tk ))

を与えることにより実現できます。また、当該理論の対象物が満たすべき性質を公理として与えようとしているならば、量化記号を用いるところはすべて存在述語記号に伴う限定量化記号を用いて表現する必要があります。

　例えば、先述の例のような、当該理論の対象物がすべて当該理論の対象物である a か b のいずれかと異なる、ということを保証したいのであれば、与えるべき公理は (4-6) ではなく、まず t(a) と t(b) という２つの公理を与えた上で、

(4-19)  "t x ( (Ø x º a) Ú (Ø x º b) )

という形の公理を与える必要があります。
　この形で理論を定式化しておくと、(4-13)~(4-15) を導く証明において、(4-6) ではなく、(4-19) に ( "_t 消去) を適用して (4-12) を得なければなりませんが、今度は t(x) が証明されていないため、( "_t 消去) を適用することができません。
　この結果、(4-12) から先の議論が展開できず、(4-13)~(4-15) の結果は得られなくなります。

　以上のような説明に対し、(4-5) のかわりに、そこに現れる量化記号をすべて限定量化記号に置き換えて得られる命題：

(4-20)  $t x($t xR Þ R)

を証明しておいて、(4-5) を使うかわりに (4-20) を用いればよいではないか、と思われるかもしれません。
　つまり、(4-20) を用いれば、( $ 消去) を用いるために (4-9) を仮定する代わりに、( $_t 消去) を用いるために t(x) と $_t xR Þ R を仮定することが許され、以後の議論が正当化されるのではないか、というわけです。
　ところが、この (4-20) の成立自体が実は保証されないのです。
　実際、$_t xR を仮定し、( $_t 消去) を用いるために t(x) と R を仮定すると、( ε_t 導入) により (ε_t xR | x)R が成り立ちます。したがって ( Þ 導入) により $_t xR Þ (ε_t xR | x)R つまり (ε_t xR | x)($_t xR Þ R) までは証明できます。
　ところが t(ε_t xR) が一般に証明できないため、そこから $_t x($_t xR Þ R) を導くことができません。

　以上見てきたように、存在述語記号 t を導入し、それに伴う限定量化記号によって当該理論を定式化しておけば、ε量化記号を導入する前には (4-5), (4-13)~(4-15) の各命題が直観主義論理では証明できなかった状況が正しく維持できていることがわかります。

　次に、s , t を共に１変項述語記号とするとき、それらに伴う限定量化記号に対しても、メタ定理35〜40と類似のメタ定理が成り立つことを確かめておきましょう。

メタ定理45	(a)　$x t(x) が成り立てば、"t xP Þ $t xP は定理である。
	(b)　$s x$t yP と $t y$s xP は同値。
	(c)　"s x"t yP と "t y"s xP は同値。
	(d)　$s x"t yP Þ "t y$s xP は定理。
	(e)　($t xP) Ú ($t xQ) と $t x(P Ú Q) は同値。
	(f)　("t xP) Ù ("t xQ) と "t x(P Ù Q) は同値。

(a)　$x t(x) を仮定し、( $ 消去) を用いるために t(x) を仮定する。"_t xP すなわち "x(t(x) Þ P) を仮定すると、( " 消去) と ( Þ 消去) により P が得られ、( Ù 導入) と ( $ 導入) により $x(t(x) Ù P) すなわち $_t xP が得られるので、( Þ 導入) により明らか。

(b)　x と y は異なる変数と仮定してよい（以下でも同様）。メタ定理36 (c) により、$x(s(x) Ù $y(t(y) Ù P)) は $x$y(s(x) Ù (t(y) Ù P)) と同値。これはメタ定理35 (b) 、23 (a) 、22 (a) により $y$x(t(y) Ù (s(x) Ù P)) と同値。これは再度メタ定理36 (c) により、$y(t(y) Ù $x(s(x) Ù P)) と同値。

(c)　メタ定理36 (a) により、"x(s(x) Þ "y(t(y) Þ P)) は "x"y(s(x) Þ (t(y) Þ P)) と同値。これはメタ定理35 (c) 、26により "y"x(t(y) Þ (s(x) Þ P)) と同値。これは再度メタ定理36 (a) により、"y(t(y) Þ "x(s(x) Þ P)) と同値。

(d)　メタ定理36 (e) により、$x(s(x) Ù "y(t(y) Þ P)) は $x"y(s(x) Ù (t(y) Þ P)) と同値。これからメタ定理35 (d) により "y$x(s(x) Ù (t(y) Þ P)) が得られる。 一方、明らかに $x(s(x) Ù (t(y) Þ P)) から t(y) Þ $x(s(x) Ù P) が導ける（s(x) と t(y) Þ P を満たす x を取ると、t(y) を仮定すれば P が得られるので $x(s(x) Ù P) が得られる）ので、"y(t(y) Þ $x(s(x) Ù P)) が得られる。

(e)　メタ定理35 (e) により、$x(t(x) Ù P) Ú $x(t(x) Ù Q) は $x((t(x) Ù P) Ú (t(x) Ù Q)) と同値。これはメタ定理24 (b) により $x(t(x) Ù (P Ú Q)) と同値。

(f)　メタ定理35 (f) により、"x(t(x) Þ P) Ù "x(t(x) Þ Q) は "x((t(x) Þ P) Ù (t(x) Þ Q)) と同値。これはメタ定理30 (a) により "x(t(x) Þ (P Ù Q)) と同値。

メタ定理46	x を Q に現れない自由変数とする。このとき
	(a)　Q Þ ("t xP) と "t x(Q Þ P) は同値。
	(b)　($t xP) Þ Q と "t x(P Þ Q) は同値。
	(c)　($t xP) Ù Q と $t x(P Ù Q) は同値。
	(d)　$t x(P Ú Q) Þ ($t xP) Ú Q が成り立つ。更に $x t(x) が成り立てば、逆 ($t xP) Ú Q Þ $t x(P Ú Q) も成り立つ。
	(e)　("t xP) Ù Q Þ "t x(P Ù Q) が成り立つ。更に $x t(x) が成り立てば、逆 "t x(P Ù Q) Þ ("t xP) Ù Q も成り立つ。
	(f)　("t xP) Ú Q Þ "t x(P Ú Q) が成り立つ。更に Q に対して排中律が成り立てば、逆 "t x(P Ú Q) Þ ("t xP) Ú Q も成り立つ。
	(g)　"t x(ØP) と Ø$t xP は同値。
	(h)　$t x(ØP) Þ Ø"t xP が成り立つ。
	(i)　"t xP Þ Ø$t x(ØP) が成り立つ。
	(j)　$t xP Þ Ø"t x(ØP) が成り立つ。
	(k)　"t x(ØØP) と Ø$t x(ØP) は同値。従って特に、ØØP が P と同値なら "t xP と Ø$t x(ØP) は同値。

(a)　メタ定理36 (a) により Q Þ ("x(t(x) Þ P)) は "x(Q Þ (t(x) Þ P)) と同値で、これはメタ定理27により "x(t(x) Þ (Q Þ P)) と同値。

(b)　メタ定理36 (b) により ($x(t(x) Ù P)) Þ Q は "x((t(x) Ù P) Þ Q) と同値で、これはメタ定理27により "x(t(x) Þ (P Þ Q)) と同値。

(c)　メタ定理36 (c) により ($x(t(x) Ù P)) Ù Q は $x((t(x) Ù P) Ù Q) と同値で、これはメタ定理23 (a) により $x(t(x) Ù (P Ù Q)) と同値。

(d)　メタ定理22と24 (b) により $x(t(x) Ù (P Ú Q)) は $x((t(x) Ù P) Ú (t(x) Ù Q)) と同値で、そこから $x((t(x) Ù P) Ú Q) が導かれるが、これはメタ定理36 (d) により ($x(t(x) Ù P)) Ú Q と同値。
　更に $x t(x) が成り立つときは、$x((t(x) Ù P) Ú Q) から $x((t(x) Ù P) Ú (t(x) Ù Q)) が言えるので、逆も成り立つ。

(e)　メタ定理36 (e) により ("x(t(x) Þ P)) Ù Q は "x((t(x) Þ P) Ù Q) と同値で、メタ定理９によりそこから "x((t(x) Þ P) Ù (t(x) Þ Q)) が導かれ、これはメタ定理30 (a) により "x(t(x) Þ (P Ù Q)) と同値。
　一方、"x((t(x) Þ P) Ù (t(x) Þ Q)) から "x(t(x) Þ P) と "x(t(x) Þ Q) が導かれるが、$x t(x) が成り立つときは後者から Q が導かれるので逆も成り立つ。

(f)　メタ定理36 (f) により ("x(t(x) Þ P)) Ú Q から "x((t(x) Þ P) Ú Q) が導かれ、メタ定理30 (c) によりそこから "x(t(x) Þ (P Ú Q)) が得られる。
　一方、Q Ú ØQ が成り立てば、メタ定理30 (c) により "x(t(x) Þ (P Ú Q)) から "x((t(x) Þ P) Ú Q) が得られるが、メタ定理36 (f) によりこれから ("x(t(x) Þ P)) Ú Q が得られる。

(g)　(b) で Q を ^ とすればよい。

(h)　t(x) と仮定すると、( "_t 消去) と ( Þ 導入) により "_t xP Þ P が、従ってメタ定理17により (ØP) Þ (Ø"_t xP) が成り立つので、( "_t 導入) により "_t x((ØP) Þ (Ø"_t xP)) が成り立つ。すなわち (b) で P に ØP を、Q に Ø"_t xP を代入したときの右の命題が成り立つので、このときの (b) の左の命題により明らか。

(i)　"_t xP と仮定し、更に $_t x(ØP) と仮定すると、(h) と ( Þ 消去) により Ø"_t xP が得られて矛盾するので Ø$_t x(ØP) が得られ、従って ( Þ 導入) により明らか。

(j)　$_t xP と仮定し、更に "_t x(ØP) と仮定すると、(g) により Ø$_t xP が得られて矛盾するので Ø"_t x(ØP) が得られ、従って ( Þ 導入) により明らか。

(k)　(g) で P を ØP とすればよい。

メタ定理47*	古典論理では、
	(a)　Ø"t xP と $t x(ØP) は同値。
	(b)　$t xP と Ø"t x(ØP) は同値。
	(c)　$x t(x) が成り立てば、$t x($t xP Þ P) は定理である。

(a)　メタ定理46 (k) の否定を取ればよい。

(b)　(a) で P を ØP とすればよい。

(c)　これはメタ定理39 (f) により $_t x{(Ø$_t xP) Ú P} と同値であり、これはまたメタ定理46 (d) により (Ø$_t xP) Ú $_t xP と同値なので、排中律により成り立つ。

　さて、これらのメタ定理群の中で、メタ定理45 (a) 、メタ定理46 (d) , (e) 、メタ定理47* (c) だけは、対応するメタ定理35 (a) 、メタ定理36 (d) , (e) 、メタ定理40* (c) と比べると、“$x t(x) が成り立てば”という余計な前提条件が付いています。これはなぜでしょうか。

　例えばメタ定理45 (a) の命題 "_t xP Þ $_t xP を考えてみましょう。
　今、"_t xP を仮定します。ここでもし $x t(x) が成り立たないと、この理論には t 項が存在しないので、( "_t 消去) を用いたくても、(T | x)P を満たす t 項 T が存在しないので、これ以上先に進めません。
　ところがこれに対し、メタ定理35 (a) の命題 "xP Þ $xP の方は、"xP を仮定すると、この理論に t 項が存在していようがいまいが、変数 x という項が存在しているため、推論規則 ( " 消去) を使って、P の x に変数 x という項それ自身を代入することにより、命題 P が証明され、更にこの命題は P の x に変数 x という項それ自身を代入したものなので、( $ 消去) により $xP が得られてしまう、というわけです。

　すなわち、存在述語記号を導入することにより、当該理論で扱う対象物を表わす“実体を持った項”と、一般的な証明を可能にするための道具に過ぎない変数とか、(T | x)R が証明されていない場合の εxR という項のような“実体を持たない項”が明確に区別できるようになるのです。

　しかも、存在述語記号を導入したことによるメリットはこれだけではありません。
　次節以降で解説するように、“集合”や“写像”のような新しい種類の“対象物”を表わす項を理論に追加しようとするとき、当該理論本来の存在述語記号に加え、項がその“新しい種類の対象物”であることを意味する新たな存在述語記号を追加導入することによって、パラドクスを生じることなく当該理論にこれらの新概念を追加することが可能になります。