だが , (v) (vii) 第 11 章めくるめく非古典論理の世界にようこそ ! ◇ロ P →ロ P ◇◇ P →◇ P 307 そこで , いくつかの還元法則を T に付け加えて多重様相の種類を減らすことを考えてみよう。 (iii) ◇ P ←◇◇ P (iv) ロ P 冖ロロ P これらの還元法則のすべてをつけ加える必要はない。 ◇ P →ロ◇ P (vi) ◇◇ P →◇ P (viiD ◇ロ P →ロ P ロ P →ロロ P をつけ加えるだけでよい。逆はすべて T の theorem だから。さらに , (v) ト T(vi), (vi)F T(v), ( 1 ) (v) または (vi) のどちらかを T につけ加えれば , (v)æ(vii) の 4 つの還元法則はすべて出てく 同ト T 圃 , 圃ト T 同 , ( v ) ト T 圃という関係があるので , ( 2 ) 圃または同のどちらかをつけ加えれ ば , 同と圃が得られるが , (v) と (vi) は出てこ ない。 そこで次のような新しい公理系が生まれ (v) ◇ P →ロ◇ P ーー→ 圃ロ P →ロロ P ーー同 5 4 る。 【定義】 T に T に (v) GiD ロ A →ロロ A ( この公理図式を 4 と呼ぶ ) をつけ加えた公理系を S4 と言 ◇ A →ロ◇ A ( この公理図式を 5 と呼ぶ ) をつけ加えた公理系を S5 と言う。 S 4 を特徴づける公理 4 は S 5 では theorem として導かれる。というわけで , T の theorem はすべて S 4 の theorem でもあり , S 4 の theorem はすべて S 5 の theorem でもある , という 具合になっている。 ついでにもう 1 つ公理系を導入しておこう。 【定義】 T に A →ロ◇ A ( この公理を B と呼ぶ ) をつけ加えた公理系を B と言う。 A →ロ◇ A は S 5 では theorem として導くことができるが , S 4 ではできない。 T の theorem はすべて B の theorem であり , B の theorem はすべて S5 の theorem でもある。 S 4 では様相は 7 種類になる S4 では , 次の theorem が導かれる。 S5 S4 ( 6 ) ( 7 ) ⑧ ロ P ←ロロ P ◇ P ←◇◇ P ロ◇ P ←ロ◇ロ◇ P
433 364 364 31 293 25 1 2 2 180 A / 引 , B / 引 246 A / の = 1 = 1 = 1 ド 0 AB A(a) 127 , 142 V(aD VM(P) VM(A) V(A)=O V(A) = 1 136 137 138 138 138 ND PAI PA2 PPL 索引 ( 記号 ) 260 293 342 342 173 ー 74 VM,6(A)= 1 VMI(A) =VM2(A) 180 145 0 329 SOL 340 148 177 177 306 307 307 B 307 B ( の / 引 C[A] 52 123 r, △ , ⑧ , ・ D DN 136 235 K 306 M/a N 351 P, Q, R, PI, P2, P3, 143 173 幻 7 Prem R 351 Q 351 182 25 25 , 122 VM,61(A)=VM, の (A) VM,6(r)= 1 V/a 143 1 5 1 290 VM , び ( 中了 1 了 2 ・・・ ) VM ( 中 n の・・・碼 1 177 3 い T 4 5 中 Z M= く D,V> 35 1 3 ロ 1 2 2 31 1 137 M=<m,V,IF> m = くび 0 , S, ミ > 351 300 3 1 1 300 び び び 列 了 270 320 139 173 145 352 146 341 321 299 122 ー 23 123 333 RAA Reit Rep S 5 T V V(P) V(A) v(Pi) 296 2 1 8 2 18 307 307 AFOL APL B FOL FPL K L MPL 2 322 250 307 320 289 202 306 2 2 342 342 1 2 2 min {x, y) max {x, y) 306 56 = 1 = 1 theorem 1 theorem 2 theorem 3 , 4 , 5 theorem 6 theorem 7 , 8 , 9 55 136 D I—D 13 290 290 251 252 257 258 259 259
252 第Ⅲ部論理をもう 1 つの目で見る 引き出された式かのいずれかであることをチェックしてみよう。ちゃんと proof であるための条 件を満たしていることがわかる。したがって , (p → Q) → ()Q → R) → (P → R)) は APL の theorem こいつを theorem2 と名づける。 公理からの proof はけっこうたいへんだが , 練習を積んで君たちもこのくらいの proof は自由 ・・というのは嘘。ちょっと昔の教科書はこの手の 自在に構成できるようになる必要がある。 proof がわんさと出てきて , 学習者をうんざりさせていた。実際に論理式を導き出したり , 論証 の正しさを確かめるには , 自然演繹やタブローというもっと使いやすい方法がある。 こで重要 なのは公理系とは何かということをしつかり理解することだ。 公理系の健全性と完全性 本章で公理系をつくったそもそものねらいはすべてのトートロジーを数え上げることにあっ た。したがって , ( 1 ) どんなトートロジーも上記の 3 つのかたちをした公理のいくつかを出発点に 置いて MP によって変形して行くと出てくる , ( 2 ) そのようにして出てくる論理式はどれもトー トロジーになっている , という 2 つのことがらが成り立っていてくれないと困る。つまり , 論理式 A が APL の theorem である A はトートロジーである。 がなりたって欲しい。一般に 【定義】論理式 A が公理系 K の theorem である A はトートロジーである がなりたっとき , 公理系 K は健全 (sound) であると言う。逆に 論理式 A がトートロジーであるつ A は公理系 K の theorem である がなりたっとき , 公理系 K は完全 (complete) であると言う。 また , 公理系が健全で完全であることをひっくるめて完全であると言うこともある。我々の公 理系 APL は健全かっ完全である。健全であることの証明は簡単だが , 完全であることの証明の ためにはずいぶんと準備が必要だ。そこで , 完全性の証明の方は 10.3 以降で行うこととして , こでは APL の健全性の証明を練習問題としておこう ( それくらい簡単なのだ ) 。 いじっていたら出た ! ? 10.1.4 仮定からの演繹 APL の健全性を示せ。 練習問題 76 ところで , 公理系は論理的帰結の概念のこれまでとは違ったとらえ方も与えてくれる。それを
第 12 章古典論理にもまだ学ぶことがたくさん残ってる 《モデル M 》 論議領域 = 自然数の集合 V(S) : 任意の自然数 n にその次の自然数 n 十 1 を対応させる関数 ( これを後続者関数 succes - sor function と言う ) V( + ) : 自然数 n と m の組にその和を対応させる関数 V( ・ ) : 自然数 n と m の組にその積を対応させる関数 V( の : 自然数 0 331 APL, AFOL などに定義されてきたいくつかの概念は同じように公理的理論にたいしても定義 theorem, 無矛盾性などの定義 を , 単に理論 K のモデルと言う。また理論 K はモデル M をもつ , などと言う。 【定義】理論 Q にとってのモデル M のように , 理論 K のすべての公理を真にするモデル は自分で確かめてほしい。 1 には 0 という風に ) 」ということを述べたものだと言える。 Q 4 以降 自然数がある ( 3 には 2 , は , 「 0 はいかなる自然数の後続者でもない」 , Q3 は , 「 0 以外の自然数には , それぞれ直前の このモデル M で解釈すると例えば Q 1 は , 「異なる自然数の後続者同士もまた異なる」 , Q 2 できる。 【定義】以下の条件を満たす , Q の論理式の有限個の列 BI, B2, あるとする ) を , C の Q における proof ( 証明 ) という。 [ 条件 ] Bi ( ただし 1 ミに n ) は , 次のいずれかである。 ( 1 ) 0 の公理である。 n ( この最後の Bn が C で ( 2 ) 先行する Bj , Bk から変形規則 (MP) によって引き出された式である。 C の proof が存在するとき , C は Q の theorem である , または C は Q において prov- able ( 証明可能 ) であるといい , ト QC と書くことにする。 0 の公理は AFOL の公理と固有公理をあわせたものだから , C が Q の theorem であるという ことは , これまでの言い方からすれば , Q の固有公理の集合から , C への AFOL における演繹が あるということに他ならない。 Q の theorem の例 本当にこれだけで算術と言えるのかなあ ? 例えば , 「 1 十 1 = 2 」は自然数についての最もかん たんな知識だと思うけど , これは 0 の公理の中にはないみたい。これも 0 から theorem として
2 2 2 第Ⅲ部論理をもう 1 つの目で見る P → (Q → R) と P に→ elim を使うと Q → R が出てくる。そして , Q → R と Q にもういちど→ elim を使うと , あれま , R が出てくるでは ありませんか。 ・・というわけでたいていの演繹は以上の攻略法に従ってやって いけばたいていは自動的にできてしまう。言うまでもないことだが , 自然演繹の推論規則は , 演繹の各行に何を書いてよいか , ある行か ら他の行へ移るときにどのような移り方なら許されるかということ を定めたものであるのに対し , 攻略法はどんな手順で , どのように P Q R 一→ elim Q → R → elim Reit P → (Q → R) Reit Prem → R Prem Q → (P → R) → intro P → R → intro はできるが , 推論規則に従っていない「演繹」は演繹になっていない。 い。したがって , 攻略法に従わなくても正しい演繹を構成すること 推論規則をつかって演繹をつくっていったらよいかのコツにすぎな こでいくつかの用語を定義しておこう。 9.1.6 演繹・定理・証明 、ア 或る条件を満たす対象言語の記号列としての theorem ・ proof と , そうした記号列について こちらの意味での定理をメタ定理 (metatheorem) と呼んで区別することもある。 くつかの補助的な記号 ( とかト爿とか ) を使って示したものがその【証明】なのだ。だから , 号をふって【】にくくって提示してきた【定理】であり , その正しさをメタ言語の日本語とい ヒンティッカ集合は充足可能だといった事実を , メタ言語の日本語で述べたものが , これまで番 どについて現に成り立っているある事実 , 例えばどの論理式もただ一通りにしか読めないとか , およびその終点にある論理式のことだ。これに対し , 論理式の集まり , 論理式と論理式の関係な たがって , ' こで定義した theorem と proof は , ようするに特定の条件を満たす論理式の列 , だ。そして「 theorem 」というのもその列の最後に並んでいる論理式のことを意味している。し こで定義した「 proof 」はある規則 ( つまり推論規則 ) に従って並んでいる論理式の列のこと 全く異なる概念だから , その 2 つを混同してはならない。 た。ところが , これまで使ってきた【定理】とここで定義した「定理」っまり「 theorem 」とは これまでも , 【定理 35 】とその【証明】というような形で , すでにこれら 2 つの言葉を使ってき こで非常に大切な注意がある。いま , 「定理」と「証明」という言葉が定義された。しかし 式を theorem ( 定理 ) と言い , その演繹を proof ( 証明 ) と言う。 がいかなる前提もおかずに演繹できたことを示している。こうした前提のない演繹がある ( 2 ) 練習問題 64 のように , 一番左の導出線に前提棒のない演繹がある。これは P → ( Q → P ) き , それを AI , ・ (n) と言う。 ・ An からの B の演繹 (deduction of B from AI, ( 1 ) AI, ・・・ , An からの B の導出があって , それが他のいかなる導出にも依存していないと 【定義】
304 第Ⅳ部論理学はここから先が面白い ! 練習問題 91 進んだ話題のロードマップ ( 1 ) 排中律 P ▽ P は直観主義的に妥当でないことを証明せよ。 ( 2 ) P →ー 1 ー IP が直観主義的に妥当であることを証明せよ。 このあとの展開は ? 直観主義論理の公理系 ( 自然演繹 N のとセマンティクスを導入した。 べきこととしては次のような 2 つの課題が思い浮かぶ。 このあとにすぐにやる ( 1 ) 直観主義論理の完全性証明 : 直観主義論理に関しても , NJ の theorem の集合と直観主義 的に妥当な式の集合とが一致し , さらに , 「論理式の集合から C への NJ における deduction がある論理式 C が論理式の集合から直観主義的・意味論的に帰結する」という完全性 が成り立つだろうか ? これは成り立っことが証明できる。というより , クリプキは完全性を証明するために直観主義 論理にセマンティクスを与えたのだった。 完全性が証明できれば , どんなにがんばって工夫しても排中律は N 」で決して provable でな いということの厳密な証明ができる。排中律は直観主義的に妥当でないから ( このことはすでに 練習問題 91 ( 1 ) で示した ) , それは NJ の theorem ではない。 ( 2 ) 直観主義論理の決定手続き : 古典命題論理にはタブローという機械的な決定手続きがあっ た。直観主義命題論理にも同じように , 任意の論理式が直観主義的に妥当であるかないかを有限 のステップで教えてくれるようなアルゴリズムがある。認識史分析という名前の方法で , タブ ローと同様非常にわかりやすい。興味のある読者は , 野矢茂樹 [ 1994 ] や大出晃 [ 1991 ] を見て みよう。 11. 4 11.4.1 古典論理の拡張としての様相論理 古典論理への代替案か古典論理の拡張か 古典論理にはたくさんの公理系がある。しかし , APL にせよ ND にせよ , そこから theorem として出てくる論理式の範囲は全く同じ , というわけで両方とも 1 つの同じ古典論理の公理系で ある。そこで , 論理のアイデンティティを , provable な式の集まりと同一視してみたらどうか。 この集まりが同じであれば , どのような仕方で公理化されていても同じ論理とみなすことにする のだ。この意味で APL と N D は見かけは異なるが同じ論理の体系ということになる。 一方 , これまでに非古典論理の代表として扱ってきた直観主義論理は , 古典論理で論理的真理 とされていたもののうちいくつかが論理的真理とみなされないという特徴があった。排中律がそ の代表だ。そして実際に , 古典論理 ND の theorem の範囲と , 直観主義論理 NJ の theorem の 範囲とは食い違っている ( 後者は前者の一部にすぎない ) 。だから , 直観主義論理と古典論理は異
258 ( 2 ) ( 4 ) ( 5 ) ( 6 ) ( 7 ) ⑧ ⑨ ⑩ ( 11 ) 第Ⅲ部論理をもう 1 つの目で見る ( P → P ) → ( ( P → P ) → P ) P → ( P → P ( P → P ) → P ・ P ( ( P P) ( P ( ( P P) P P ) ) → ( ( P →い P → P ) ) → P ・ P → P P → ( P → P ) ・ ( P → ( P → P ) ) → ( P → P ) ・ ・・・仮定 ・・・ A 1 ・・・ ( 1X3 ) MP ・・・ ( 2X4 ) MP ・・・ A 1 ・・・ ( 6X7 ) MP ・・・ A 1 ・・・ ( 8X9 ) MP ・・・ ( 5X10 ) MP うまくいった。演繹定理によれば P → P に proof があることがわかった ( 上の式の列じた いは P → P の proof ではないよ ) 。そこで P → P を theorem 6 と名づけよう。ところで上 の deduction をよく見ていると , ( 6 ) から⑩までのところは , 一番最初に示した P → P の proof の 「 P 」のところを「 P 」に置き換えてもう一度繰り返しているにすぎないことがわかる。これは いかにも無駄じゃなかろうか。そこで , これまでに proof があることがわかっている theorem は , 公理と同じように deduction や proof において自由に使ってよいことにしよう。さらに , P → P の proof がいったんなされていれば , その proof で「 P 」が出てくるところをいっせいに 「 ( Q → R ) 」に置き換えれば ( Q → R ) → ( Q → R ) の proof としてそのまま使えるわけだから , 一度 proof があることが示された theorem は , そのあとは図式として使ってよいということに なる。こうして , 次のように deduction をはしよることができる。 ( 2 ) ( 4 ) ( 5 ) ( 6 ) ( 7 ) い P → P ) → ( ( P → P ) → P ) ・ P → ( P → P ) P → P ( P → P ) → P ・ P → P ・・・ A 3 ・・・ A 1 ・・・ ( 1X3 ) MP ・・・ ( 2X4 ) MP ・・ theorem 1 手を抜かずにちゃんとやれ ! と言われたら , ( 5 ) と ( 6 ) の間に P → P の proof を挿入すればよ 派生規則 いわけだ。 中に P → Q, Q → R, P という 3 つの式が現れているなら , その列に続けて R を書き込んでも , おこう。さてそうすると , 何か他の deduction を構成しようと試みているときに , 論理式の列の 例えば , P → Q, Q → R, P ト R であることがわかったとする。この deduction を D と呼んで
第 10 章シンタクスの視点から論理学のゴールに迫る 257 ト BI である。一方 , A 1 よりト BI → ( A → BI ) である。これらより , 定理 37 の ( 4 ) ( 5 ) によって rh-A → BI ・ Subcase 2 . BI が IA の要素であるとき , ト BI である。 AI よりト BI → ( A → BI ) である。 ・ Subcase 3 . BI が A であるとき , BI これらより , 定理 37 の ( 4X5 ) によって I* ト A → ト A → A である。しかし , BI が A に他ならないのだから , I*F-A → BI 以上より , いずれにせよ→ BI が成立する。 [lnduction step] k<i なるすべての k について , rFA → Bk と仮定する ( 帰納法の仮定 ) 。 この仮定のもとで , I* ト A →となることを証明しよう。 は deduction のなかに現れる式だから , 公理であるか , の要素であるか , A であるか , 先行す る 2 つの式 B 」 , BI ( j , 1 < i ) から MP によって得られた式であるかのいずれかだ。 Subcase 1 ~ 3 . 公理であるか , IÄの要素であるか , A である場合。 CBasis] での証明と全 く同様に I* ト A →であることが言える。残るは , 次の場合のみ。 ・ Subcase 4 . Bi が先行する 2 つの式 b, (j , 1 < i) から MP によって得られた式である場 帰納法の仮定により , ト A → Bj かっ , ト A →である。また , Bj , から MP によって Bi が得られたのだから , が Bj →の形をしているか , Bj が片→の形をしているのでなくて はならない。そこで , かりに前者であるとしよう。このとき , I*h—A → BI と , が Bj →の形をしていることにより , I*k-A → ()j → Bi)0 また , A 2 より , h-(A → ()j → (i)) → ()A → (J) → (A → Bi))O これと rh-A → BJ により これらから定理 37 の ( 4X5 ) によって , rF(A → (J) → (A → (i)0 さらに 定理 37 の ( 5 ) を用いて I* ト A → Bi である。 Bj が片→ Bi の形をしている場合も全く同様。・ ( 2 ) 以下のことがらを示せ。演繹定理を用いてもよい。 ( 1 ) rk-A → C っ I*,AFC を示せ。こちらの方向は簡単。これにより , 演繹定理の証明が完成す 練習問題 78 ( この論理式を theorem 3 と呼ぶ ) (a) F(P → (Q → R)) → (Q → (P → R)) (b) h-(P → (P → Q)) → (P → Q) ( 同様に theorem 4 ) (c) ト ( Q → - ー + ) → ( P → Q ) (theorem 5 ) 10.1.6 deduction 中での theorem の利用と派生規則 一度 proof の存在を示した theo 「 em は図式として使おう 次に 2 重否定則 , ト P → P を示してみよう。演繹定理により , P ト P を示せばよかろ
ここで定義した proof はある条件を満たす論理式の列のこと , theorem はその列の最後にあ る論理式そのもののことだ。だから , これまで【定理 25 】とかその証明と言ってきたように , 論理式の性質について或る事実を日本語で述べたもの , そしてその正しさを示すこととしての定 理や証明とは全く異なるから気をつけてほしい。両方とも同じ「定理」という言葉を使うと紛ら ' こで新しく定義された概念の方は「 proof 」 , 「 theorem 」という語を使っていく わしいので , ことにする。くどいなあ , 自然演繹のところでも同じような注意をしたじゃないか ( 222 ペー ジ ) 。そうである。でもこの区別は本当に重要なんだから何度でも言わせて。 公理からの p 「 00f の例 先ほどの P → P の導出は , APL における proof の条件を満たしている。したがって , p → p は APL の theorem だと言ってよい。そこで , この論理式を theorem 1 と名づけておこう。次にも う少し込み入った proof の例を挙げる。推移律の proof だ。 第 10 章シンタクスの視点から論理学のゴールに迫る おいて provable ( 証明可能 ) であるという。 ()Q → R) → (P → Q)) → ()Q → R) → (P → R)) ・ 251 ( 1 ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) ( 6 ) ( 7 ) ⑧ ⑨ ⑩ 圓 ( 12 ) ( 13 ) ( 14 ) 05 ) (P → (Q → R)) → ()P → Q) → (P → R)) ・ ()P → (Q → R)) → ()P → Q) → (P → R))) → ()Q → R) → ()P → (Q → R)) → ()P → Q) → (P → R)))) ・ ( Q → R ) → ( ( P → ( Q → R ) ) → ( ( P → Q ) → ( P → R ) ) ) ・・ ()Q → R) → ()P → (Q → R)) → ()P → Q) → (P → R)))) → (((Q → R) → ()P → (Q → R)))) → ()Q → R) → ()P → Q) → (P → R)))) ()Q → R) → ()P → (Q → R)) → ()Q → R) → ()P → Q) → (P → R))) (Q → R) → ()P → Q) → (P → R)) ・ (Q → R) → (P → (Q → R)) ・ ()Q → R) → ()P → Q) → (P → R))) → ( ( P → Q ) →巛 Q → R ) → ( P → Q ) ) → ( ( Q → R ) → ( P → R ) ) ) ) → (P → Q) → (((Q → R) → (P → Q)) → ()Q → R) → (P → R))) ・ ()P → Q) →巛 Q → R) → (P → Q)) → ()Q → R) → (P → R)))) ・・ (((Q → R) → (P → Q)) → ()Q → R) → (P → R))) → (((Q → R) → (P → Q)) → ()Q → R) → (P → R))) ・・ ( ( P → Q ) → ( ( ( Q → R ) → ( P → Q ) ) ) → ( ( P → Q ) → ( ( Q → R ) → ( P → R ) ) ) ・・ (((P → Q) → (((Q → R) → (P → Q)))) → ()P → Q) → (((Q → R) → (P → R))))) (P → Q) → ()Q → R) → (P → R)) ・ (P → Q) → ()Q → R) → (P → Q)) ・・・ A 2 ・・・圓 ( 12 ) から MP ・・・ 03X1 のから MP ・・・ A 2 ・・・ A 1 ・・・ ( 1X2 ) から MP ・・・ A 2 ・・・ ( 3X4 ) から MP ・・・ A 1 ・・・ ( 5X6 ) から MP ・・・ ( 7X8 ) から MP ・・・ A 1 ・・・⑨⑩から MP ここに出てくる 15 個のすべての論理式が , 公理か , 先行する 2 つの式から推論規則によって
250 第Ⅲ部論理をもう 1 つの目で見る 公理系 APL (axiomatic system for propositionallogic の略 ) A 1 A → (B → A) A 2 (A → (B → c)) → ()A → B) → (A → c)) A 3 ( B → A ) → ( ( B → A ) → B ) R 1 MP ここにない論理定項は定義 D I—D 3 で導入されるものとする。この公理系の大きな特徴は , 公理そのものが A, B などの図式文字をつかって書かれているということだ。つまり , A 1 はひ とつの論理式ではなく , P → (Q → P), ( P → Q ) → ( R → ( P → Q ) ) , (P → (Q → P)) →巛 P → Q) → (P → ( p → Q ) ) ) → ( P → ( Q → P ) ) ) など A → (B → A) の形をした無数の論理式を一括して表している。 つまり , A 1 は「しかじかの形をした任意の論理式を公理とします」と言っている。したがっ て , APL は無限に多くの公理をもつ。このようなことから , A 1 から A 3 は公理図式 (axiom schema) と呼ばれることもある。公理図式を使うメリットは , 代入規則がいらなくなるという ことだ。 P → P はトートロジーの 1 つだが APL の公理には含まれていない。ということは , この式も APL のいずれかの公理から推論規則を適用して導かれるはずだ。実際 , 次のように導くことが できる。 ( 1 ) ( 2 ) ( 3 ) ( 4 ) ( 5 ) 10.1.3 P → ()P → P) → P) ・・ (P → ()P → P) → P)) → ()P → (P → P)) → (P → P)) ( P → ( P → P ) ) → ( P → P ) ・・・ P → (P → P) ・ P → P ・ 公理系に関して定義される諸概念 ・・・ A 1 A 2 ・・・ ( 1X2 ) から MP により ・・・ A 1 ・・・ ( 3X4 ) から MP により theorem と proof 公理系 APL に対して , APL での theorem, proof ということを次のように定義する。 【定義】 ( 1 ) 以下の条件を満たす , 論理式の有限個の列 BI, B2, る ) を , C の APL における proof ( 証明 ) という。 [ 条件 ] Bi ( ただし 1 ミ i ミ n ) は , 次のいずれかである。 (a) APL の公理である。 ・ , Bn ( この最後の Bn が C であるとす ( 2 ) (b) 先行する Bj , Bk から推論規則 MP によって引き出された式である。 C の proof が存在するとき , C は APL の theorem ( 定理 ) である , または C は APL に