On mathematical structure in a broad sense (Japanese)

See discussions, stats, and author profiles for this publication at: https://www.researchgate.net/publication/344428145  Preprint · September 2020 DOI: 10.13140/RG.2.2.33360.53760 CITATIONS 0 1 author: Hiroki Yagisita Kyoto Sangyo University 12 PUBLICATIONS24 CITATIONS SEE PROFILE All content following this page was uploaded by Hiroki Yagisita on 30 September 2020. The user has requested enhancement of the downloaded file. 「部分関数を含む数学的構造」の 意味論、形式証明系、完全性定理 柳下浩紀 （京都産業大学） 要旨 例えば、環は言語 {+,−,×,0,1}の構造であり、環の乗法逆元の演算 ·−1 の定義域は全体でないため、環は言語 {+,−,×,·−1,0,1}の構造ではない。 一般的には、部分関数に対して関数記号を導入することは公式にはでき ないことになっている。この原稿では、関数記号の解釈として部分関数 を許容するような「広義の構造」について考え、その意味論と（ヒルベ ルト流の）形式証明系を与え、完全性定理を証明する。シーケント計算、 自然演繹に関しては、難しくないのかもしれないが、未解決問題である。 Mathematical structure in a broad sense, Partial function, Function symbol, Semantics, Hilbert-style formal deductive system, Sequent calculus, Natural deduction, Completeness theorem, Intuitionistic logic, Kripke model, Universal TM, Derivability condition. 1 1序 最初に、動機付けとして、次のことを指摘したい。有理数の全体 Qを 宇宙としたとき、例えば、 ∀x(x−1×x= 1) 0−1×0 = 1 ∃x(x×0 = 1) 0−1×06= 1 ∀x(x−1=x−1) 0−1= 0−1 ∃x(x= 0−1) 0−16= 0−1 ∀x((0 ≤x)→(√x×√x=x)) √2×√2 = 2 ∃x(x×x= 2) √2×√26= 2 ∀x((0 ≤x)→(√x=√x)) √2 = √2 ∃x(x=√2) √26=√2 などは、いずれも、素朴に判断をすれば、正しい命題ではないであろう。 これらの「素朴には真ではない文字列」には「偽と言いたくなるもの」も あれば、「偽とも言い難いもの」もあるように思われる。 通常の数学では、例えば、環の乗法逆演算を表す記号として ·−1がごく 普通に用いられている。一方、「既存の構造」においては、未定義な項の 出現を排除するために、定義域が全体ではない関数に関数記号を宛てる ことは禁止されている。既存の構造においては、関数記号が表す関数の 定義域は全体であるので、言語が ·−1と0を含むとき、 ∃x(x= 0−1) は「通常の意味論」では恒真であり、「通常の形式証明系」では証明可能 である。 2 この原稿では、関数記号の解釈として部分関数を許容するような「広 義の構造」を考えたい。例えば、言語が ·−1と0を含むとき、0−1が定義 されているかは、どうかは、「広義の構造」ごとに異なる。しかし、証明 とは正しいことを確認することであるとすれば、部分関数を許容する代 価として、上述のような「正しくない文字列」が証明されないようにす るために、（通常の形式証明系に比べて）形式証明系に何らかの制約が必 要である。 このような「広義の構造」に対して、我々がこの原稿で与えたい意味 論は２値論理である。但し、上でも見たように「未定義な項を含む閉論 理式」は、真とも偽とも言い難い場合がある。よって、まず、最初に取り 上げるべき意味論は、「真である（正しい）」、「真でない（正しくない）」 を定義することである。しかしながら、より具体的には、 「¬(A)は真である」：⇔「 Aは真でない」、 「(A)∧(B)は真である」：⇔「 A、および、Bのいずれも、が真である」、 「(A)∨(B)は真である」：⇔「 A、または、Bのいずれか、は真である」、 「(A)→(B)は真である」：⇔「 Aが真であるならば、Bは真である」、 「∀x(A)は真である」：⇔「任意の対象 xに対して、「Aは真である」」、 「∃x(A)は真である」：⇔「ある対象 xが存在して、「Aは真である」」 と定義することになるので、これらの記号に関しては、結果的に、通常 の意味論と同じである。但し、未定義な項の出現が有り得るので、否定 ¬ の意味（真でない）は通常の意味（偽である）よりも拡大されていて（広 義であり）、そのため、否定 ¬を通常の意味（偽である）で安易に解釈し ようとすると混乱する可能性が高いことに注意しておく。例えば、通常の ように、0は宇宙に存在し、0−1は宇宙に存在しないとすると、¬(0−16= 0−1)と∀x(∀y((¬(x6=y)) →(x=y))) は真であるが、0−1= 0−1と ∀x(∀y((¬(x−16=y−1)) →(x−1=y−1))) は真ではない。但し、ここで、 6=は「等しくない」を意図する「宇宙上の２項関係」を表す述語記号で ある。一方、もちろん、=は「等しい」を意図する「宇宙上の２項関係」 を表す述語記号（または、論理記号）である。排中律は一般に成立する が、それは否定 ¬を広義に（真でない、と）解釈した結果である。 さて、「通常の意味論」の定義との違いは、未定義な項が出現している 場合であっても原子閉論理式 r=s, R(t1, t2,··· , tn)が取る値を定義する ことである。そして、既に指摘したように、この違いは通常の形式証明系 の機能不全を引き起こす。しかしながら、後に完全性定理として明らかに するように、適当な修正により機能が回復できる。我々の形式証明系は、 3 通常の形式証明系より、（証明可能な論理式が少ないという意味で）弱い 形式証明系であるが、さらに、「通常の完全性定理」と「我々が示す完全 性定理」により、通常の形式証明系は、我々の形式証明系において、「定 義域が全体であること」を意図する数学的公理からなる理論と（証明可 能な論理式が同じという意味で）同値である。また、我々がこの原稿で 与える「広義の構造に対する完全性定理」の証明は、ヘンキン流の「通 常の完全性定理」の証明とあまり変わらない。 第２節で、「広義の構造」とその「意味論」を定義し、次節以降の準備 も少し行う。第３節で、（ヒルベルト流の）「形式証明系」を与え（←こ こが、この原稿の最大の工夫のしどころである）、その「健全性」を注意 し、さらに、完全性証明の準備を行う。第４節で、「完全性定理」を証明 する。 通常の意味論と我々の意味論は、「既存の構造」に対しては、同じ結果 を与えることは自明である。我々の歴史に対する常識が正しければ、「通 常の意味論」は、「通常の完全性定理」のヘンキンによる証明の影響下で 広く受容されるようになった。読者にあっては、「広義の構造」に対して、 他に適当な意味論がないか、どうか、是非、ご検討をお願いしたい。 最後に、（通常の）多種論理は（通常の）１種論理に還元できると言わ れるが、当然ながら、その正当化には多種論理の意味論が必要であろう し、「広義の構造」は「既存の構造」に還元できると主張する場合にも、 その前提として「広義の構造」に対する意味論が必要であろう。蛇足かも しれないが、広義の構造の全体は、２種論理の既存の構造の全体の「適 当な部分」に対応するように思われる。また、逆に、多種論理の広義の 構造も考えられるであろう。その他、直観主義論理のクリプキモデルに 対する広義の構造をどうすべきか、考えてみる余地もあるかもしれない。 4 2擬構造とその意味論 この節では、「広義の構造」（後に擬構造と名付ける）、「定義されてい る項」（後に既定義項と名付ける）と「意味論」を定義する。とは言え、 前節の説明で、それらの定義は容易に推測できると思われる。 言語、述語記号、関数記号、項、閉項、原子論理式、論理式、閉論理式 などの定義は、通常の（等号 =を含む）古典１階述語論理と同じであると する。但し、定数記号は 0変数関数記号であるとするが、0列（空列）が 置かれていることを示すはずの括弧は省略しても良いこととする。応用 上の必要性は低いと思われるが、一応、0変数述語記号も許容し、同様に 括弧は省略しても良いこととする。変数記号は、v0, v1, v2,··· , vn,··· で あるとする。論理式 A、変数記号全体の集合の部分集合から閉項全体の 集合への写像 eに対して、Ahe(·)/·iでAにおける（eの定義域に属する） xのすべての自由な出現を e(x)で置き換えた論理式を表すとする。これ は、閉項の（標準的な）代入である。この特別な場合として、論理式 A、 変数記号 x、閉項tに対して、Aht/xiでAにおける xのすべての自由な出 現を tで置き換えた論理式を表すとする。論理式 A、変数記号 x、項tに 対して、Aにおける xへの tの代入条件が満たされるとき、A[t/x]でAに おける xのすべての自由な出現を tで置き換えた論理式を表すとする。も ちろん、代入条件とは「単なる置き換えが代入である」という条件であっ て、具体的には、「項に含まれる変数が置き換え箇所において束縛を受け ない」という条件である。我々は意味論の定義に（また、ヘンキン定数の 添加にも）名前を用いるので、言語 Lと集合 Uに対して、L(U)でL′は Lを拡大した言語であり、L′\L=∪u∈U{due}であり、u∈Uならば due はL′の定数記号であるような L′を表すとする。念のため、du1e=du2e ならば u1=u2であることに注意する。また、dueを（対象 uのLにおけ る）標準名前（または、真名）と言うことにする。念のため、dueはLの 項ではないことに注意する。また、U⊂Vであることと L(V)がL(U)を 拡大した言語であることは同値である。 定義２．１（擬構造）： Lを言語とする。(U, F)が（Lの）擬構造であるとは、次を満たすこと を言うとする。 (1) Uは空でない集合である。 (2) Fは定義域が Lである全射である。 (3) R がLのn変数述語記号ならば、F(R) はUnの部分集合である。 5 (4) fがLのn変数関数記号ならば、F(f)は定義域がUnの部分集合 であり、値域が Uの部分集合である全射である。 □ 注意 (1) n= 0 のとき、Un={()}であり、F(R)、及び、F(f)の定義域は、 ∅、または、{()}である。 (2) 構造は擬構造である。「fがLのn変数関数記号ならば、F(f)の 定義域は Unである」ことは、擬構造が構造であるための必要十分条件で ある。 □ 定義２．２（既定義項とその解釈）： Lを言語、(U, F)を擬構造とする。L(U)の閉項 tに対して、tが（Fで） 既定義であること、及び、既定義であるとき、その解釈 tFをtの構成の 木構造に関して帰納的に次のように定義する。 (0) t∈L(U)\Lのとき： このとき、ある u∈Uが一意に存在して、 t=dueである。tは既定義であると定義し、さらに、tF:= uと定義する。 (1) t∈Lのとき： このとき、tはLの定数記号である。F(t)の定義 域が {()}のとき、かつ、そのときに限り、tは既定義であると定義する。 さらに、既定義であるとき、tF:= (F(t))() と定義する。 (2) t6∈ L(U)のとき： このとき、正のある整数 n、Lのある n変 数関数記号 fとL(U)のある閉項 t1, t2,··· , tnが一意に存在して、t= f(t1, t2,··· , tn)である。t1, t2,··· , tnが既定義であり、(t1F, t2F,··· , tnF) がF(f)の定義域の要素であるとき、かつ、そのときに限り、tは既定義であ ると定義する。さらに、既定義であるとき、tF:= (F(f))(t1F, t2F,··· , tnF) と定義する。 □ 注意 tが既定義であるとき、tF∈Uである。任意の t∈L(U)\Lに対して、 tは既定義な L(U)の閉項であり、dtFe=tである。任意の u∈Uに対し て、(due)F=uである。 □ 定義２．３（等号記号の意味論）： Lを言語、(U, F)を擬構造とする。Aが等号記号による（L(U)の）閉 論理式であるとは、L(U)のある閉項 t1, t2が存在して、Aがt1=t2であ ることを言うとする。Aは等号記号による閉論理式であるとする。この とき、Aは原子閉論理式であり、ある閉項 t1, t2が一意に存在して、Aは t1=t2である。t1, t2が既定義であり、t1F=t2Fであるとき、かつ、その ときに限り、(U, F)|=Aであると定義する。 □ 6 定義２．４（述語記号の意味論）： Lを言語、(U, F)を擬構造とする。Aが述語記号による（L(U)の）閉 論理式であるとは、Aが原子閉論理式であり、かつ、等号記号による閉 論理式ではないことを言うとする。Aは述語記号による閉論理式である とする。このとき、非負のある整数 n、ある n変数述語記号 Rと（L(U) の）ある閉項 t1, t2,··· , tnが一意に存在して、AはR(t1, t2,··· , tn)であ る。t1, t2,··· , tnが既定義であり、(t1F, t2F,··· , tnF)∈F(R) であるとき、 かつ、そのときに限り、(U, F)|=Aであると定義する。 □ 定義２．５（非原子閉論理式の意味論）： Lを言語、(U, F)を擬構造とする。Aが（L(U)の）非原子閉論理式で あるとは、Aが閉論理式であり、かつ、原子閉論理式ではないことを言 うとする。非原子閉論理式 Aに対して、(U, F)|=Aであることを、通常 のように論理式の構成の木構造に関して帰納的に定義する。すなわち、 (1) (U, F)|=¬(A) ：⇔「 (U, F)|=Aでない」、 (2) (U, F)|= (A)∧(B) ：⇔「 (U, F)|=Aである、かつ、(U, F)|=Bである」、 (3) (U, F)|= (A)∨(B) ：⇔「 (U, F)|=Aである、または、(U, F)|=Bである」、 (4) (U, F)|= (A)→(B) ：⇔「 (U, F)|=Aであるならば、(U, F)|=Bである」、 (5) (U, F)|=∀x(A) ：⇔「 既定義なL(U)の任意の閉項tに対して、(U, F)|=Aht/xiである」、 (6) (U, F)|=∃x(A) ：⇔「 既定義なL(U)のある閉項 tが存在して、(U, F)|=Aht/xiである」 と定義する。但し、もちろん、それぞれにおいて、¬(A),(A)∧(B),(A)∨ (B),(A)→(B),∀x(A),∃x(A)はそれぞれ（L(U)の）閉論理式であると する。 □ 注意 量化記号の解釈は通常、「任意の c∈L(U)\Lに対して」、「ある c∈ L(U)\Lが存在して」と定義をするのであろうが、上のように定義した 方が健全性の確認が容易になるように思われる。もちろん、これらの定 義は同値であろう（実際に、そうであることを、後出の補題２．９で述 べる）。 □ 7 例 (U, F)を言語 {+,−,×,·−1,0,1}の環の擬構造とすると、 (U, F)|=∀v0((v0−1=v0−1)→(v0−1×v0= 1)) (U, F)|=∀v0((v0−1×v0= 1) →(v0−1=v0−1)) である。Nを標準モデルとすると、 N|=∀v0((√v0=√v0)→(√v0×√v0=v0)) N|=∀v0((√v0×√v0=v0)→(√v0=√v0)) である。 □ 定義２．６（非閉論理式の意味論）： Lを言語、(U, F)を擬構造とする。Aは（L(U)の）論理式であり、か つ、閉論理式ではないとする。このとき、(U, F)|=Aであることを通常の ように定義する。すなわち、Aに自由な出現がある変数記号全体の集合か ら既定義なL(U)の閉項全体の集合への任意の写像 eに対して、(U, F)|= Ahe(·)/·iであるとき、かつ、そのときに限り、(U, F)|=Aであると定義 する。 □ 例 (U, F)を言語 {+,−,×,·−1,0,1}の環の擬構造とすると、 (U, F)|= (v0−1=v0−1)→(v0−1×v0= 1) (U, F)|= (v0−1×v0= 1) →(v0−1=v0−1) である。Nを標準モデルとすると、 N|= (√v0=√v0)→(√v0×√v0=v0) N|= (√v0×√v0=v0)→(√v0=√v0) である。 □ 以上により、(U, F)|=Aであることが、言語 L、擬構造 (U, F)、（L(U) の）論理式 Aに対して定義された。 注意 Lを言語、D1, D2を変数記号全体の集合の部分集合、e1, e2をそれぞれ D1, D2から（Lの）閉項全体の集合への写像とする。 8 次のように、論理的公理は擬構造に対して恒真であることを注意する。 補題３．３： Lを言語、Aを（Lの）論理的公理とする。このとき、（Lの）任意の 擬構造 (U, F)に対して、 (U, F)|=A である。 □ 証明 等号公理は、補題２．９ (1) より確認できる。それ以外は、容易である。 ■ 注意３．４： Lを言語、L′をLを拡大した言語とする。 (1) Lの任意の論理式 Aに対して、AがLの論理的公理であることと AがL′の論理的公理であることは同値である (2) c0はL′の定数記号であり、L′\L={c0}であるとする。A′をL′ の論理式、xをA′に出現がない変数記号とする。AをA′における c0の出 現をすべて xに置き換えたものであるとする。このとき、AがLの論理 的公理であることと A′がL′の論理的公理であることとは同値である。■ 次に、通常のように、推論規則（ただし、我々は操作と言う）を定義 する。 定義３．５（推論型）： Lを言語、Sを（Lの）論理式全体の集合の部分集合、Aを（Lの）論 理式とする。 公理操作：S⇝Aは（Lの）公理操作であるとは、Aが（Lの）論理 的公理であることを言うとする。 単純操作：S⇝Aは（Lの）単純操作であるとは、（Lの）ある論理 式Bが存在して、 B, (B)→(A)∈S であることを言うとする。 全称操作：S⇝Aは（Lの）全称操作であるとは、（Lの）ある論理 式B、ある変数記号 xとxの自由な出現がない（Lの）ある論理式 Cが 存在して、 (C)→(B)∈S であり、Aが 15 (C)→(∀x(B)) であることを言うとする。 補対操作：S⇝Aは（Lの）補対操作であるとは、ある A1∈S、 （Lの）ある論理式 A2とある変数記号 xが存在して、AがA1における ∃x(A2)の一つの出現を ¬(∀x(¬(A2))) で置き換えたものであるか、また は、¬(∀x(¬(A2))) の一つの出現を ∃x(A2)で置き換えたものであること を言うとする。 □ 定義３．６（許容操作）： S⇝Aが（Lの）許容操作であるとは、S⇝Aが（Lの）公理操作、 単純操作、全称操作、または、補対操作であることを言うとする。 □ 注意 素朴な印象としては、公理操作以外は言語にほとんど依存していない、 と言うのが妥当だと思われる。 □ 次のように、許容操作は充足性を保存することを注意する。 補題３．７： Lを言語、S⇝Aを（Lの）許容操作、(U, F)を（Lの）の擬構造と する。任意の B∈Sに対して、 (U, F)|=B であるとする。このとき、 (U, F)|=A である。 □ 証明 公理操作は補題３．３より、補対操作は補題２．７より、確認できる。 それ以外は、容易である。 ■ 注意３．８： Lを言語、L′をLを拡大した言語とする。 (1) SをLの論理式全体の集合の部分集合、AをLの論理式とする。 S⇝AがLの許容操作であることと S⇝AがL′の許容操作であること は同値である。 (2) c0はL′の定数記号であり、L′\L={c0}であるとする。S′をL′ の論理式全体の集合の部分集合、A′をL′の論理式とする。xはS′とA′ に出現がない変数記号であるとする。SをS′における c0の出現をすべて 16 xに置き換えたものであるとする。AをA′における c0の出現をすべて x に置き換えたものであるとする。このとき、S⇝AがLの許容操作であ ることと S′⇝A′がL′の許容操作であることは同値である。 ■ 定義３．９（形式証明）： Lを言語とする。（Lの）論理式 A1, A2,··· , Anに対して、 7→L(A1, A2,··· , An) であるとは、任意の k∈ {1,2,··· , n}に対して、{A1, A2,··· , Ak−1}⇝Ak が（Lの）許容操作であることを言うとする。 □ 注意３．１０： Lを言語、L′をLを拡大した言語とする。 (1) (A1, A2,··· , An)をLの論理式の列とする。このとき、7→L(A1, A2, ··· , An)であることと 7→L′(A1, A2,··· , An)であることとは同値である。 (2) c0はL′の定数記号であり、L′\L={c0}であるとする。(A′1, A′2,··· , A′n)をL′の論理式の列とする。xを(A′1, A′2,··· , A′n)に出現がない変数 記号であるとする。(A1, A2,··· , An)を(A′1, A′2,··· , A′n)における c0の 出現をすべて xに置き換えたものとする。このとき、7→L(A1, A2,··· , An) であることと 7→L′(A′1, A′2,··· , A′n)であることとは同値である。 ■ 定義３．１１（証明可能）： Lを言語とする。 (1) （Lの）論理式 Aに対して、 `LA であるとは、正のある整数 nと（Lの）ある論理式 A1, A2,··· , An−1が存 在して、 7→L(A1, A2,··· , An−1, A) であることを言う。 (2) Tを（Lの）閉論理式全体の集合の部分集合とする。（Lの）論理 式Aに対して、 T`LA であるとは、非負のある整数 nとある C1, C2,··· , Cn∈Tが存在して、 `L(Cn)→((Cn−1)→(··· → ((C2)→((C1)→(A))) ···)) であることを言うとする。 □ 17 注意 (0) `LAと∅ `LAは同値である。 (1) T`LAの定義の仕方は、通常とは少し違っている。我々の定義は、 演繹定理そのものである。 (2) Tを閉論理式全体の集合の部分集合としたとき、命題論理により （Tから）証明可能であることと「命題公理の公理操作」と「単純操作」 だけに操作を限定して（Tから）証明可能であることは同じである。以 後の議論では、このことを特に明示的に注意することなく用いる。 □ 補題３．１２（健全性）： Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。Aを （Lの）論理式とし、 T`LA であるとする。このとき、（Lの）任意の擬構造 (U, F)に対して、 [∀C∈T: (U, F)|=C] =⇒(U, F)|=A である。 □ 証明 ある C1, C2,··· , Cn∈Tが存在して、 `L(Cn)→((Cn−1)→(··· → ((C2)→((C1)→(A))) ···)) である。よって、補題３．７を用いて、形式証明の構成に関する帰納法で、 (U, F)|= (Cn)→((Cn−1)→(··· → ((C2)→((C1)→(A))) ···)) が確認される。一方、Ck∈Tより (U, F)|=Ckであるので、(U, F)|=A が確認される。 ■ 定義３．１３（矛盾、無矛盾）： Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。 (1) Tが（Lで形式的に）矛盾しているとは、（Lの）任意の論理式 A に対して、 T`LA であることを言うとする。 (2) Tが（Lで形式的に）無矛盾であるとは、Tが（Lで形式的に）矛 盾していないことを言うとする。 □ 18 注意 (1) Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。T が（Lで形式的に）矛盾していることと（Lの）ある論理式 Aが存在して、 T`LAかつ T`L¬(A) であることは同値である。以後の議論では、このことを明示的に注意す ることなく、用いる。 (2) 健全性とは「形式的に矛盾」していることは「（真に）矛盾」し ているという主張であり、完全性とは「形式的に無矛盾」なことは「（真 に）無矛盾」であるという主張であるとも考えられるであろう。もちろ ん、これは、意味論は普遍的であるのに対し、形式証明系は個別的であ る、という素朴な印象によるものである。しかしながら、「通常の意味論」 と「我々の意味論」は異なっている。例えば、{¬(∃v0(v0= 0−1))}は「通 常の意味論」では矛盾しているが、「我々の意味論」では無矛盾である。 □ 以下、完全性の証明のための準備をする。具体的には、後出の補題３． ２０を証明する。実質的に、ここから（おおよそ、この原稿の半分）が ヘンキンの方法による完全性定理の証明である。 補題３．１４（ヘンキン補題）： Lを言語、L′をLを拡大した言語とする。c0はL′の定数記号であり、 L′\L={c0}であるとする。AをLの論理式、xを変数記号とし、∃x(A) がLの閉論理式であるとする。TをLの閉論理式全体の集合の部分集合 とする。このとき、T∪ {∃x(A)}がLで形式的に無矛盾であることと T∪ {c0=c0, Ahc0/xi}がL′で形式的に無矛盾であることとは同値であ る。 □ 証明 T∪{∃x(A)}がLで形式的に矛盾しているとする。このとき、 T`L¬(∃x(A)) であるので、 T∪{c0=c0, Ahc0/xi} `L′¬(∃x(A)) である。一方、代入公理より `L′(c0=c0)→((∀x(¬(A))) →(¬(Ahc0/xi))) であるので、 19 {c0=c0} `L′(Ahc0/xi)→(¬(∀x(¬(A)))) である。よって、補対操作より、 {c0=c0} `L′(Ahc0/xi)→(∃x(A)) T∪{c0=c0, Ahc0/xi} `L′∃x(A) である。したがって、T∪ {c0=c0, Ahc0/xi}はL′で形式的に矛盾して いる。 逆に、T∪{c0=c0, Ahc0/xi}はL′で形式的に矛盾しているとする。こ のとき、ある C1, C2,··· , Cn∈Tが存在して、 `L′ (c0=c0) →((Cn)→((Cn−1)→(··· → ((C2)→((C1)→(¬(Ahc0/xi)))) ···))) である。よって、L′の論理式のある列 (A′1, A′2,··· , A′m)が存在して、A′m は (c0=c0) →((Cn)→((Cn−1)→(··· → ((C2)→((C1)→(¬(Ahc0/xi)))) ···))) であり、 7→L′(A′1, A′2,··· , A′m) である。ここで、xと異なるある変数記号 yが存在して、yはA, (A′1, A′2, ··· , A′m)に出現がない。このとき、注意３．１０ (2) より、 `L (y=y) →((Cn)→((Cn−1)→(··· → ((C2)→((C1)→(¬(A[y/x])))) ···))) である。>を (∀v0(v0=v0)) ∨(¬(∀v0(v0=v0))) とし、Cを ((···(((>)∧(C1)) ∧(C2)) ∧···)∧(Cn−1)) ∧(Cn) とする。`L>、T`LCである。対象公理より、 20 `L(C)→(¬(A[y/x])) である。よって、等号公理より、 `L(y=x)→((C)→(¬(A))) `L(>)→((y=x)→((C)→(¬(A)))) である。よって、全称操作より、 `L(>)→(∀y((y=x)→((C)→(¬(A))))) `L∀y((y=x)→((C)→(¬(A)))) である。よって、代入公理より、 `L(x=x)→((x=x)→((C)→(¬(A)))) である。よって、対象公理より `L(C)→(¬(A)) であるので、全称操作より `L(C)→(∀x(¬(A))) `L(C)→(¬(¬(∀x(¬(A))))) である。よって、補対操作より `L(C)→(¬(∃x(A))) であるので、 T`L¬(∃x(A)) である。T∪{∃x(A)}はLで形式的に矛盾している。 ■ 補題３．１５（ヘンキン定数）： Lを言語、TをLの閉論理式全体の集合の部分集合とする。TはLで 形式的に無矛盾であるとする。このとき、Lを拡大したある言語 L′とL′ の閉論理式全体の集合のある部分集合 T′が存在して、次を満たす。 (1) c′∈L′\Lならば、c′はL′の定数記号である。 (2) T′はL′で形式的に無矛盾である。 21 (3) AはLの論理式で、xは変数記号であるとする。∃x(A)はLの閉 論理式であり、 T`L∃x(A) であるとする。このとき、L′のある定数記号 c′が存在して、 (c′=c′)∧(Ahc′/xi)∈T′ である。 (4) T⊂T′である。 □ 証明 WをAがLの論理式で、xが変数記号で、∃x(A)がLの閉論理式 で、T`L∃x(A)である (x, A)全体の集合とする。L′:= L(W)とする。 (x, A)∈Wに対して、φ(x,A)を (d(x, A)e=d(x, A)e)∧(Ahd(x, A)e/xi) とする。T′:= T∪(∪(x,A)∈W{φ(x,A)})とする。 このとき、L′はLを拡大した言語であり、T′はL′の閉論理式全体の集 合の部分集合であり、(1), (3), (4) を満たす。 (2) を示す。背理法。T′はL′で形式的に矛盾しているとする。⊥を (∀v0(v0=v0)) ∧(¬(∀v0(v0=v0))) とする。ある C1, C2,··· , Cn∈T′が存在して、 `L′(Cn)→((Cn−1)→(··· → ((C2)→((C1)→(⊥))) ···)) である。L′の論理式のある列 (B1, B2,··· , Bm)が存在して、Bmは (Cn)→((Cn−1)→(··· → ((C2)→((C1)→(⊥))) ···)) であり、 ⇝L′(B1, B2,··· , Bm) である。ある (x1, A2),(x2, A2),··· ,(xk, Ak)∈Wが存在して、任意の (x, A)∈Wに対して、d(x, A)eが(B1, B2,··· , Bm)に出現しているな らば、 (x, A)∈ {(x1, A2),(x2, A2),··· ,(xk, Ak)} である。注意３．１０ (1) より、 22 ⇝L({(x1,A2),(x2,A2),··· ,(xk,Ak)})(B1, B2,··· , Bm) である。よって、{C1, C2,··· , Cn}はL({(x1, A2),(x2, A2),··· ,(xk, Ak)}) で形式的に矛盾している。さらに、 {C1, C2,··· , Cn} ⊂ T∪{φ(x1,A1), φ(x2,A2),··· , φ(xk,Ak)} であり、T∪ {φ(x1,A1), φ(x2,A2),··· , φ(xk,Ak)}がL({(x1, A1),(x2, A2),··· , (xk, Ak)})で形式的に矛盾している。lをT∪{φ(x1,A1), φ(x2,A2),··· , φ(xl,Al)} がL({(x1, A1),(x2, A2),··· ,(xl, Al)})で形式的に矛盾している最小の非負 の整数とする。仮定より、l6= 0である。よって、T∪{φ(x1,A1), φ(x2,A2),··· , φ(xl−1,Al−1)}はL({(x1, A1),(x2, A2),··· ,(xl−1, Al−1)})で形式的に無矛盾 である。さらに、(xl, Al)∈Wより T`L∃xl(Al) であるので、(T∪ {φ(x1,A1), φ(x2,A2),··· , φ(xl−1,Al−1)})∪ {∃xl(Al)}はL ({(x1, A1),(x2, A2),··· ,(xl−1, Al−1)})で形式的に無矛盾である。ところ が、そうすると、補題３．１４より、T∪{φ(x1,A1), φ(x2,A2),··· , φ(xl,Al)}が L({(x1, A1),(x2, A2),··· ,(xl, Al)})で形式的に無矛盾である。矛盾。よっ て、(2) が満たされる。 ■ 定義３．１６（極大無矛盾）： Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。Tが（L で形式的に）極大無矛盾であるとは、次が成り立つことを言うとする。 (1) Tは（Lで形式的に）無矛盾である。 (2) （Lの）閉論理式全体の集合の任意の部分集合 Sに対して、Sが （Lで形式的に）無矛盾であるならば、 T⊂S=⇒T=S である。 □ 補題３．１７： Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。Tは（L で形式的に）極大無矛盾であるとする。このとき、（Lの）任意の閉論理 式Cに対して、 T`LC⇐⇒ C∈T である。 □ 23 証明 C∈Tならば T`LCであることは、自明である。 T`LCとする。このとき、T∪{C}が矛盾していれば Tが矛盾してい る。よって、仮定より、T∪{C}は無矛盾であるので、さらに、C∈Tで ある。 ■ 補題３．１８： Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。Tは（L で形式的に）無矛盾であるとする。このとき、Tが（Lで形式的に）極大 無矛盾であるのは、（Lの）任意の閉論理式 Cに対して、 C∈Tまたは ¬(C)∈T であるとき、かつ、そのときに限る。 □ 証明 Tが極大無矛盾であるとする。T`LCのとき、補題３．１７より、 C∈Tである。T`LCでないとき、T∪ {¬(C)}は無矛盾であるので、 ¬(C)∈Tである。よって、C∈T、または、¬(C)∈Tである。 Tは極大無矛盾でないとする。ある閉論理式 Cが存在して、C∈Tで なく、T∪{C}は無矛盾である。¬(C)∈Tであるとすると、T∪{C}は 矛盾しているので、矛盾。よって、¬(C)∈Tでない。 ■ 補題３．１９： Lを言語、Tを（Lの）閉論理式全体の集合の部分集合とする。Tは（L で形式的に）無矛盾であるとする。このとき、（Lの）閉論理式全体の集 合のある部分集合 T∗が存在して、T∗は（Lで形式的に）極大無矛盾であ り、T⊂T∗である。 □ 証明 ツォルンの補題の条件を確認する。Wを空でない（ここで当然、考え るべき半順序集合の）全順序部分集合とする。∪S∈WSは、閉論理式全体 の集合の部分集合である。∪S∈WSが、無矛盾であることを示す。背理法。 ∪S∈WSが、矛盾しているとする。⊥を (∀v0(v0=v0)) ∧(¬(∀v0(v0=v0))) とする。ある C1, C2,··· , Cn∈ ∪S∈WSが存在して、 `L(Cn)→((Cn−1)→(··· → ((C2)→((C1)→(⊥))) ···)) である。Wは空でない全順序集合であるので、ある S∈Wが存在して、 24 `L∗∃v0(v0=v0) である。よって、補題３．２０の条件 (3) より、L∗のある閉項 t∗が存在 して、 (t∗=t∗)∧(t∗=t∗)∈T∗ である。よって、(t∗=t∗)∈T∗であり、t∗∈Vである。よって、V6=∅ であり、U6=∅である。 — ［ステップ６］ Wの同値類から代表元を選択する写像が存在する。 σをその一つとする。すなわち、σはUから Vへの単射であり、任意の u∈Uに対して、 u= [σ(u)]T∗ である。さらに、任意の t∈Vに対して、 (σ([t]T∗) = t)∈T∗, (t=σ([t]T∗)) ∈T∗ である。u∈Uに対して、σ(u)を（σによる対象 uの）仮名と言うこと にする。因みに、（uのL∗における）真名（標準名前）は dueであり、こ れは L∗の項ではなかった。対して、σ(u)はL∗の閉項である。 — ［ステップ７］ L∗を定義域とする全射 Fを以下のように定める。 (i) R がL∗の（n変数）述語記号であるとき： F(R) := {(u1, u2,··· , un)∈Un|R(σ(u1), σ(u2),··· , σ(un)) ∈T∗} と定める。 (ii) fがL∗の（n変数）関数記号であるとき： DF f:= {(u1, u2,··· , un)∈Un|f(σ(u1), σ(u2),··· , σ(un)) ∈V} とおく。 F(f)を定義域が DF fであり、任意の (u1, u2,··· , un)∈DF fに対 して、 (F(f))(u1, u2,··· , un) := [f(σ(u1), σ(u2),··· , σ(un))]T∗ である全射とする。 — ［ステップ８］ (U, F)はL∗の擬構造である。 — 以下の数ステップを費やして、通常の場合と大体、同じように任意の A∈Tに対して、(U, F)|=Aであることを示す。 — 31 ［ステップ９］ L∗の任意の閉項 tに対して、 (i) tが既定義であることと t∈Vであることは、 同値であること (ii) 「tが既定義であり、かつ、t∈Vである」ならば、 tF= [t]T∗であること をtの構成の木構造に関する帰納法で示す。 — (a) tがL∗の定数記号であるとき： tは既定義であるとする。このとき、F(t)の定義域は {()}である。す なわち、DF t={()}である。よって、t∈Vである。 t∈Vであるとする。このとき、() ∈DF tであるので、DF t={()}であ る。よって、tは既定義である。 tが既定義であり、かつ、t∈Vであるとする。このとき、tF= (F(t))() = [t]T∗である。 (b) tがL∗の定数記号でないとき： 正のある整数n、L∗のあるn変数関数記号fとL∗のある閉項t1, t2,··· , tn が一意に存在して、 t=f(t1, t2,··· , tn) である。 tは既定義であるとする。このとき、t1, t2,··· , tnは既定義であり、かつ、 (t1F, t2F,··· , tnF)∈DF fである。よって、帰納法の仮定より、 t1, t2,··· , tn∈ Vであり、かつ、([t1]T∗,[t2]T∗,··· ,[tn]T∗)∈DF fである。よって、 (f(σ([t1]T∗), σ([t2]T∗),··· , σ([tn]T∗)) = f(σ([t1]T∗), σ([t2]T∗),··· , σ([tn]T∗))) ∈T∗ である。一方、ステップ６より (σ([tk]T∗) = tk)∈T∗であるので、ステッ プ２を順次、用いることより T∗`L∗f(t1, σ([t2]T∗),··· , σ([tn]T∗)) = f(t1, σ([t2]T∗),··· , σ([tn]T∗)) T∗`L∗f(t1, t2, σ([t3]T∗),··· , σ([tn]T∗)) = f(t1, t2, σ([t3]T∗),··· , σ([tn]T∗)) ··· T∗`L∗f(t1, t2,··· , tn) = f(t1, t2,··· , tn) である。すなわち、T∗`L∗t=tであるので、t∈V。 32 t∈Vとする。 このとき、 (f(t1, t2,··· , tn) = f(t1, t2,··· , tn)) ∈T∗ である。よって、定義公理より、T∗`L∗tk=tkである。tk∈V。よって、 帰納法の仮定より、tkは既定義であり、tkF= [tk]T∗である。よって、ス テップ６より (tk=σ([tk]T∗)) ∈T∗であるので、同様にステップ２を順 次、用いることより T∗`L∗ f(σ([t1]T∗), σ([t2]T∗),··· , σ([tn]T∗)) = f(σ([t1]T∗), σ([t2]T∗),··· , σ([tn]T∗)) であるので、 f(σ([t1]T∗), σ([t2]T∗),··· , σ([tn]T∗)) ∈V f(σ(t1F), σ(t2F),··· , σ(tnF)) ∈V である。よって、(t1F, t2F,··· , tnF)∈DF fである。tは既定義。 tが既定義であり、かつ、t∈Vであるとする。tは既定義であるので、 tkは既定義である。帰納法の仮定より、tk∈V、tkF= [tk]T∗である。よっ て、ステップ６より、 (tk=σ(tkF)) ∈T∗ である。よって、t∈Vより (f(t1, t2,··· , tn) = f(t1, t2,··· , tn)) ∈T∗ であるので、ステップ２を順次、用いることより T∗`L∗f(σ(t1F), σ(t2F),··· , σ(tnF)) = f(t1, t2,··· , tn) である。よって、 (f(σ(t1F), σ(t2F),··· , σ(tnF)), f(t1, t2,··· , tn)) ∈W であるので、tが既定義であることより、tF= (F(f))(t1F, t2F,··· , tnF) = [f(σ(t1F), σ(t2F),··· , σ(tnF))]T∗= [f(t1, t2,··· , tn)]T∗= [t]T∗である。— ［ステップ１０］ 任意の u∈Uに対して、σ(u)は既定義であり、 (σ(u))F=u であることを示す。 — 33 u∈Uとする。σ(u)∈Vであるので、ステップ９より、σ(u)は既定義で あり、(σ(u))F= [σ(u)]T∗である。よって、ステップ６より、(σ(u))F=u。 — ［ステップ１１］ L∗の任意の閉論理式 Aに対して、A∈T∗と(U, F)|= Aが同値であることを論理式の長さ（¬,∧,∨,→,∀,∃の出現の個数）に関 する帰納法で示す。 — (a) t, s をL∗の閉項とし、(U, F)|=t=sとする。t, s は既定義で、 tF=sFである。ステップ９より、t, s ∈Vであり、tF= [t]T∗, sF= [s]T∗ である。よって、[t]T∗= [s]T∗であり、(t, s)∈W。(t=s)∈T∗。 (b) t, s をL∗の閉項とし、(t=s)∈T∗とする。このとき、(t, s)∈W であるので、t, s ∈V、[t]T∗= [s]T∗。ステップ９より、t, s は既定義で、 tF=sF。(U, F)|=t=s。 (c) R をL∗の（n変数）述語記号、t1, t2,··· , tnをL∗の閉項とし、 (U, F)|= R(t1, t2,··· , tn)とする。t1, t2,··· , tnは既定義であり、(t1F, t2F, ··· , tnF)∈F(R) である。よって、R(σ(t1F), σ(t2F),··· , σ(tnF)) ∈T∗。 また、ステップ９より、tk∈V、tkF= [tk]T∗である。よって、ステップ ６より (σ(tkF) = tk)∈T∗であるので、ステップ２を順次、用いることよ りR(t1, t2,··· , tn)∈T∗である。 (d) R をL∗の（n変数）述語記号、t1, t2,··· , tnをL∗の閉項とし、 R(t1, t2,··· , tn)∈T∗とする。定義公理より、T∗`L∗tk=tkである。 tk∈V。ステップ９より、tkは既定義で、tkF= [tk]T∗。よって、ステップ ６より(tk=σ(tkF)) ∈T∗であるので、ステップ２を順次、用いることより R(σ(t1F), σ(t2F),··· , σ(tnF)) ∈T∗である。よって、(t1F, t2F,··· , tnF)∈ F(R) であり、(U, F)|= R(t1, t2,··· , tn)。 (e) ∀x(B)はL∗の閉論理式であるとし、∀x(B)∈T∗でないとする。 このとき、 ¬(∀x(B)) ∈T∗ である。一方、代入公理より `L∗(x=x)→((∀x(¬(¬(B)))) →(¬(¬(B)))) `L∗(∀x(¬(¬(B)))) →(¬(¬(B))) `L∗(∀x(¬(¬(B)))) →(B) `L∗(∀x(¬(¬(B)))) →(∀x(B)) `L∗(¬(∀x(B))) →(¬(∀x(¬(¬(B))))) `L∗(¬(∀x(B))) →(∃x(¬(B))) 34 であるので、 T∗`L∗∃x(¬(B)) である。よって、補題３．２０の条件 (3) をここで使うことになり、L∗の ある閉項 tが存在して、 (t=t)∧(¬(Bht/xi)) ∈T∗ である。(t=t)∈T∗、¬(Bht/xi)∈T∗であるので、t∈Vであり、か つ、Bht/xi ∈ T∗でない。よって、ステップ９と帰納法の仮定より、tは 既定義であり、かつ、(U, F)|=Bht/xiでない。よって、既定義な L∗(U) のある閉項 tが存在して、「(U, F)|=Bht/xiでない」。「既定義な L∗(U) の任意の閉項 tに対して、(U, F)|=Bht/xi」でない。(U, F)|=∀x(B)で ない。 (f) ∀x(B)はL∗の閉論理式であるとし、∀x(B)∈T∗とする。tを既 定義な L∗(U)の閉項とする。tF∈Uである。ステップ１０より、σ(tF)は 既定義であり、 (σ(tF))F=tF である。σ(tF)∈Vより、 (σ(tF) = σ(tF)) ∈T∗ であり、σ(tF)はL∗の閉項である。一方、代入公理より `L∗(σ(tF) = σ(tF)) →((∀x(B)) →(Bhσ(tF)/xi)) であるので、 Bhσ(tF)/xi ∈ T∗ である。よって、帰納法の仮定より、(U, F)|=Bhσ(tF)/xiである。補題 ２．９ (1) より、(U, F)|=Bht/xiである。以上より、(U, F)|=∀x(B)。 (g) ∃x(B)はL∗の閉論理式であるとし、(U, F)|=∃x(B)とする。こ のとき、既定義な L∗(U)のある閉項 tが存在して、 (U, F)|=Bht/xi である。tF∈Uである。ステップ１０より、σ(tF)は既定義であり、 35 (σ(tF))F=tF である。よって、補題２．９ (1) より、 (U, F)|=Bhσ(tF)/xi である。σ(tF)∈Vより、σ(tF)はL∗の閉項である。よって、Bhσ(tF)/xi はL∗の閉論理式である。したがって、帰納法の仮定より、 Bhσ(tF)/xi ∈ T∗ である。一方、σ(tF)∈Vより、 (σ(tF) = σ(tF)) ∈T∗ である。よって、代入公理より、 T∗`L∗(∀x(¬(B))) →(¬(Bhσ(tF)/xi)) T∗`L∗(Bhσ(tF)/xi)→(¬(∀x(¬(B)))) T∗`L∗¬(∀x(¬(B))) である。よって、補対操作より、∃x(B)∈T∗である。 (h) ∃x(B)はL∗の閉論理式であるとし、∃x(B)∈T∗とする。補題３． ２０の条件 (3) をここで使うことになり、L∗のある閉項 tが存在して、 (t=t)∧(Bht/xi)∈T∗ である。よって、(t=t)∈T∗、(Bht/xi)∈T∗である。t∈Vであるの で、tは既定義である。また、帰納法の仮定より、(U, F)|= (Bht/xi)で ある。したがって、(U, F)|=∃x(B)である。 (i) ¬,∧,∨,→については、容易である。 — ［ステップ１２］ A∈Tとする。このとき、T⊂T∗とステップ１１ によって、(U, F)|=A。■ 注意 上の証明において、T∗はL∗で極大無矛盾であるが、一方、T∗∪(∪u∈U{due =σ(u)})はL∗(U)で完全無矛盾であろう。また、L∗(U)の任意の閉論理 式Aに対して、BをAにおける真名（d·e）のすべての出現を仮名（σ(·)） で置き換えたものとすると、T∗∪(∪u∈U{due=σ(u)})`L∗(U)Aであるこ とと B∈T∗であることは同値であろう。上で構成された (U, F)の重要な 特徴は、任意の u∈Uに対して、既定義な L∗のある閉項 tが存在して、 36 u=tFであることであるように思われる。擬構造がこのような特徴を持 つことと補題３．２０の条件 (2), (3) を満たすある T∗が存在して、擬構 造が T∗から上の方法（ヘンキンの方法）で構成される (U, F)と同型であ ることは同値であるように思われる。 □ 定理４．２（完全性定理）： Lを言語、TをLの閉論理式全体の集合の部分集合とする。 (1) Tが（Lで形式的に）無矛盾であることと（Lの）ある擬構造 (U, F) が存在して、任意の C∈Tに対して、(U, F)|=Cであることは、同値で ある。 (2) Aを（Lの）論理式とする。このとき、T`LAであることと（Lの） 任意の擬構造 (U, F)に対して、「「任意の C∈Tに対して、(U, F)|=Cで ある」ならば、(U, F)|=Aである」ことは同値である。 □ 証明 (1) (a) Tが（Lで形式的に）無矛盾であるとする。このとき、補題４．１ より、Lを拡大したある言語 L′とL′のある擬構造 (U, F′)が存在して、任 意の C∈Tに対して、(U, F′)|=Cである。Fを定義域が Lである全射 で、任意の s∈Lに対して、 F(s) := F′(s) であるものとする。(U, F)はLの擬構造である。さらに、補題２．１０ (4) より、任意の C∈Tに対して、(U, F)|=Cである。 (b) (U, F)は（Lの）擬構造であり、任意のC∈Tに対して、(U, F)|=C であるとする。⊥を (∀v0(v0=v0)) ∧(¬(∀v0(v0=v0))) とする。このとき、（閉論理式における ¬,∧の意味論の帰納的定義によ り、）(U, F)|=⊥でない。Tが（Lで形式的に）無矛盾であることを示す。 背理法。Tが（Lで形式的に）矛盾しているとする。このとき、T`L⊥ である。よって、補題３．１２より、(U, F)|=⊥。矛盾。よって、Tは （Lで形式的に）無矛盾である。 (2) (a) T`LAでないとする。ある ¯ Aが存在して、 ¯ AはAの閉包である。 37 代入公理と対象公理を順次、用いることより `L¯ A→A であるので、T`L¯ Aでない。よって、T∪{¬(¯ A)}は（Lで形式的に）無 矛盾である。よって、(1) より、（Lの）ある擬構造 (U, F)が存在して、任 意の C∈T∪{¬(¯ A)}に対して、(U, F)|=Cである。(U, F)|=¬(¯ A)であ るので、（閉論理式における ¬の意味論の帰納的定義により、）(U, F)|=¯ A でない。(U, F)|=Aでない。 (b) T`LAであるならば云々であることは、補題３．１２そのもので ある。 ■ 38 Hiroki Yagisita (Kyoto Sangyo University) Abstract: For example, a ring is a structure of the language {+,−,×,0,1}, and a ring is not a structure of the language {+,−,×,·−1,0,1}because the domain of the operation ·−1of the multiplicative inverse is not the whole. In general, it is not officially possible to introduce a function symbol into a partial function. In this paper, we consider “a structure in a broad sense” that allows a partial function as the interpretation of a function symbol, we give its semantics and a Hilbert-style formal deductive system, and we prove the completeness theorem. Regarding sequent calculus and natural deduction, it may not be difficult, but it is an unsolved problem. 感想 「通常の述語論理」が未定義項を排除しているのは、「命題論理からの 発展」として述語論理が見なされることが常態であった、という歴史的 経緯によるのではないのであろうか。もう一つは、それなりに相対性が 浸透した後も、「等号にも、若干の相対性がある」（例えば、√2 = √2を どの宇宙で考えているのか？）ことについては注意を向けられることが 多くなかったということもあるかもしれない。 K. Godel, Die Vollstandigkeit der Axiome des logischen Funktionenkalkuls, Monatsh. Math. Phys., 37 (1930), 349-360. L. Henkin, The completeness of the first-order functional calculus, J. Symbolic Logic, 14 (1949), 159-166. 田中一之『数学基礎論講義』（日本評論社） 嘉田勝『論理と集合から始める数学の基礎』（日本評論社） 坪井明人『数理論理学の基礎・基本』（牧野書店） 菊池誠『不完全性定理』（共立出版） 39 View publication statsView publication stats