数学の基礎

　本文第１節や付録３では自然推論や (LJ), (LK) による論理の定式化を解説しましたが、これとは別の定式化もあります。
　というより、むしろ歴史的に見ると、自然推論や (LJ), (LK) による定式化は後発のもので、それ以前は別の定式化が行われていました。以下でそのような定式化の一つについて説明し、古典論理の自然推論との同等性を確かめることにします。

　最初に次の５種類の命題を考えます：

(A4-1a)	(P Ú P) Þ P
(A4-1b)	P Þ (P Ú Q)
(A4-1c)	(P Ú Q) Þ (Q Ú P)
(A4-1d)	(P Þ Q) Þ ((R Ú P) Þ (R Ú Q))
(A4-1e)	"xP Þ (T | x)P

　まず、これらの命題が自然推論によって導出可能であることを確かめましょう。
　実際、最初の (A4-1a) は、本文第３節メタ定理21により明らかです。
　また、次の (A4-1b) は、(Ú 導入) と (Þ 導入) により明らかです。
　また、次の (A4-1c) は、本文第３節メタ定理22により明らかです。
　また、次の (A4-1d) は次のように証明されます。

ア　P Þ Q , R Ú P├ R Ú P　　　　　　………　[ ( 仮 定 ) ] イ　P Þ Q , R Ú P , R├ R　　　　　　　………　[ ( 仮 定 ) ] ウ　P Þ Q , R Ú P , R├ R Ú Q　　　　………　[ イ に (Ú 導入) を適用 ] エ　P Þ Q , R Ú P , P├ P　　　　　　　………　[ ( 仮 定 ) ] オ　P Þ Q , R Ú P , P├ P Þ Q　　　　………　[ ( 仮 定 ) ] カ　P Þ Q , R Ú P , P├ Q　　　　　　　………　[ エ と オ に (Þ 消去) を適用 ] キ　P Þ Q , R Ú P , P├ R Ú Q　　　　………　[ カ に (Ú 導入) を適用 ] ク　P Þ Q , R Ú P├ R Ú Q　　　　　　………　[ ア と ウ と キ に (Ú 消去) を適用 ] ケ　P Þ Q├ (R Ú P) Þ (R Ú Q)　　　………　[ ク に (Þ 導入) を適用 ] コ　(P Þ Q) Þ ((R Ú P) Þ (R Ú Q))　………　[ ケ に (Þ 導入) を適用 ]

　また、最後の (A4-1e) は (" 消去) と (Þ 導入) から明らかです。

　一方、古典論理においては、次の推論規則：

(A4-2a)	P P Þ Q ———– Q
(A4-2b)	P Ú Q ————— ("xP) Ú Q	( x は公理にも Q にも現れない変数 )

は導出可能です。
　実際、(A4-2a) は (Þ 消去) そのものですし、(A4-2b) は、(" 導入) により上段から "x(P Ú Q) が得られるので、第３節メタ定理39 (k) により下段が得られます。

　ところで、古典論理では、論理記号のうちいくつかの論理記号は他の論理記号によって定義可能であることに注意します。
　実際、古典論理では排中律を仮定しますから、本文第３節のメタ定理39の (f) と (c) 及びメタ定理40の (b) により、P Þ Q は (Ø P) Ú Q と同値であり、P Ù Q は Ø ((Ø P) Ú (Ø Q)) と同値であり、$xP は Ø"x(Ø P) と同値であることがわかります。
　更に、本文第２節のメタ定理５によると、命題同士を論理記号で合成して作った命題の構成要素となっている命題を、同値な命題に置き換えて得られる命題は、もとの命題と同値になります。
　そこで、論理記号のうち、Ø と Ú と " のみを本来の論理記号とみなし、他の論理記号 Þ , Ù , $ については、P Þ Q を (Ø P) Ú Q の省略記号とみなし、P Ù Q を Ø ((Ø P) Ú (Ø Q)) の省略記号とみなし、$xP を Ø"x(Ø P) の省略記号とみなすことにします。

　このとき、上記の (A4-1) と (A4-2) を推論規則に持つ推論体系を考えると、この推論体系のもとでは、古典論理の自然推論の推論規則がすべて導出できることを証明しましょう。
　実際、この推論体系のもとで、次のメタ定理が成り立つことをまず証明します：

(A4-3a)	P Þ Q と Q Þ R が証明可能なら P Þ R も証明可能。
(A4-3b)	Q Þ (P Ú Q) は証明可能。
(A4-3c)	P Þ R と Q Þ R が証明可能なら (P Ú Q) Þ R は証明可能。
(A4-3d)	P Þ P すなわち (Ø P) Ú P は証明可能。
(A4-3e)	P Ú (Ø P) は証明可能。
(A4-3f)	P Þ (ØØ P) は証明可能。
(A4-3g)	(ØØ P) Þ P は証明可能。
(A4-3h)	P Þ Q が証明可能なら (Ø Q) Þ (Ø P) も証明可能。
(A4-3i)	P Þ Q と P Þ Ø Q が証明可能なら Ø P は証明可能。
(A4-3j)	((P Ú Q) Ú R) Þ (P Ú (Q Ú R)) は証明可能。
(A4-3k)	P と Q が証明可能なら P Ù Q は証明可能。
(A4-3l)	(P Ù Q) Þ P は証明可能。
(A4-3m)	(P Ù Q) Þ Q は証明可能。
(A4-3n)	x が公理に現れない変数で、P が証明可能なら、"xP は証明可能。
(A4-3o)	(T | x)P Þ $xP は証明可能。
(A4-3p)	x が公理にも Q にも現れない変数で、P Þ Q が証明可能なら、$xP Þ Q は証明可能。
(A4-3q)	P Ú (Q Ú R) が証明可能なら Q Ú (P Ú R) は証明可能。
(A4-3r)	P が証明可能なら、R Þ P は証明可能。
(A4-3s)	R Þ P と R Þ (P Þ Q) が証明可能なら、R Þ Q は証明可能。
(A4-3t)	x が公理にも Q にも R にも現れない変数で、R Þ (P Ú Q) が証明可能なら、R Þ ("xP Ú Q) は証明可能。

　実際、まず (A4-3a) は、

… ア　P Þ Q 　… イ　Q Þ R 　… ウ　(Q Þ R) Þ ((P Þ Q) Þ (P Þ R))　………　[ (A4-1d) で P , Q , R にそれぞれ Q , R , Ø P を代入 ] エ　(P Þ Q) Þ (P Þ R)　　　　　　　　　………　[ イ と ウ に推論規則 (A4-2a) を適用 ] オ　P Þ R　　　　　　　　　　　　　　　　　………　[ ア と エ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3b) は

ア　Q Þ (Q Ú P)　　　　　　　　　………　[ (A4-1b) で、P , Q にそれぞれ Q , P を代入 ] イ　(Q Ú P) Þ (P Ú Q)　　　　　　………　[ (A4-1c) で、P , Q にそれぞれ Q , P を代入 ] ウ　Q Þ (P Ú Q)　　　　　　　　　………　[ ア と イ に (A4-3a) を適用 ]

という手順で証明されます。
　また (A4-3c) は

… ア　P Þ R 　… イ　Q Þ R 　… ウ　(Q Þ R) Þ ((P Ú Q) Þ (P Ú R))　………　[ (A4-1d) で P, Q, R にそれぞれ Q, R, P を代入 ] エ　(P Ú Q) Þ (P Ú R)　　　　　　　　　………　[ イ と ウ に推論規則 (A4-2a) を適用 ] オ　(P Ú R) Þ (R Ú P)　　　　　　　　　………　[ (A4-1c) で P , Q にそれぞれ P , R を代入 ] カ　(P Ú Q) Þ (R Ú P)　　　　　　　　　………　[ エ と オ に (A4-3a) を適用 ] キ　(P Þ R) Þ ((R Ú P) Þ (R Ú R))　………　[ (A4-1d) で P , Q , R にそれぞれ P , R , R を代入 ] ク　(R Ú P) Þ (R Ú R)　　　　　　　　　………　[ ア と キ に推論規則 (A4-2a) を適用 ] ケ　(P Ú Q) Þ (R Ú R)　　　　　　　　　………　[ カ と ク に (A4-3a) を適用 ] コ　(R Ú R) Þ R　　　　　　　　　　　　………　[ (A4-1a) で P に R を代入 ] サ　(P Ú Q) Þ R　　　　　　　　　　　　………　[ ケ と コ に (A4-3a) を適用 ]

という手順で証明されます。
　また (A4-3d) は

ア　P Þ (P Ú P)　　　………　[ (A4-1b) で P と Q に P を代入 ] イ　(P Ú P) Þ P　　　………　[ (A4-1a) ] ウ　P Þ P　　　　　　………　[ ア と イ に (A4-3a) を適用 ]

という手順で証明されます。
　また (A4-3e) は

ア　(Ø P) Ú P　　　　　　　　　　　　………　[ (A4-3d) ] イ　((Ø P) Ú P) Þ (P Ú (Ø P))　　………　[ (A4-1c) で P , Q にぞれぞれ Ø P と P を代入 ] ウ　P Ú (Ø P)　　　　　　　　　　　　………　[ ア と イ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3f) は、(A4-3e) の P に Ø P を代入したものに他なりません。
　また (A4-3g) は

ア　(Ø P) Þ (ØØØ P)　　　　　　　　　　　　　………　[ (A4-3f) で P に Ø P を代入 ] イ　((Ø P) Þ (ØØØ P)) Þ ((P Ú (Ø P)) Þ (P Ú (ØØØ P)))　………　[ (A4-1d) で P , Q , R にそれぞれ Ø P , ØØØ P , P を代入 ] ウ　(P Ú (Ø P)) Þ (P Ú (ØØØ P))　　　　　　………　[ ア と イ に推論規則 (A4-2a) を適用 ] エ　P Ú (Ø P)　　　　　　　　　　　　　　　　　　………　[ (A4-3e) ] オ　P Ú (ØØØ P)　　　　　　　　　　　　　　　　………　[ エ と ウ に推論規則 (A4-2a) を適用 ] カ　(P Ú (ØØØ P)) Þ ((ØØØ P) Ú P)　　　　………　[ (A4-1c) で P, Q にそれぞれ P , ØØØ P を代入 ] キ　(ØØ P) Þ P　　　　　　　　　　　　　　　　………　[ オ と カ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3h) は

… ア　P Þ Q 　… イ　Q Þ (ØØ Q)　　　　　　　　　　　　　　　　　………　[ (A4-3f) の P に Q を代入 ] ウ　(Ø P) Ú (ØØ Q)　　　　　　　　　　　　　　　………　[ ア と イ に (A4-3a) を適用 ] エ　((Ø P) Ú (ØØ Q)) Þ ((ØØ Q) Ú (Ø P))　　………　[ (A4-1c) で P , Q にそれぞれ Ø P , ØØ Q を代入 ] オ　(Ø Q) Þ (Ø P)　　　　　　　　　　　　　　　　………　[ ウ と エ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3i) は、

… ア　P Þ Q 　… イ　P Þ Ø Q 　… ウ　(ØØ Q) Þ (Ø P)　　　　　　　　………　[ イ に (A4-3h) を適用 ] エ　(Ø Q) Þ (Ø P)　　　　　　　　　………　[ ア に (A4-3h) を適用 ] オ　((ØØ Q) Ú (Ø Q)) Þ (Ø P)　　………　[ ウ と エ に (A4-3c) を適用 ] カ　(ØØ Q) Ú (Ø Q)　　　　　　　　………　[ Ø Q に (A4-3d) を適用 ] キ　Ø P　　　　　　　　　　　　　　　………　[ カ と オ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3j) は

ア　P Þ (P Ú (Q Ú R))　　　　　　　　　　………　[ (A4-1b) で Q に Q Ú R を代入 ] イ　Q Þ (Q Ú R)　　　　　　　　　　　　　………　[ (A4-1b) で P , Q にそれぞれ Q , R を代入 ] ウ　(Q Ú R) Þ (P Ú (Q Ú R))　　　　　　………　[ (A4-3b) で Q に Q Ú R を代入 ] エ　Q Þ (P Ú (Q Ú R))　　　　　　　　　　………　[ イ と ウ に (A4-3a) を適用 ] オ　(P Ú Q) Þ (P Ú (Q Ú R))　　　　　　………　[ ア と エ に (A4-3c) を適用 ] カ　R Þ (Q Ú R)　　　　　　　　　　　　　………　[ (A4-3b) で P , Q にそれぞれ Q , R を代入 ] キ　R Þ (P Ú (Q Ú R))　　　　　　　　　　………　[ カ と ウ に (A4-3a) を適用 ] ク　((P Ú Q) Ú R) Þ (P Ú (Q Ú R))　　　………　[ オ と キ に (A4-3c) を適用 ]

という手順で証明されます。
　また (A4-3k) は

… ア　P 　… イ　Q 　… ウ　((Ø P) Ú (Ø Q)) Ú (P Ù Q)　　　　　　………　[ (A4-3e) で P に (Ø P) Ú (Ø Q) を代入 ] エ　(((Ø P) Ú (Ø Q)) Ú (P Ù Q)) Þ ((Ø P) Ú ((Ø Q) Ú (P Ù Q)))　……　[ (A4-3j) で P , Q , R にそれぞれ Ø P , Ø Q , P Ù Q を代入 ] オ　P Þ (Q Þ (P Ù Q))　　　　　　　　　………　[ ウ と エ に推論規則 (A4-2a) を適用 ] カ　Q Þ (P Ù Q)　　　　　　　　　　　　　………　[ ア と オ に推論規則 (A4-2a) を適用 ] キ　P Ù Q　　　　　　　　　　　　　　　　　………　[ イ と カ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3l) は

ア　(Ø P) Þ ((Ø P) Ú (Ø Q))　　………　[ (A4-1b) で P , Q にそれぞれ Ø P , Ø Q を代入 ] イ　(P Ù Q) Þ (ØØ P)　　　　　　………　[ ア に (A4-3h) を適用 ] ウ　(ØØ P) Þ P　　　　　　　　　………　[ (A4-3g) ] エ　(P Ù Q) Þ P　　　　　　　　　………　[ イ と ウ に (A4-3a) を適用 ]

という手順で証明されます。
　また (A4-3m) は

ア　(Ø Q) Þ ((Ø P) Ú (Ø Q))　　………　[ (A4-3b) で P , Q にそれぞれ Ø P , Ø Q を代入 ] イ　(P Ù Q) Þ (ØØ Q)　　　　　　………　[ ア に (A4-3h) を適用 ] ウ　(ØØ Q) Þ Q　　　　　　　　　………　[ (A4-3g) で P に Q を代入 ] エ　(P Ù Q) Þ Q　　　　　　　　　………　[ イ と ウ に (A4-3a) を適用 ]

という手順で証明されます。
　また (A4-3n) は

… ア　P 　… イ　P Þ (P Ú "xP)　　　　　　………　[ (A4-1b) で Q に "xP を代入 ] ウ　P Ú "xP　　　　　　　　　　………　[ ア と イ に推論規則 (A4-2a) を適用 ] エ　"xP Ú "xP　　　　　　　　………　[ ウ に推論規則 (A4-2a) を適用 ] オ　("xP Ú "xP) Þ "xP　　………　[ (A4-1a) で P に "xP を代入 ] カ　"xP　　　　　　　　　　　　………　[ エ と オ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3o) は

ア　"x(Ø P) Þ (T | x)(Ø P)　　　………　[ (A4-1e) で P に Ø P を代入 ] イ　(ØØ (T | x)P) Þ $xP　　　　　………　[ ア に (A4-3h) を適用 ] ウ　(T | x)P Þ (ØØ (T | x)P)　　　………　[ (A4-3f) で P に (T | x)P を代入 ] エ　(T | x)P Þ $xP　　　　　　　　………　[ ウ と イ に (A4-3a) を適用 ]

という手順で証明されます。
　また (A4-3p) は

… ア　P Þ Q 　… イ　("x(Ø P)) Ú Q　　　　　　　　　　　　　………　[ 推論規則 (A4-2b) を、P に Ø P を代入して ア に適用 ] ウ　("x(Ø P)) Þ (Ø$xP)　　　　　　　　　………　[ (A4-3f) で P に "x(Ø P) を代入 ] エ　(Ø$xP) Þ ((Ø$xP) Ú Q)　　　　　　　………　[ (A4-1b) で P に Ø$xP を代入 ] オ　("x(Ø P)) Þ ((Ø$xP) Ú Q)　　　　　………　[ ウ と エ に (A4-3a) を適用 ] カ　Q Þ ((Ø$xP) Ú Q)　　　　　　　　　　………　[ (A4-3b) で P に Ø$xP を代入 ] キ　(("x(Ø P)) Ú Q) Þ ((Ø$xP) Ú Q)　　………　[ オ と カ に (A4-3c) を適用 ] ク　$xP Þ Q　　　　　　　　　　　　　　　　………　[ イ と キ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3q) は

… ア　P Ú (Q Ú R) 　… イ　P Þ (P Ú R)　　　　　　　　　　　　　………　[ (A4-1b) で Q に R を代入 ] ウ　(P Ú R) Þ (Q Ú (P Ú R))　　　　　　………　[ (A4-3b) で P , Q にそれぞれ Q , P Ú R を代入 ] エ　P Þ (Q Ú (P Ú R))　　　　　　　　　………　[ イ と ウ に (A4-3a) を適用 ] オ　Q Þ (Q Ú (P Ú R))　　　　　　　　　………　[ (A4-1b) で P , Q にそれぞれ Q , P Ú R を代入 ] カ　R Þ (P Ú R)　　　　　　　　　　　　　………　[ (A4-3b) で Q に R を代入 ] キ　R Þ (Q Ú (P Ú R))　　　　　　　　　………　[ カ と ウ に (A4-3a) を適用 ] ク　(Q Ú R) Þ (Q Ú (P Ú R))　　　　　　………　[ オ と キ に (A4-3c) を適用 ] ケ　(P Ú (Q Ú R)) Þ (Q Ú (P Ú R))　　………　[ エ と ク に (A4-3c) を適用 ] コ　Q Ú (P Ú R)　　　　　　　　　　　　　………　[ ア と ケ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3r) は

… ア　P 　… イ　P Þ (R Þ P)　　　………　[ (A4-3b) で P , Q にそれぞれ Ø R , P を代入 ] ウ　R Þ P　　　　　　　………　[ ア と イ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　また (A4-3s) は

… ア　R Þ P 　… イ　R Þ (P Þ Q) 　… ウ　P Þ (R Þ Q)　　　　　　　　　………　[ (A4-3q) で P , Q , R にそれぞれ Ø R , Ø P , Q を代入したものを イ に適用 ] エ　R Þ (R Þ Q)　　　　　　　　　………　[ ア と ウ に (A4-3a) を適用 ] オ　(Ø R) Þ (R Þ Q)　　　　　　　………　[ (A4-1b) で P に Ø R を代入 ] カ　(R Ú (Ø R)) Þ (R Þ Q)　　　　………　[ エ と オ に (A4-3c) を適用 ] キ　R Ú (Ø R)　　　　　　　　　　　　………　[ (A4-3e) で P に R を代入 ] ク　R Þ Q　　　　　　　　　　　　　　………　[ キ と カ に推論規則 (A4-2a) を適用 ]

という手順で証明されます。
　最後に (A4-3t) は

… ア　R Þ (P Ú Q) 　… イ　P Ú ((Ø R) Ú Q)　　　　………　[ (A4-3q) で P , Q , R にそれぞれ Ø R , P , Q を代入したものを ア に適用 ] ウ　"xP Ú ((Ø R) Ú Q)　　………　[ イ に推論規則 (A4-2b) を適用 ] エ　R Þ ("xP Ú Q)　　　　………　[ (A4-3q) で P , Q , R にそれぞれ "xP , Ø R , Q を代入したものを ウ に適用 ]

という手順で証明されます。
　以上で (A4-3) はすべて確かめられました。

　さて、この推論体系では、(Þ 導入) に相当する

(A4-4)

ある公理系 A に P を追加した理論で Q が証明可能なら、公理系 A のもとで P Þ Q は証明可能である。

というメタ定理が成り立ちます。これを演繹定理といいます。

　その証明ですが、P を公理系 A , P のもとでの Q の証明文とします。そこで、P を構成する各 R に対し、P Þ R が公理群 A のもとで証明可能であることを順次示していけば十分です。
　そこで、R より手前の命題についてはこのことが示せたものと仮定します。R は、それが公理である（すなわち公理系 A , P のうちのいずれかの命題である）か、(A4-1) の形の命題であるか、R より手前の命題から推論規則 (A4-2) のいずれかを適用して得られたかのいずれかです。

　まず R が A の中に現れる命題なら、それは公理系 A のもとで証明可能ですから、(A4-3r) により、公理系 A のもとで P Þ R は証明可能です。
　次に、R が P なら、P Þ R は P Þ P ですから、(A4-3d) により公理系 A のもとで証明可能です。
　以上により、R が公理系 A , P の公理である場合は確認できました。

　次に、R が (A4-1) のいずれかの形をしている場合を考えます。このとき、明らかに R は公理系 A のもとでも証明可能です。従って (A4-3r) により P Þ R は公理系 A のもとで証明可能です。

　次に、R が推論規則 (A4-2a) を適用して得られた命題である場合を考えます。この場合、P において、R より手前に A 及び A Þ B の形の命題が存在し、R は B です。
　このとき、仮定により、P Þ A と P Þ (A Þ B) は公理系 A において証明可能です。従って (A4-3s) により P Þ B すなわち P Þ R は、公理系 A のもとで証明可能です。

　最後に、R が推論規則 (A4-2b) を適用して得られた命題である場合を考えます。この場合、P において、R より手前に A Ú B の形の命題が存在し、公理系 A , P にも B にも現れない変数 x が存在して R は ("xA) Ú B です。
　このとき、仮定により、P Þ (A Ú B) は公理系 A において証明可能で、しかも変数 x は A にも P にも B にも現れません。従って (A4-3t) により P Þ ("xA Ú B) すなわち P Þ R は、公理系 A のもとで証明可能です。

　以上により、すべての場合に対して確かめられたので、特に R が Q の場合を考えることにより、(A4-4) は証明されました。

　さて、(A4-3k) は自然推論における (Ù 導入) そのものです。一方 (A4-3l),(A4-3m),(A4-2a) により、自然推論における (Ù 消去) が導出できます。
　また、(A4-1b),(A4-3b),(A4-2a) により、自然推論における (Ú 導入) が導出でき、(A4-3c),(A4-2a) と演繹定理により、自然推論における (Ú 消去) が導出できます。
　また、演繹定理 (A4-4) は自然推論における (Þ 導入) そのもので、推論規則 (A4-2a) は自然推論における (Þ 消去) そのものです。
　また、(A4-3i) と演繹定理により、自然推論における (Ø 導入) が導出でき、(A4-3g),(A4-2a) により、自然推論における (Ø 消去) が導出できます。
　また、(A4-3n) は自然推論における (" 導入) そのもので、(A4-1e),(A4-2a) により、自然推論における (" 消去) が導出できます。
　また、(A4-3o),(A4-2a) により、自然推論における ($ 導入) が導出でき、(A4-3p),(A4-2a) と演繹定理により、自然推論における ($ 消去) が導出できます。

　以上で、推論規則 (A4-1),(A4-2) を持つ推論体系が、自然推論による古典論理の推論体系と同等であることが証明されました。

　さて、上で紹介した推論体系は、“自然推論のように推論の途中で公理（仮定）を追加したり削除したりすることがない”という特徴がありますが、それもそのはずで、上記のようなGentzen以前の推論体系では、推論の途中で公理を変更するという発想がまだなかったのです。
　その代償として、上記の定式化では、推論規則が論理記号ごとに分かれているわけでもなく、またそれぞれの推論規則を仮定すべき形式上の必然性もよくわからないものになっています。

　さて、最初の話題はここまでとし、続いてι量化記号について解説することにしましょう。

　論理記号として Ù , Ú , Þ , ^ , " , $ しか持たない等号 = を持つ直観主義論理又は古典論理の推論体系では、R を満たす x が唯一つ存在する、すなわち $!xR が証明されても、その“唯一のもの”を表す項を作ることができません。
　そこで、第４節で解説したようなε量化記号のように理論を真に拡大することなく、一意存在が保証されたモノを表す項を導入する方法を考えてみましょう。

　今、$!xR という命題を仮定します。
　このとき、任意の命題 P に対して "x(R Þ P) と $x(R Ù P) という２つの命題は同値になります。
　なぜなら、前者を仮定すると、$xR ですから ($ 消去) を用いるために R を仮定すると、(" 消去) により R Þ P が、従って (Þ 消去) により P が、従って (Ù 導入) により R Ù P が、従って ($ 導入) により $x(R Ù P) が得られますが、これは x を含まないので ($ 消去) により後者の命題が得られます。
　逆に後者を仮定し、($ 消去) を用いるため R Ù P を仮定すると、(Ù 消去) により R と P が得られます。
　ここで、自由変数 z を取り、(z | x)R を仮定すると、$!xR による一意性条件により z = x が得られ、これと P に (= 消去) を用いれば (z | x)P が得られ、(Þ 導入) により (z | x)R Þ (z | x)P が得られ、(" 導入) により "z( (z | x)R Þ (z | x) )P すなわち "x(R Þ P) すなわち前者の命題が得られます。

　そこで、P を x を含む原子命題（すなわち一番左の記号が述語記号であるような命題）とするとき、同値な２つ命題 "x(R Þ P) と $x(R Ù P) のいずれか一方を (ιxR | x)P と略記することにします。ただし、ι は、省略記号として新規に導入した引数が命題の項型量化記号です。
　なお、x が P に現れない場合、本文第３節メタ定理36 (c) により $x(R Ù P) は ($xR) Ù P と同値で、これは更に、$xR が成り立つことから P とも同値であり、これはまた P が x を含まないことから (ιxR | x)P と書くことができます。
　すなわち P が原子命題ならば、x が P に現れていようがいまいが (ιxR | x)P は "x(R Þ P) とも $x(R Ù P) とも同値であることがわかります。そこで、この事実が一般に成り立つ、すなわち

(A4-5)

命題 $!xR を仮定すれば、任意の命題 P に対し、(ιxR | x)P は "x(R Þ P) とも $x(R Ù P) とも同値である。

ということを証明しましょう。

　まず P に現れる x 以外の変数がすべて R に現れない場合について証明すれば十分であることに注意します。
　実際、命題 P に現れる x 以外の変数全体を x₁ ,¼, x_k とし、P にも R にも現れず x と異なる k 個の変数 z₁ ,¼, z_k を用意し、(z₁ | x₁ )¼(z_k | x_k )P を P' と書くと、仮定により P' については (A4-5) が成り立つので、この結果の z_k に x_k を代入したもの、すなわち P に関する (A4-5) の同値性が、推論規則 ( 代 入 ) により導かれます。

　次に、命題 P に現れる x 以外の変数がすべて R に現れない場合を考え、C を P の構成手続きとします。ここで C において、C に登場し、命題 P に現れない x 以外の変数全体 x₁ ,¼, x_k を、C にも R にも現れず x とも異なる変数 z₁ ,¼, z_k に置き換えたものを C ' とすると、これは明らかに R とは x 以外に共通の変数を持たない P の構成手続きになっています。
　ゆえに、C の構成要素となる命題に現れる x 以外の変数は、R に現れず x とも異なると仮定して、C の構成要素である命題について (A4-5) が成り立つことを順に示していくことにしましょう。

　最初に C に現れる A と B について (A4-5) が成り立つと仮定します。
　このとき、本文第３節メタ定理30 (a) と メタ定理35 (f) により、"x(R Þ (A Ù B)) は ("x(R Þ A)) Ù ("x(R Þ B)) と同値であり、仮定によりこれは更に ( (ιxR | x)A ) Ù ( (ιxR | x)B ) すなわち (ιxR | x)(A Ù B) とも同値です。
　また、本文第３節メタ定理24 (b) と メタ定理35 (e) により、$x(R Ù (A Ú B)) は ($x(R Ù A)) Ú ($x(R Ù B)) と同値であり、仮定によりこれは更に ( (ιxR | x)A ) Ú ( (ιxR | x)B ) すなわち (ιxR | x)(A Ú B) とも同値です。
　また ($x(R Ù A)) Þ ("x(R Þ B)) から "x(R Þ (A Þ B)) が得られ、逆に "x(R Þ (A Þ B)) から ("x(R Þ A)) Þ ("x(R Þ B)) が得られることから "x(R Þ (A Þ B)) は ( (ιxR | x)A ) Þ ( (ιxR | x)B ) すなわち (ιxR | x)(A Þ B) と同値です。
　以上で、C に現れる A と B について (A4-5) が成り立てば、A Ù B , A Ú B , A Þ B についても (A4-5) が成り立つことがわかりました。
　なお、C に命題 ^ が現れる場合については、^ は０項述語記号ともみなせるので、原子命題の一種ですから明らかに成り立ちます。

　次に C に現れる A について (A4-5) が成り立つと仮定して、"zA と $zA に対しても (A4-5) が成り立つことを証明しましょう。
　まず z が x のときは、"zA あるいは $zA を B と書けば、B は x を含まないので (ιxR | x)B は B です。一方、本文第３節メタ定理36 (c) により $x(R Ù B) は ($xR) Ù B と同値で、これは更に、$xR が成り立つことから B とも同値ですから、この場合は B について (A4-5) は成り立ちます。
　次に、z が x でない場合を考えると、まず x が A に現れる場合は、仮定により z は R に現れません。また、z が A に現れない場合は、これを A にも R にも現れない別の変数に置き換えても "zA や $zA は変わらないので、結局 z は R に現れないと仮定することができます。
　ゆえに、本文第３節メタ定理36 (a) により "x(R Þ "zA) と "x"z(R Þ A) と "z"x(R Þ A) は同値であり、仮定によりこれは更に "z( (ιxR | x)A ) すなわち (ιxR | x)( "zA ) とも同値です。
　また、本文第３節メタ定理36 (c) により $x(R Ù $zA) と $x$z(R Ù A) と $z$x(R Ù A) は同値であり、仮定によりこれは更に $z( (ιxR | x)A ) すなわち (ιxR | x)( $zA ) とも同値です。

　以上で (A4-5) は証明されました。

　さて次に、命題 $!xR を仮定した場合、このι量化記号で作った項 ιxR を、省略記号ではなく、あたかも当該理論本来の項であるかのように扱った場合でも、構造に関する推論規則、論理記号や等号に関する推論規則を自由に使ってよい、すなわち

(A4-6)

命題 $!xR を仮定すれば、ιxR を省略記号ではない本来の項とみなして、もとの理論の推論規則を適用して得られる命題は、もとの理論においても証明可能である。

ということを証明しましょう。
　まず、推論規則のうち、一般の項に関する言及のない推論規則については明らかに成立しますから、一般の項に関する言及のある ( 代入 ) , (" 消去) , ($ 導入) , (= 消去) について確かめれば十分です。

　最初にsequent A ® P から (T | y)A ® (T | y)P が得られることを証明します。
　この場合、T の中に含まれる項 ιxR を、一斉に A にも P にも T にも R にも現れず x とも y とも異なる変数 z で置き換えた文字列を U とすると、これは ι を含まない本来の項ですから、推論規則 ( 代入 ) により (U | y)A ® (U | y)P は証明可能です。
　ここで仮定 A の構成要素を A_i とすると、仮定 (T | y)A のもとで、(T | y)A_i すなわち (ιxR | z)(U | y)A_i すなわち "z( (z | x)R Þ (U | y)A_i ) が成り立ちます。
　一方、仮定 $!xR により、($ 消去) を用いるため (z | x)R を仮定すると、(" 消去) と (Þ 消去) により、すべての i に対して (U | y)A_i が成り立ち、これは仮定 (U | y)A が成り立つことを意味するので、(U | y)P が得られ、($ 導入) により $z( (z | x)R Ù (U | y)P ) すなわち (ιxR | z)(U | y)P すなわち (T | y)P が得られ、これは z を含まないので (T | y)A ® (T | y)P が証明されたことを意味します。

　次に、"yP から (T | y)P が得られることを証明します。
　まず、T の中に含まれる項 ιxR を、一斉に P にも T にも R にも現れず x とも y とも異なる自由変数 z で置き換えた文字列を U とします。
　一方、仮定 $!xR により、($ 消去) を用いるため (z | x)R を仮定すると、(" 消去) により (U | y)P が得られ、($ 導入) により $z( (z | x)R Ù (U | y)P ) すなわち (ιxR | z)(U | y)P すなわち (T | y)P が得られます。

　次に、(T | y)P から $yP が得られることを証明します。
　まず、T の中に含まれる項 ιxR を、一斉に P にも T にも R にも現れず x とも y とも異なる自由変数 z で置き換えてた文字列を U とします。
　このとき (T | y)P は (ιxR | z)(U | y)P すなわち $z( (z | x)R Ù (U | y)P ) ですから、($ 消去) を用いるために (z | x)R Ù (U | y)P を仮定すれば、特に (U | y)P なので、($ 導入) により $yP が得られます。

　最後に S = T と (S | y)P から (T | y)P が得られることを証明します。
　まず、S 及び T の中に含まれる項 ιxR を、一斉に P にも S にも T にも R にも現れず x とも y とも異なる自由変数 z で置き換えた文字列をそれぞれ U , V とします。
　すると、命題 S = T は (ιxR | z)( U = V ) すなわち $z( (z | x)R Ù U = V ) と書けるので、($ 消去) を用いるため (z | x)R Ù U = V を仮定します。
　また、命題 (S | y)P は (ιxR | z)(U | y)P すなわち "z( (z | x)R Þ (U | y)P ) なので、(Ù 消去) と (" 消去) と (Þ 消去) により (U | y)P が得られ、これと U = V に対して (= 消去) を用いると (V | y)P が得られ、(Ù 導入) と ($ 導入) により $z( (z | x)R Ù (V | y)P ) すなわち (ιxR | z)(V | y)P すなわち (T | y)P が得られます。

　以上で (A4-6) の証明は完成しました。

　さて、(A4-5) は、命題 $!xR を仮定するという前提のもとでの主張ですが、考えている理論が少なくとも一個の定項を持ち（その一つを c とします）、しかも古典論理の場合は、若干定義を修正することにより、この前提を削除することができます。
　すなわち、P を x を含む原子命題とするとき、( $!xR Þ "x(R Þ P) ) Ù ( ( Ø $!xR ) Þ (c | x)P ) を (ιxR | x)P と略記することにするのです。

　実際、このように定義し直すことにより、$!xR を仮定したときは、上述の議論により上記の議論がそのまま適用できます。
　一方、Ø $!xR を仮定したときは、(ιxR | x)P は (c | x)P と同値ですから、これは、与えられた証明文において、項 ιxR をすべて c に置き換えれば、やはりもとの理論における証明文になっていることを意味します。
　従って、排中律と (Ú 消去) により、何ら仮定なしで上述の結果が成り立つことがわかります：

(A4-7)

少なくとも一つ定項を持つような古典論理の等号を持つ理論においては、ιxR を含む命題を上述のように定義し直せば、任意の命題 P に対し、(ιxR | x)P は ( $!xR Þ "x(R Þ P) ) Ù ( ( Ø $!xR ) Þ (c | x)P ) と同値である。 　また、ιxR を本来の項とみなして、もとの理論の推論規則を適用して得られる命題は、もとの理論においても証明可能である。