[2026前期火５] 論理学（京都大学文学部 前期 第8回）「正規化定理の証明」

科学哲学科学史 (演習) 前期 第8回　論理学　（京都大学文学部・矢田部俊介）
「正規化定理の証明」
2026年6月9日（火）1645〜1815（予定）

Transcript

1. Պֶ఩ֶՊֶ࢙ (ԋश) લظ ୈ 8 ճ ࿦ཧֶ ਖ਼نԽఆཧͷূ໌ ݟఢඞࡴɾఀࢭੑɾ࿦ཧͷ఩ֶ΁ 2026 ೥ 6 ݄ 9 ೔ʢՐʣ16:45–18:15 จֶ෦ୈ 4 ߨٛࣨ ୲౰ɿ໼ా෦ढ़հʢ੢೔ຊཱྀ٬మಓגࣜձࣾʣ yatabe.shunsuke.24n@st.kyoto-u.ac.jp
2. ຊ೔ͷ಺༰ Section 0ɿલճ͓͞Β͍ ূ໌थͷ͔ͨͪʢ༿ɾࠜɾV ࣈܕʣ detour ͱਖ਼نͳূ໌ ਖ਼نԽఆཧͷओுʢલճʣ Section 1ɿࠓ೔ͷํ਑ͱجຊઓུ ΞϑΟϯ࿦ཧͰূ໌͢Δ جຊઓུɿݟఢඞࡴ Section 2ɿ֤݁߹ࢠͷ detour আڈ → ͷ৔߹ ∧ ͷ৔߹ ∨ ͷ৔߹ Section 3ɿఀࢭੑͷূ໌ ΞϑΟϯ࿦ཧͰͷఀࢭੑ ༗ݶճͰਖ਼نܗʹ౸ୡ͢Δ Section 4ɿॖ໿͕͋Δͱ೉͍͠ ূ໌ͷෳ੡ͱࢦ਺తരൃ ʮӅΕͨճΓಓʯ໰୊ʢผ໰୊ʣ Section 5ɿਖ਼نԽఆཧͷ஥ؒͨͪ ऑਖ਼نԽɾڧਖ਼نԽ Χοτআڈఆཧ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 2
3. Section 0ɿલճ͓͞Β͍ŠŠূ໌थͷ͔ͨͪʢ Vࣈܕʣ ূ໌थͷ 3 ཁૉ ༿ ʢ্ʣ ɿԾఆ [u:A]ʢΩϟϯηϧࡁʣ ΍ AʢະΩϟϯηϧʣ ಺෦ϊʔυɿਪ࿦نଇͷద༻ ࠜʢԼʣɿ݁࿦ ਖ਼نͳূ໌ͷ V ࣈܕߏ଄ ্൒෼ʢআڈنଇʣ ԾఆΛ෼ղɾ৘ใΛऔΓग़͢ ⇓ V ࣈͷఈʢ࠷খͷ໋୊ʣ ⇓ Լ൒෼ʢಋೖنଇʣ ݁࿦Λ૊ΈཱͯΔ ྫɿA ∧ (A → B) → B ͷਖ਼نͳূ໌ [u:A ∧ (A → B)] ∧−L A [u:A ∧ (A → B)] ∧−R A → B →− B →+u A ∧ (A → B) → B ্ɿ∧EL ɾ∧ER ɾ→Eʢআڈنଇʣ Լɿ→Iʢಋೖنଇʣˡ V ࣈͷఈ͔Β૊Έཱͯ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 3
4. Section 0ɿલճ͓͞Β͍ŠŠ detour ͱਖ਼نͳূ໌ detourʢճΓಓʣͷྫɿ∧ ͷ৔߹ ʮA ͱ B Λ·ͱΊͯʢ∧Iʣ͙͢ A ͚ͩऔΓग़ ͢ʢ∧EL ʣ ʯ A B ∧+ A ∧ B ∧−L A A ∧ B Λܦ༝͢Δͷ͸ʮճΓಓʯ ௚઀ A ͔Β A ͰΑ͍ 3 छྨͷ detour →I ͷ௚ޙʹ →E ʢA → B ͕ๆʣ ∧I ͷ௚ޙʹ ∧E ʢA ∧ B ͕ๆʣ ∨I ͷ௚ޙʹ ∨E ʢA ∨ B ͕ๆʣ detour ͷڞ௨ύλʔϯ . . . ඞཁͳ΋ͷ I نଇ A ◦ Bʢๆʣ E نଇ औΓग़͢΋ͷ ࡞͙ͬͯ͢յ͢ʹ detour ਖ਼نͳূ໌ɾਖ਼نԽఆཧ ਖ਼نͳূ໌ɿdetour Λؚ·ͳ͍ূ໌ ਖ਼نԽఆཧʢલճओுͷΈʣ ɿ ೚ҙͷূ໌͸ਖ਼نͳূ໌ʹม׵Ͱ ͖Δ ˠ ࠓ೔͜ΕΛূ໌͢Δ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 4
5. Section 1ɿࠓ೔ͷํ਑ŠŠΞϑΟϯ࿦ཧͰਖ਼نԽ͢Δ ࠷খ໋୊࿦ཧ vs ΞϑΟϯ࿦ཧ ࠷খ໋୊࿦ཧ ॖ໿نଇ͋Γ ΞϑΟϯ࿦ཧ ॖ໿نଇͳ͠ ॖ໿نଇʹಉ͡લఏΛෳ਺ճ࢖͑Δ proof net ͰͷʮY ࣈϊʔυʯ ΞϑΟϯ࿦ཧͷಛ௃ ֤લఏ͸ͪΐ͏Ͳ 1 ճ͔͠࢖͑ͳ͍ proof net ʹʮY ࣈϊʔυʯ͕ग़ͯ͜ͳ͍ ֤ϫΠϠ͕ 1 ຊͷ··ྲྀΕΔ ͳͥΞϑΟϯ࿦ཧͰূ໌͢Δͷ͔ ূ໌͕γϯϓϧʹͳΔ ఀࢭੑͷٞ࿦͕໌֬ ॖ໿͕͋Δͱূ໌ͷෳ੡͕ى͖ɺ ࢦ਺తʹূ໌͕๲ΒΉ ʢSection 4 Ͱৄ͘͠ʣ ࠓ೔ͷূ໌ͷର৅ ΞϑΟϯ໋୊࿦ཧ ʢ→, ∧, ∨ ͷ 7 نଇ͔Β ॖ໿نଇΛআ͍ͨମܥʣ ͜ͷମܥͰ΋ਖ਼نԽఆཧ͕੒ཱ͢Δɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 5
6. Section 1ɿਖ਼نԽఆཧ͸ϝλఆཧ ਖ਼نԽఆཧ͸ϝλͷఆཧ ਖ਼نԽఆཧ͸ʮ໋୊࿦ཧͷఆཧʯͰ͸ͳ͘ɺ ূ໌࿦ͷϝλఆཧͰ͋Δɻ ର৅ݴޠʢobject languageʣ ɿ ໋୊ A, B, A → B, . . . ͷੈք ϝλݴޠʢmeta languageʣ ɿ ূ໌ਤͷߏ଄ʹ͍ͭͯޠΔݴޠ ʮ೚ҙͷূ໌ਤ π ͸ਖ਼نܗʹม׵Ͱ͖Δʯ ͸ର৅ݴޠͷ໋୊Ͱ͸ͳ͍ɻ ূ໌ਤͦͷ΋ͷʹ͍ͭͯͷओுɻ Կʹର͢Δؼೲ๏͔ detour ਺ɿূ໌ਤʹؚ·ΕΔ detour ͷݸ਺ɻ ྫʣ∧I ௚ޙʹ ∧E ͕ 2 Օॴ ˠ detour ਺ = 2 ͜ΕΛܭଌྔͱͯ͠ؼೲ๏Λճ͢ɿ detour ਺ = 0ɿ͢Ͱʹਖ਼نܗ ✓ detour ਺ = n + 1ɿ 1 ճؐݩ ˠ detour ਺͕ n ҎԼʹ ͳΔ ˠ ؼೲ๏ͷԾఆΛద༻ ΞϑΟϯ࿦ཧͰ͸ʮؐݩͰ detour ਺͕୯ௐʹ ݮΔʯ ͕อূ͞ΕΔʢSection 3 Ͱূ໌ʣ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 6
7. Section 1ɿجຊઓུŠŠݟఢඞࡴʢ Search and Destroyʣ جຊઓུͷ 3 εςοϓ 1. αʔνɿূ໌ͷதΛ͘·ͳ͘୳͠ɺ detourʢI ϊʔυͱ E ϊʔυͷྡ઀ʣΛݟͭ ͚Δ 2. σετϩΠɿݟ͚ͭͨ detour Λ ʮؐݩૢ࡞ʯͰফڈ͢Δ ʢdetour Λؚ·ͳ͍ূ໌ʹม׵ʣ 3. ܁Γฦ͠ɿdetour ͕࢒͍ͬͯΕ͹ εςοϓ 1 ʹ໭Δ ֤݁߹ࢠʹ͍ͭͯʮͲ͏ؐݩ͢Δ͔ʯΛ࣍ͷ Section 2 Ͱ֬ೝ͢Δɻ ؐݩͱ͸Կ͔ detour ෦෼ΛʮΧοτ&ϖʔε τʯͰ ΑΓ୹͍ূ໌ʹஔ͖׵͑Δ͜ͱɻ ূ໌ πʢdetour ͋Γʣ ؐݩ ূ໌ π′ʢdetour1 ݸݮʣ ΞϑΟϯ࿦ཧͰ͸ 1 ճͷؐݩͰ detour ͕ݫີʹ 1 ݸݮΔɻ ʢSection 3 Ͱূ໌ʣ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 7
8. Section 2ɿ→ ͷdetourআڈ → ͷ detourŠŠ I ϊʔυͱ E ϊʔυ͕ྡ઀ →I Ͱ A → B Λ࡞Γɺ௚ޙʹ →E Ͱ B ΛऔΓग़͢ɻ ؐݩલʢdetour ͋Γʣ [u:A] π1 B →+u A → B π2 A →− B A → B ͕ detour ͷʮๆʯ ⇒ ؐݩޙʢdetour ͳ͠ʣ π2 A π1 [π2 /u] B π1 ͷதͷ [u:A] Λ π2 ʢA ͷূ໌ʣͰஔ͖׵͑ ϙΠϯτ A → B ͱ →Iɾ→E ͷ྆ϊʔυ͕ফ͑Δɻ π1[π2/u] ʹ π1 தͷԾఆ [u:A] Λ π2 Ͱஔ͖׵͑ͨূ໌ɻ ΞϑΟϯ࿦ཧͰ͸ u ͸ 1 ճ͔͠ग़ͯ͜ͳ͍ͨΊɺπ2 Λෳ੡͠ͳ͍ɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 8
9. Section 2ɿ∧ ͷdetourআڈ ∧ ͷ detourŠŠ I ϊʔυͱ E ϊʔυ͕ྡ઀ ∧I Ͱ A ∧ B Λ࡞Γɺ௚ޙʹ ∧EL Ͱ A ͚ͩऔΓग़͢ɻ ؐݩલʢdetour ͋Γʣ π1 A π2 B ∧+ A ∧ B ∧−L A A ∧ B ͕ detour ͷʮๆʯ ʢ∧ER ͷ৔߹΋ରশతʹಉ༷ʣ ⇒ ؐݩޙʢdetour ͳ͠ʣ π1 A π1 ʢA ͷূ໌ʣ͚͕ͩ࢒Δ π2 ʢB ͷূ໌ʣ͸ফ͑Δ ϙΠϯτ A ∧ Bɾ∧Iɾ∧E ͷશ͕ͯফ͑Δɻ ࢖Θͳ͔ͬͨ π2 ʢB ͷূ໌ʣ͸ʮࡍʹ͸ෆཁͩͬͨʯ͜ͱʹͳΔɻ proof net Ͱ͸ B ͷϫΠϠ͕ dangling wireʢߦ͖৔ΛࣦͬͨϫΠϠʣʹͳΔɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 9
10. Section 2ɿ∨ ͷdetourআڈ ∨ ͷ detourŠŠ I ϊʔυͱ E ϊʔυ͕ྡ઀ ∨IL Ͱ A ∨ B Λ࡞Γɺ௚ޙʹ ∨E Ͱ৔߹෼͚͢Δɻ ؐݩલʢdetour ͋Γʣ π1 A ∨+L A ∨ B [u:A] π2 C [v:B] π3 C ∨−[u, v] C A ∨ B ͕ detour ͷʮๆʯ ࠨࢬɿ[u:A] Λ࢖͏ π2 ɺӈࢬɿ[v:B] Λ࢖͏ π3 ⇒ ؐݩޙʢdetour ͳ͠ʣ π1 A π2 [π1 /u] C ࠨࢬ͕ੜ͖࢒Δ π2 தͷ [u:A] Λ π1 Ͱஔ͖׵͑ ӈࢬ π3 ͸ফ͑Δ ϙΠϯτ ∨IL Ͱʮࠨ͔Βདྷͨʯͱ͍͏৘ใ͕อ࣋͞Ε͍ͯΔͨΊɺࠨࢬ π2 ͕ੜ͖࢒Δɻ ∨IR ͔Βདྷͨ৔߹͸ӈࢬ π3 ͕ੜ͖࢒Δʢରশతʣ ɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 10
11. Section 2ɿؐݩૢ࡞ͷ·ͱΊ 3 छྨͷؐݩʢΞϑΟϯ࿦ཧͰͷ detour আڈʣ ݁߹ࢠ ؐݩલͷܗ ؐݩޙ ফ͑Δ΋ͷ → →I ௚ޙʹ →E π1 [π2 /u] A → Bɺ→Iɺ→E ∧ ∧I ௚ޙʹ ∧EL π1 ʢA ͷূ໌ʣ A ∧ Bɺ∧Iɺ∧EL ɺπ2 ∨ ∨IL ௚ޙʹ ∨E π2 [π1 /u] A ∨ Bɺ∨IL ɺ∨Eɺπ3 ڞ௨ύλʔϯ I-ϊʔυͱ E-ϊʔυͷ྆ํ͕ফ͑Δ ʮ࣮ࡍʹ࢖ͬͨʯূ໌͕࢒Δ ʮ࢖Θͳ͔ͬͨʯূ໌͸ফ͑Δ proof net ͰݟΔͱ I ϊʔυͱ E ϊʔυ͕ ʮ୹བྷʯ ͯ͠ফ͑Δ ࢖ͬͨϫΠϠ͸௚௨ ࢖Θͳ͔ͬͨϫΠϠ͸ dangling Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 11
12. Section 3ɿఀࢭੑͷূ໌ŠŠΞϑΟϯ࿦ཧ൛ ఀࢭੑͷূ໌ͷུ֓ 1. ূ໌ π ͷ detour ͷ૯਺Λ n ͱ͓͘ɻ ʢn ͸༗ݶɿূ໌ਤ͸༗ݶʣ 2. ΞϑΟϯ࿦ཧͰ͸֤ϥϕϧ u ͸ ͪΐ͏Ͳ 1 ճ͔͠ग़ͯ͜ͳ͍ɻ 3. π1 [π2 /u] Λ࡞Δͱ͖ π2 Λ ෳ੡͠ͳ͍ʢu ͸ 1 ՕॴͷΈʣ ɻ 4. 1 ճͷؐݩͰ detour ૯਺͕ ݫີʹ n − 1 ҎԼʹͳΔɻ 5. ߴʑ n ճͰਖ਼نܗʹ౸ୡɻ □ ఆཧʢΞϑΟϯ࿦ཧ൛ਖ਼نԽఆཧʣ ΞϑΟϯ໋୊࿦ཧͷ೚ҙͷূ໌͸ɺ ༗ݶճͷؐݩૢ࡞ʹΑͬͯ ਖ਼نܗʹ౸ୡ͢Δɻ ূ໌ͷϙΠϯτ ֤ؐݩͰ detour ਺͕ݮΔ ॖ໿ͳ͠ ˠ ෳ੡ͳ͠ detour ਺͸༗ݶ ূ໌ਤ͸༗ݶ ͕ͨͬͯ͠ඞͣఀࢭ͢Δ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 12
13. Section 3ɿఀࢭੑͷΠϝʔδ ʮdetour ਺ʯͱ͍͏ܭଌث ֤ؐݩ: detour ਺͕ n → n−1 ʹݮΔ n ͸༗ݶʢূ໌͸༗ݶαΠζʣ ∴ ߴʑ n εςοϓͰਖ਼نܗ π0 ʢdetour n ݸʣ ؐݩ π1 ʢdetour n − 1 ݸʣ ؐݩ . . . ؐݩ πn ʢdetour 0 ݸʣʹਖ਼نܗ ͳͥʮΞϑΟϯʯ͕ॏཁ͔ ॖ໿͋Γͷ৔߹ɿ π1 [π2 /u] Ͱ u ͕ෳ਺ճग़ͯ͘Δ ˠ π2 Λෳ੡͠ͳ͚Ε͹ͳΒͳ͍ ˠ ෳ੡͞Εͨ π2 ͷதʹ ৽͍͠ detour ͕ੜ·ΕΔՄೳੑ ˠ detour ਺͕૿͑Δ͜ͱ͕͋Δʂ ΞϑΟϯͷ৔߹ɿ u ͸ 1 ճ͔͠ग़ͯ͜ͳ͍ ˠ ෳ੡ͳ͠ ˠ detour ਺͸୯ௐݮগ ˠ ఀࢭੑ͕໌֬ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 13
14. Section 4ɿॖ໿نଇ͕͋Δͱ೉͍͠ ॖ໿نଇ͋Γͷ৔߹ͷ໰୊ →I ͷΩϟϯηϧϥϕϧ u ͕ෳ਺ճग़ͯ͘Δ͜ ͱ͕͋Δ ʢproof net ͷ Y ࣈϊʔυʣ ɻ ͜ͷͱ͖ π1 [π2 /u] Λ࡞Δͱɿ π2 Λෳ੡͢Δඞཁ͕͋Δ ෳ੡ͨ͠ π2 ͷதʹ detour ͕͋Δͱ ˠ ৽͍͠ detour ͕૿͑Δʂ ʮ1 ݸফͯ͠ 2 ݸ૿͑Δʯ͕܁Γฦ͞ΕΔ ˠ detour ਺͕୯ௐʹݮΒͳ͍ ࠷ѱέʔεɿࢦ਺తരൃ n ݸͷॖ໿Λ࣋ͭূ໌Λਖ਼نԽ͢Δͱɺ ূ໌ͷαΠζ͕ 2n Φʔμʔʹ ͳΓ͏Δ͜ͱ͕஌ΒΕ͍ͯΔɻ ʢ ʮఀࢭ͸͢Δʯ͕ʮαΠζ͕രൃ͢Δʯ ʣ ڧਖ਼نԽͷূ໌ʹ௒ݶؼೲ๏͕ඞཁͳ ཧ༝ ʮͲͷॱ൪Ͱؐݩͯ͠΋ఀࢭ͢Δʯ ʢڧਖ਼نԽʣΛࣔ͢ʹ͸ɺ ୯ͳΔʮdetour ਺ͷݮগʯͰ͸ෆे෼ ΑΓਫ਼ີͳʮdegree measureʯ ʢ௒ݶॱং਺ʹΑΔܭଌʣ͕ඞཁ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 14
15. Section 4ɿ͓·͚ŠŠʮӅΕͨճΓಓʯ໰୊ʢˮ Eݻ༗ʣ ӅΕͨճΓಓͱ͸ʢॖ໿ͱ͸ผͷ໰୊ʣ ∨E نଇ͸ 3 ೖྗͷʮେ͕͔Γͳنଇʯ ɻ ଞͷআڈنଇ͕ ∨E ͷ಺֎ʹ·͕ͨΔͱɺ detour ͕ʮݟͨ໨ʹ͸ݟ͑ͳ͍ʯ͜ͱ͕͋Δɻ ྫɿҎԼͷূ໌ʹ͸ detour ͕ͳ͍ɻ ͔͠͠෦෼࿦ཧࣜݪཧ͕ഁΕ͍ͯΔʂ [u:A] C → D [v:B] C → D π′ A ∨ B ∨−[u, v] C → D π C →− D C → D ͸݁࿦ D ͷ෦෼࿦ཧࣜͰͳ͍ ˠ ෦෼࿦ཧࣜݪཧ͕ ഁΕ͍ͯΔ ղܾࡦɿॱ൪มߋʢcommuting conversionʣ ∨E ͱ →E ͷॱ൪ΛೖΕସ͑Δͱ ӅΕͨճΓಓ͕ݦࡏԽ͢Δɿ π′ A ∨ B [u:A] C → D π C →− D [v:B] C → D π C →− D ∨−[u, v] D ˠ ∨E ͷ಺෦ʹ → ͷ detour ͕ग़ݱ ˠ جຊઓུͰআڈ Մೳ ·ͱΊ ӅΕͨճΓಓ͸ॖ໿ͷ͍ͤͰ͸ͳ͍ ∨E نଇͷʮ3 ೖྗʯߏ଄ʹݻ༗ͷ໰୊ ॱ൪มߋ ˠ جຊઓུͷ 2 εςοϓͰղܾ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 15
16. Section 5ɿਖ਼نԽఆཧͷ஥ؒͨͪᶃŠŠऑɾڧਖ਼نԽ ऑ͍ਖ਼نԽఆཧʢweak normalizationʣ ೚ҙͷূ໌ π ʹରͯ͠ɺ π ͔Βਖ਼نܗʹ౸ୡͰ͖Δ ؐݩྻ͕গͳ͘ͱ΋ 1 ͭଘࡏ͢Δɻ ʮ͏·͘΍Ε͹ਖ਼نܗʹ୧Γண͚Δʯ ˠ ࠓ೔ΞϑΟϯ࿦ཧͰূ໌ͨ͠ͷ͸͜Εɻ ڧ͍ਖ਼نԽఆཧʢstrong normalizationʣ ೚ҙͷূ໌ π ʹରͯ͠ɺ detour আڈΛͲͷॱ൪Ͱߦͬͯ΋ɺ ඞͣ༗ݶεςοϓͰਖ਼نܗʹ౸ୡ͢Δɻ ʮͲΜͳॱ൪Ͱ΍ͬͯ΋ඞͣऴΘΔʯ લճ Q&AʢQ3ʣͷ౴͑ ʮεϥΠυͷਖ਼نԽఆཧ͕ωοτͰݟΔ ΋ͷͱҧ͏ʯ ˠ ऑਖ਼نԽͷόʔδϣϯ ʢڧਖ਼نԽΑΓऑ͍ओுʣ ඪ४తͳڭՊॻʢPrawitz ౳ʣͰ͸ ڧਖ਼نԽΛओு͢Δ͜ͱ͕ଟ͍ɻ ڧ͞ͷॱং ڧਖ਼نԽ ⇒ ऑਖ਼نԽ ʢٯ͸Ұൠʹ͸੒ཱ͠ͳ͍ʣ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 16
17. Section 5ɿਖ਼نԽఆཧͷ஥ؒͨͪᶄŠŠΧοτআڈఆཧ ਪ݅ܭࢉʢsequent calculusʣ ࣗવԋ៷ͱ͸ผͷূ໌࿦ͷܗࣜԽɻ 1930 ೥୅ʹήϯπΣϯ͕ಋೖɻ ࣗવԋ៷ɿԾఆ͔Β݁࿦ΛੵΈ্͛Δ ਪ݅ܭࢉɿલ݅ʢલఏͷू߹ʣͱ ޙ݅ʢ݁࿦ͷू߹ʣΛʮ⊢ʯͰͭͳ͙ Χοτنଇ ਪ݅ܭࢉʹ͓͚Δʮத໋ؒ୊Λܦ༝͢Δਪ࿦ʯ ɿ Γ ⊢ A A, ∆ ⊢ C Γ, ∆ ⊢ C (cut) ࣗવԋ៷ͷ detour ʹରԠ͢Δɻ ήϯπΣϯͷΧοτআڈఆཧʢHauptsatzʣ ਪ݅ܭࢉʹ͓͍ͯɺ ΧοτنଇΛ࢖Θͣʹ ূ໌Ͱ͖Δ΋ͷ͸ɺ ΧοτΛ࢖ͬͯ΋ূ໌Ͱ͖Δɻ ʢ ʮΧοτ͸ূ໌ͷೳྗΛ૿΍͞ͳ͍ʯ ʣ ରԠؔ܎ ࣗવԋ៷ ਪ݅ܭࢉ detour Χοτʢcutʣ ਖ਼نԽ Χοτআڈ ਖ਼نԽఆཧ Hauptsatz Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 17
18. Section 5ɿਖ਼نԽఆཧͷ஥ؒͨͪᶅŠŠ෦෼࿦ཧࣜݪཧ ਖ਼نԽ ˠ ෦෼࿦ཧࣜݪཧ ਖ਼نͳূ໌ʢdetour ͳ͠ʣͰ͸ɺ ূ໌ʹݱΕΔશͯͷ࿦ཧࣜ͸ ݁࿦·ͨ͸։͍ͨԾఆͷ෦෼࿦ཧࣜɻ ূ໌ͷϙΠϯτɿ ֤ؐݩͰʮๆʯͷ࿦ཧ͕ࣜফ͑Δ ਖ਼نܗͰ͸ʮๆʯ͕θϩ ༨ܭͳதؒ࿦ཧ͕ࣜଘࡏ͠ͳ͍ ˠ ෦෼࿦ཧࣜݪཧ͕ࣗಈతʹ੒ཱ ࠓ೔ূ໌ͨ͜͠ͱͷશମ૾ ೚ҙͷূ໌ π ݟఢඞࡴ ʢ༗ݶճʣ ਖ਼نͳূ໌ π′ ࣗಈతʹ ෦෼࿦ཧࣜݪཧ ݹయ࿦ཧͰ͸ʁ ݹయ࿦ཧʢഉத཯ΛؚΉʣͰ͸ ෦෼࿦ཧࣜݪཧ͕Ұൠʹ੒ཱ͠ͳ͍ɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 18
19. ԋश໰୊ ࠓ೔ͷԋशͷςʔϚ ਖ਼نԽૢ࡞Λࣗ෼ͷखͰ΍ͬͯΈΔɻ ূ໌ʹؚ·ΕΔ detour Λݟ͚ͭΔ ରԠ͢Δؐݩૢ࡞Λద༻͢Δ ਖ਼نܗʢdetour ͳ͠ʣͷূ໌ΛಘΔ ໰ 1ʢඞमʣ ҎԼͷূ໌ʹؚ·ΕΔ detour Λશͯڍ͛ɺ ਖ਼نԽͤΑʢਖ਼نͳূ໌Λ࡞Εʣ ɻ A B ∧+ A ∧ B ∧−L A A B ∧+ A ∧ B ∧−R B ∧+ A ∧ B ໰ 2ʢඞमʣ ҎԼͷূ໌Λਖ਼نԽͤΑɻ [u:A → B] [v:A] →− B →+v A → B [w:A] →− B →+w A → B →+u (A → B) → (A → B) Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 19
20. ԋश໰୊ʢଓ͖ʣ ໰ 3ʢඞमʣ ٯࢉ๏Λ࢖ͬͯҎԼͷਖ਼نͳূ໌Λ࡞Εɻ A ∧ (A → B) → B ώϯτɿԾఆ͔ΒԿΛऔΓग़ͤΔ͔ߟ͑Αɻ ໰ 4ʢඞमʣ ࠷খ໋୊࿦ཧʢॖ໿نଇ͋ΓʣͰ A → A ∧ A Λূ໌ͤΑɻ ώϯτɿॖ໿نଇͰ͸ಉ͡લఏΛ ෳ਺ճ࢖͑Δʢproof net ͷ Y ࣈʣ ɻ [u:A] ΛԿճ࢖͏͔ʁ νϟϨϯδ໰୊ʢՃ఺ɾ೚ҙʣ ҎԼͷূ໌Λਖ਼نԽͤΑɻ ∨ ͷ detour আڈΛؚΉɻ [u:A] ∨+L A ∨ A [v:A] [w:A] ∨−[v, w] A →+u A → A ∨IL ͷ௚ޙʹ ∨E ͕དྷ͍ͯΔʢdetourʣ ɻ ਖ਼نԽ͢ΔͱԿʹͳΔ͔ʁ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 20
21. ਖ਼نԽఆཧͷҙຯŠŠδϥʔϧͷಎ࡯ ਖ਼نԽఆཧ͸ʮ୯ͳΔٕज़తศٓʯͰ͸ͳ͍ Jean-Yves Girardʢઢܗ࿦ཧͷ૑࢝ऀʣʹΑΕ͹ɺ ਖ਼نԽఆཧ͸࿦ཧʹͱͬͯຊ࣭తʹॏཁɻ ͳ͔ͥʁ ਖ਼نͳূ໌ ʹ ΧϊχΧϧͳূ໌ ࿦ཧతਪ࿦ͷʮਅͷ࢟ʯ ෦෼࿦ཧࣜݪཧɿ ূ໌͸݁࿦ͷҙຯͷൣғ಺Ͱಈ͘ ʮ༨ܭͳ΋ͷΛ࣋ͪࠐ·ͳ͍ূ໌ʯ ٯʹɿ෦෼࿦ཧࣜݪཧΛഁΔ࿦ཧମܥ͸ Կ͔͕͓͔͍͠ʢݹయ࿦ཧ͸Ͳ͏ʁʣ ಋೖنଇͱআڈنଇͷʮௐ࿨ʯ ಋೖنଇɿ݁߹ࢠʹҙຯΛ༩͑Δ ʮA ∧ B Λূ໌͢Δͱ͸ A ͱ B Λ ূ໌͢Δ͜ͱʯ আڈنଇɿͦͷҙຯΛ࢖͏ ʮA ∧ B ͔Β A ΛऔΓग़ͤΔʯ detour ͕আڈͰ͖Δ ʹ ಋೖͱআڈ͕ʮௐ࿨͍ͯ͠Δʯ ఩ֶతؚҙ ࿦ཧ݁߹ࢠͷҙຯ͸ਪ࿦نଇ͕ܾΊΔ ʢinferentialismɿਪ࿦ओٛʣ ͔͠͠ʮͲΜͳنଇͰ΋Α͍ʯͷ͔ʁ ˠ ࣍ճͷ࿦ཧֶͷ఩ֶ΁ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 21
22. ࣍ճʢୈ9ճɿ6/16ʣͷ༧ࠂŠŠ࿦ཧֶͷ఩ֶ ୈ 9 ճɿ࿦ཧֶͷ఩ֶ ਪ࿦ओٛʢinferentialismʣೖ໳ ࿦ཧޠͷҙຯ͸ਪ࿦نଇʹΑܾͬͯ·Δ ŠŠͰ͸ͲΜͳنଇͰ΋ʮ࿦ཧʯʹͳΕΔͷ͔ʁ Arthur Priorʢ1960ʣͷ Tonk ͷྫ ಋೖنଇ ʴ আڈنଇΛউखʹઃఆ͢Δͱ ԿͰ΋ূ໌Ͱ͖ͯ͠·͏ʂ ʮྑ͍ʯਪ࿦نଇͷ৚݅͸Կ͔ ʢௐ࿨ɾอकੑɾਖ਼نԽʣ μϝοτʢDummettʣͷҙຯ࿦ ͱ proof-theoretic semantics Tonk ͷϓϨϏϡʔ Prior (1960) ͕ఏҊͨ݁͠߹ࢠ Tonkɿ ಋೖنଇ A A Tonk B আڈنଇ A Tonk B B ͜ΕΛ࢖͏ͱ೚ҙͷ A, B ʹ͍ͭͯ A ⊢ B ͕ূ໌Ͱ͖ͯ͠·͏ɻ ˠ ਖ਼نԽͰ͖ͳ͍ʢdetour ͕ফͤͳ͍ʣ ˠ ʮ࿦ཧʯͱͯ͠ෆద֨ ॓୊ ໰ 1ʙ໰ 4 ͷ͏ͪղ͚ͳ͔ͬͨ΋ͷΛ ୈ 9 ճલ·Ͱʹ KULMS ͷʮ՝୊ʯ͔Βఏग़ɻ ղ͘ͷʹ͔͔ͬͨ࣌ؒΛهೖ͢Δ͜ͱɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 22