[2026前期火５] 論理学（京都大学文学部 前期 第4回）「 ならば（→）の導入と証明ネット」

科学哲学科学史 (演習) 前期 第1回　論理学　（京都大学文学部・矢田部俊介）
「ならば（→）の導入と証明ネット」
2026年5月12日（火）1645〜1815（予定）

Transcript

1. Պֶ఩ֶՊֶ࢙ (ԋश) લظ ୈ 4 ճ ࿦ཧֶ ͳΒ͹ͷಋೖͱূ໌ωοτ → ͷਪ࿦نଇɾproof net ೖ໳ 2026 ೥ 5 ݄ 12 ೔ʢՐʣ16:45–18:15 จֶ෦ୈ 4 ߨٛࣨ ୲౰ɿ໼ా෦ढ़հʢ੢೔ຊཱྀ٬మಓגࣜձࣾʣ yatabe.shunsuke.24n@st.kyoto-u.ac.jp
2. ຊ೔ͷϝχϡʔ 0. લճͷ͓͞Β͍ 1. ॓୊ͷ౴͑߹Θͤɾจͷఆٛͷվగ 2. ͳΒ͹ʢ→ʣͷਪ࿦نଇ 3. ূ໌ωοτʢproof netʣೖ໳ 4. ԋश໰୊ 5. ॓୊ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 2
3. ຊतۀ͸੢೔ຊཱྀ٬మಓגࣜձࣾͷۀ຿ͱ࣮ͯ͠ࢪ͍ͯ͠·͢ ੢೔ຊཱྀ٬మಓ͸ LLM ͷ׆༻Λਪਐ͍ͯ͠·͢ɻ
4. 0. લճͷ͓͞Β͍
5. ܗࣜݴޠͱ੔ࣜʢwffʣŠŠୈ 3ճͷఆٛ ߲ͷؼೲతఆٛ (1) ม਺ x0 , x1 , . . . ͸߲ (2) Z ͸߲ (3) t ͕߲ ⇒ S(t) ͸߲ (4) t1 , t2 ͕߲ ⇒ plus(t1 , t2 ) ͸߲ (5) ্هҎ֎͸߲Ͱͳ͍ ໋୊ʢจʣͷؼೲతఆٛ (1) t1 = t2 ʢt1 , t2 ͸߲ʣ͸จ (2) A, B ͕จ ⇒ (A ∧ B) ͸จ (3) A, B ͕จ ⇒ (A → B) ͸จ (4) A ͕จ ⇒ ¬A ͸จ (5) ্هҎ֎͸จͰͳ͍ ؼೲతఆٛͷڞ௨ߏ଄ ࠷ॳͷҰาʢجఈʣ ม਺ɾఆ਺ɾݪࢠ໋୊ نଇͷ܁Γฦ͠ʢؼೲεςοϓʣ ݁߹ࢠɾޙऀؔ਺ ดแ৚݅ ʮ্هҎ֎͸ʜͰͳ͍ʯ ࣍ͷεςοϓ ͜ͷݴޠͷதͰਪ࿦ʢࣗવԋ៷ʣΛఆٛ͢Δ ֤݁߹ࢠʹಋೖنଇɾআڈنଇΛ༩͑Δ ˠ ࠓ೔͸ → ͔Β࢝ΊΔ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 5
6. ߏ੒ͱղମŠŠ࿦ཧ݁߹ࢠͷೋଆ໘ ࣗવ਺΋Ͳ͖Ͱͷߏ੒ɾղମ ߏ੒ࢠɿS Ͱࣗવ਺Λ࡞Δ Z S − → S(Z) S − → S(S(Z)) S − → · · · ղମࢠɿplus ͷத਎ΛऔΓग़͢ plus(t1 , t2 ) ͔Β t1 , t2 Λ෼ղ ࿦ཧ݁߹ࢠͰ΋ಉ͡ ಋೖنଇʢߏ੒ࢠʹ૬౰ʣ ͦͷه߸ΛؚΉ໋୊Λ࡞Δ আڈنଇʢղମࢠʹ૬౰ʣ ͦͷه߸ΛؚΉ໋୊Λ෼ղͯ͠࢖͏ ূ໌࿦తҙຯ࿦ͷ֩৺ ࿦ཧ݁߹ࢠͷҙຯ͸ ಋೖنଇͱআڈنଇͷରʹΑͬͯ༩͑ΒΕΔ ʮਅِʯͰ͸ͳ͘࢖ΘΕํ͕ҙຯΛܾΊΔ ˠਅཧ஋දͳ͠Ͱ࿦ཧΛఆٛͰ͖Δ ຊतۀͷΞϓϩʔνʢ࠶֬ೝʣ ਅཧॏࢹܕɿਖ਼͍͠લఏˠਖ਼͍݁͠࿦ ਪ࿦نଇॏࢹܕʢຊतۀʣɿ نଇʹैͬͨه߸ͷม׵͕ਖ਼͍͠ਪ࿦ ˠ ϋϧγωʔγϣϯ਍அʹ௚݁ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 6
7. ϋʔϞχʔɿϩʔΧϧͱάϩʔόϧͷ௼Γ߹͍ʢ࠶ܝʣ ہॴతϋʔϞχʔ ಋೖنଇͱআڈنଇͷ௼Γ߹͍ ʮআڈͰ͖Δͷ͸ɺಋೖʹΑͬͯ ೖΕͨ΋ͷ͚ͩʯ ˠ ֤݁߹ࢠͷઃܭͷ੔߹ੑ ࠓ೔͸͜͜ʹूத͢Δ େҬతϋʔϞχʔ ূ໌ͷਖ਼نԽՄೳੑ ʮͲΜͳӌճ࿏ͷ͋Δূ໌΋ ͖Ε͍ͳূ໌ʹม׵Ͱ͖Δʯ ˠ ମܥશମͷ݈શੑ ୈ 12ʙ14 ճͰѻ͏ ࠓޙͷतۀܭըʢ࠶ܝʣ • ୈ 4ʙ5 ճɿ∧, ∨, →, ¬ ͷਪ࿦نଇʢϩʔΧϧͳنଇʣ • ୈ 6ʙ7 ճɿূ໌ͷಡΈํɾॻ͖ํʢԋशʣ • ୈ 8ʙ9 ճɿอकత֦ுɾ൓సݪཧ • ୈ 10ʙ11 ճɿTonk ໰୊ɾBoche ໰୊ • ୈ 12ʙ14 ճɿূ໌ͷਖ਼نԽʢਅਖ਼ͳϋʔϞχʔʣ • ࠷ऴճɿLLM ͷϋϧγωʔγϣϯΛূ໌࿦తʹݟΔ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 7
8. 1. ॓୊ͷ౴͑߹Θͤɾจͷఆٛͷվగ
9. ॓୊໰୊ͷ࠶ܝ Ұൠ໰୊ɿҎԼͷ͔ࣜΒ wffʢ੔ࣜʣΛબ΂ (a) S(∗) (b) (Z = S(Z)) ∧ (Z = S(Z)) (c) x0 ∨ (x1 = x2 ) (d) (x0 = x1 ) ∧ (x1 = x2 ) ղ͖ํͷํ਑ ؼೲతఆٛΛҰͭͻͱͭͨͲͬͯ൑ఆ͢Δ ఆٛͷͲͷεςοϓͰߏ੒͞ΕΔ͔ʢ·ͨ͸ߏ੒Ͱ͖ͳ͍͔ʣΛࣔ͢͜ͱ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 9
10. 2. ͳΒ͹ʢ→ʣͷਪ࿦نଇ
11. ϝλϨϕϧɿ਺ֶʹ͓͚ΔʮͳΒ͹ʯͷ࢖ΘΕํ ʮͳΒ͹ʯͷಋೖʢˠΛ࡞Δʣ ∠A = 90◦ ͔Β ∠B + ∠C = 90◦ Λ ಋग़ͨ͠ਪ࿦શମΛࢦͯ͠ɿ ʮ∠A = 90◦ ͳΒ͹ ∠B + ∠C = 90◦ʯ ˠ લఏͱ݁࿦Λ݁ͼ͚ͭͯ ৽ͨͳ໋୊Λߏ੒͢Δ ʮͳΒ͹ʯͷআڈʢˠΛ࢖͏ʣ ʮ∠A = 90◦ ͳΒ͹ ∠B + ∠C = 90◦ʯ ͔࣮ͭࡍʹ ∠A = 90◦ Ͱ͋Δͱ͖ɿ ∠B + ∠C = 90◦ ͕੒ཱ ˠ → ΛؚΉ໋୊ʹલఏΛద༻ͯ͠ ݁࿦ΛऔΓग़͢ ʮͳΒ͹ʯͷܗࣜతఆٛͷํ਑ ্هͷϝλϨϕϧͷ࢖ΘΕํΛର৅ϨϕϧͰγϛϡϨʔτ͢Δ ˠ ಋೖنଇʢߏ੒ʣͱআڈنଇʢղମʣͷରͱͯ͠ఆٛ͢Δ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 11
12. ࣗવԋ៷ͷ૑࢝ऀɿήϧϋϧτɾήϯπΣϯʢ1909–1945ʣ ήϯπΣϯ͕ఆࣜԽͨ͠΋ͷʢ1934 ೥ʣ ࣗવԋ៷ʢnatural deductionʣ ਺ֶऀ͕࣮ࡍʹߦ͏ਪ࿦Λ ಋೖنଇɾআڈنଇͱͯ͠ܗࣜԽ ਪ݅ܭࢉʢsequent calculusʣ ਪ࿦ͷରশతͳߏ଄Λ໌ࣔ͢Δମܥ جຊݪཧʢGentzen 1934ʣ ࿦ཧఆ߲ͷҙຯ͸ɺ ͦͷਪ࿦نଇʹΑͬͯ༩͑ΒΕΔ ˠ ূ໌࿦తҙຯ࿦ͷग़ൃ఺ ܦྺʹ͍ͭͯʢҰݴʣ ήονϯήϯେֶͰϕϧφΠεͷఋࢠ 1945 ೥ϓϥϋղ์ޙɺऩ༰ॴͰծࢮʢڗ೥ 35 ࡀʣ एͯ͘͠ূ໌࿦ͷجૅΛଧཱͪͯɺੜ֔Λͦ͜ʹ๋͛ͨ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 12
13. →-ಋೖنଇʢ→Iʣ ఆٛ [u : A] . . . B →+u A → B ಡΈํɿA ΛԾఆͯ͠ B ͕ূ໌Ͱ͖ͨͱ͖ɺ A → B ͕ূ໌͞ΕΔ ԾఆͷΩϟϯηϧʢdischargeʣ [u : A]ɿԾఆ A ʹϥϕϧ u ΛషΓɺ ࢖͍ऴΘͬͨ͜ͱΛએݴ͢Δ ϥϕϧ͸೚ҙʢu, v, w, . . . ͳͲʣ ଞͷϥϕϧͱࠞಉ͠ͳ͚Ε͹Α͍ ࠷΋୹͍ྫɿA → A ͷূ໌ [u : A] →+u A → A Ծఆ A ͔Β A ͕ʢࣗ໌ʹʣಘΒΕΔ ˠ →I Ͱ A → A Λߏ੒ ূ໌໦ͷߏ଄ ઌ୺ʢ༿ʣɿԾఆʢΩϟϯηϧલʣ ֤εςοϓɿنଇͷҰճద༻ ࠜʢ຤୺ʣɿূ໌͞Εͨ݁࿦ Ωϟϯηϧ͢ΔԾఆ͕ͳ͘ͳͬͨΒূ໌׬ྃ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 13
14. →-আڈنଇʢ→Eɺmodus ponensʣ ఆٛ A A → B →− B ಡΈํɿA ͱ A → B ͕͋Ε͹ B ͕ಘΒΕΔ ओͳԾఆɿ→ ΛؚΉଆʢA → Bʣ ෭࣍తͳԾఆɿؚ·ͳ͍ଆʢAʣ modus ponens ݹ͔͘Β modus ponensʢલ݅ߠఆʣͱݺ͹ΕΔ ࿦ཧ๏ଇͷ୅දྫͷͻͱͭ ʮA ͳΒ͹ BʯͱʮAʯ͔ΒʮBʯ →I ͱ →E ͷରൺ ໾ׂ → ͷಈ͖ →I ߏ੒ → Λ࡞Δ →E ղମ → ΛऔΓআ͘ ϋʔϞχʔͷ৚݅ʢ௚ײʣ →E ͰऔΓग़ͤΔͷ͸ →I ͰೖΕͨ಺༰͚ͩ ˠ نଇ͕ʮ௼Γ߹͍ͬͯΔʯঢ়ଶ ࠷খ໋୊࿦ཧͷ → அย →I ͱ →E ͚ͩΛ࣋ͭମܥ ˠ ࠷খ໋୊࿦ཧͷ → அย ࠓ೔ͷԋशͱ॓୊͸͜ͷମܥͷதͰߦ͏ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 14
15. ͖Ε͍ͳূ໌ͷॻ͖ํŠŠʮ࠷ޙͷ݁߹ࢠʯ͔Βٯࢉ͢Δ ٯࢉͷखॱ Step 1ɿূ໌໋͍ͨ͠୊ͷ ʮ࠷ޙʹಋೖ͞Εͨ݁߹ࢠʯΛಛఆ Step 2ɿͦͷ௚લͷ໋୊ͷ ܗΛ֬ఆ͢Δ Step 3ɿStep 2 Λ܁Γฦͯ͠ Ծఆ·Ͱ૎Δ Step 4ɿআڈنଇͰ Ծఆ͔Β݁࿦Λ૊ΈཱͯΔ ͖Ε͍ͳূ໌ʢਖ਼نͳূ໌ʣ ճΓಓͷͳ͍ূ໌ ʮಋೖ͙ͯ͢͠আڈ͢Δʯ ແବͳεςοϓ͕ͳ͍ ˠ ෦෼࿦ཧࣜݪཧΛຬͨ͢ ྫɿA → (B → A) ͷٯࢉ ࠷ޙͷ݁߹ࢠɿ֎ଆͷ →ʢA ͱ B → Aʣ ˠ Ծఆ [u : A] ͔Β B → A Λূ໌ ࣍ͷ݁߹ࢠɿ಺ଆͷ →ʢB ͱ Aʣ ˠ Ծఆ [v : B] ͔Β A Λূ໌ A ͸طʹԾఆʹ͋Δ ˠ ׬੒ʂ [u : A] →+v B → A →+u A → (B → A) ʢ[v : B] ͸࢖ΘΕͳ͍ŠŠऑԽଇʣ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 15
16. Լ͔Βٯࢉͷ࣮ྫɿA → ((A → B) → B) Λ૊ΈཱͯΔ Step 1ɿ࠷ޙͷ݁߹ࢠ͔Βɻ݁࿦ͷܗΛݟͯԾఆΛܾఆ [u : A] . . . (A → B) → B →+u A → ((A → B) → B) ࠷ޙͷ → ΛݟΔɿA ͱ (A → B) → B ˠ Ծఆ [u : A] ΛΩϟϯηϧ͢Δ͸ͣ Step 2ɿҰஈ্ͷ (A → B) → B ͷ࠷ޙͷ݁߹ࢠΛݟΔ [u : A] [w : A → B] . . . B →+w (A → B) → B →+u A → ((A → B) → B) A → B ͱ B ˠ Ծఆ [w : A → B] Λ௥Ճɻ[u : A] ͱ [w : A → B] ͔Β B Λ࡞Ε͹Α͍ Step 3ɿԾఆ [u : A] ͱ [w : A → B] ͔Β B Λ࡞Δ ˠ →E Ұൃʂ ׬੒ [u : A] [w : A → B] →− B →+w (A → B) → B →+u A → ((A → B) → B) ճΓಓͳ͠ɻআڈʢ→Eʣˠ ಋೖʢ→I × 2ʣͷॱɻ͖Ε͍ͳূ໌ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 16
17. ࿦ཧతޠኮͷ໾ׂɿ໌ࣔԽʢmaking it explicitʣ Robert Brandom → ͷ໾ׂŠŠԿ͕ʮ໌ࣔԽʯ͞ΕΔ͔ ର৅ϨϕϧͰ A ͔Β B ͕ಋग़͞ΕΔͱ͖ɺ ϝλϨϕϧͷ؍࡯ऀ͸ʮA ͔Β B ͕ಋग़͞Εͨʯ ͱ͍͏ࣄ࣮Λओு͢Δ͜ͱ͕Ͱ͖Δ →-ಋೖنଇ͸ɺ͜ͷϝλϨϕϧͷओுΛ ର৅Ϩϕϧͷ໋୊ A → B ͱͯ͠औΓࠐΉ ˠ ਪ࿦ͷࣄ࣮Λʮ͍·͜͜ͷݴޠͷதͰޠΕΔʯ Α͏ʹ͢Δͷ͕ → ͱ͍͏࿦ཧه߸ Brandom ͷηϦϑʢཁ໿ʣ ࿦ཧతޠኮ͸ɺ΋ͱ΋ͱͷ࣮࣭ਪ࿦ˊŠ ͕ͨͬͯ͠ݹ͍ޠኮʹΑͬͯදݱ͞Εͨ ֓೦త಺༰ˊŠ ໌ࣔతʹ͢Δ ͱ͍͏ࡍཱͬͨදݱత໾ׂΛԋ͡Δ ˠ Making it Explicitʢ1994ʣ ͨͩ͠ɿ໌ࣔԽ͕੒ཱ͢Δʹ͸ɺ→ ͷنଇ͕ ʮѱ͞Λ͠ͳ͍ʯ͜ͱʢϋʔϞχʔʣ͕ඞཁ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 17
18. ԾఆͷΩϟϯηϧɿ࿦ཧମܥͷσβΠϯબ୒ σβΠϯબ୒ 1ɿॖ໿ଇ ಉ͡ϥϕϧͷԾఆΛෳ਺ՕॴͰ࢖͍ɺ ҰวʹΩϟϯηϧͯ͠Α͍͔ʁ ࠷খ໋୊࿦ཧʢຊतۀʣɿ✓ ڐ͢ ΞϑΟϯ࿦ཧɿ× ֤Ծఆ͸ߴʑҰճ ྫɿ[v : A] ͕ূ໌தʹ 2 ՕॴݱΕɺ →I[v] ͰҰวʹΩϟϯηϧ σβΠϯબ୒ 2ɿऑԽଇ ࢖Θͳ͍ԾఆΛࣗ༝ʹ௥Ճͯ͠Α͍͔ʁ ࠷খ໋୊࿦ཧɾΞϑΟϯ࿦ཧɿ✓ ڐ͢ ઢܗ࿦ཧɾϥϯϕοΫܭࢉɿ× ڐ͞ͳ͍ ྫɿA → (B → A) ͷূ໌Ͱ [v : B] ͕࢖ΘΕͣʹऴΘΔ ମܥͷൺֱ ମܥ ॖ໿ ऑԽ ࠷খ໋୊࿦ཧ ✓ ✓ ΞϑΟϯ࿦ཧ × ✓ ઢܗ࿦ཧ × × ͳͥσβΠϯ͕ॏཁ͔ ॖ໿ଇͷ༗ແͰূ໌Ͱ͖Δ໋୊ͷू߹͕มΘΔ ূ໌࿦తʹ͸ॖ໿ଇ͕ ਖ਼نԽΛ೉͘͢͠Δओ൜ ʢୈ 12ʙ14 ճͰৄड़ʣ ˠ proof net Ͱʮݟ͑ΔԽʯ͞ΕΔ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 18
19. ύζϧͷੈք΁ Α͏ͦ͜ ূ໌ωοτ͸ূ໌ਤͷ ʮ΋͏Ұͭͷݟํʯ ಋೖɾআڈͷنଇΛ ϫΠϠͱϊʔυͱͯ͠ ඳ͖௚ͯ͠ΈΑ͏
20. 3. ূ໌ωοτʢproof netʣೖ໳
21. ূ໌ωοτͷ૑࢝ऀɿδϟϯʹΠϰɾδϥʔϧ Jean-Yves Girard ʢϚϧηΠϢେֶʣ δϥʔϧͷओͳۀ੷ ઢܗ࿦ཧʢLinear Logic, 1987ʣ ॖ໿ଇɾऑԽଇΛ࣋ͨͳ͍࿦ཧମܥ ʮ໋୊͸Ϧιʔεʯͱ͍͏௚؍ ূ໌ωοτʢProof nets, 1987ʣ ূ໌ͷຊ࣭తߏ଄Λ ϫΠϠʴϊʔυͱͯ͠ՄࢹԽ γεςϜ Fʢଟ૬ܕϥϜμܭࢉʣ ϓϩάϥϛϯάݴޠཧ࿦ͷجૅ ຊतۀͰͷҐஔ͚ͮ Girard ͷ proof net ͷΞΠσΞΛ ࠷খ໋୊࿦ཧʢ→ அยʣʹద༻͢Δ ূ໌ͷॖ໿ଇʢY ࣈϊʔυʣ͕ ਖ਼نԽͷෳࡶ͞ΛੜΉཧ༝Λ ࢹ֮తʹཧղ͢ΔͨΊͷಓ۩ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 21
22. ূ໌ωοτʢproof netʣͱ͸Կ͔ ূ໌໦ͷݟ͑ʹ͘͞ ূ໌໦Ͱ͸໋୊ͷྲྀΕ͕Θ͔Γʹ͍͘ w ಉ͡Ծఆ [u : A] ͕ෳ਺Օॴʹॻ͔Εͯ΋ ʮಉ͡΋ͷʯ͔ࢴ໘্͸Θ͔Βͳ͍ w ಋೖɾআڈͷੵΈॏͶͰ໋୊͕ Ͳ͔͜ΒͲ͜΁ྲྀΕ͍ͯΔ͔௥͍ʹ͍͘ proof net ͷൃ૝ ໋୊ΛϫΠϠʢ഑ઢʣͱͯ͠දݱ ਪ࿦Λϊʔυʢശʣͱͯ͠දݱ ˠ ূ໌ͷຊ࣭తߏ଄Λࢹ֮Խ͢Δ Girardʢ1987 ೥ɺઢܗ࿦ཧͷ࿦จʣͰಋೖ ຊतۀͰ͸࠷খ໋୊࿦ཧʹద༻͢Δ ه๏ͷϧʔϧ ࣮ઢϫΠϠɿ௨ৗͷ໋୊ͷྲྀΕ ఺ઢϫΠϠɿΩϟϯηϧ͞ΕͨԾఆ ʢdischargedʣ ;Β;ΒϫΠϠɿ࢖ΘΕͳ͍Ծఆ ʢweakeningɺऑԽʣ →E ϊʔυɿ2 ຊೖྗ ˠ 1 ຊग़ྗ →I ϊʔυɿ఺ઢ 1 ຊʴ࣮ઢ 1 ຊ ˠ ࣮ઢ 1 ຊग़ྗ ˠ ԋशͰ࣮ࡍʹखΛಈ͔ͯ͠ඳ͍ͯΈΑ͏ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 22
23. →-E ͱ →-I ͷ proof net →-Eʢআڈʣͷϊʔυ A → B A →E B 2 ຊͷ࣮ઢϫΠϠ͕ೖྗ 1 ຊͷ࣮ઢϫΠϠ͕ग़ྗ →-Iʢಋೖʣͷϊʔυ [u:A] B →I[u] A → B ఺ઢʹ discharged ఺ઢʢdischargedʣʴ࣮ઢ͕ೖྗ A → B ͷ࣮ઢϫΠϠ͕ग़ྗ ྫɿA → A ͷ proof net [u:A] →I[u] A → A Ծఆ A ͷ఺ઢϫΠϠҰຊ͕ଈ࠲ʹΩϟϯηϧ͞ΕΔɻ ໋୊͕Ұछྨ͔͠ొ৔͠ͳ͍͜ͱ͕Ұ໨ྎવɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 23
24. ॖ໿ଇͱ Y ࣈϊʔυŠŠ proof net ͷʮ೉఺ʯͷՄࢹԽ ॖ໿ଇͱ͸ʢ࠶ܝʣ ಉ͡ϥϕϧͷԾఆΛෳ਺ՕॴͰ࢖͍ɺ ҰวʹΩϟϯηϧ͢Δ ྫɿ[v : A] ͕ূ໌தʹ 2 ՕॴݱΕΔ proof net Ͱͷදݱ Ծఆ [v : A] ͷϫΠϠ్͕தͰ ೋވʹ෼ذ͢Δ ͜Ε͕ Y ࣈϊʔυʢॖ໿ϊʔυʣ [v:A] Y ࣈʢॖ໿ʣ ࢬ 1 ࢬ 2 Y ࣈϊʔυͷূ໌࿦తҙຯ Y ࣈͳ͠ʢΞϑΟϯ࿦ཧʣ ˠ ূ໌ͷਖ਼نԽʢΧοτআڈʣ͕ ہॴతॻ͖׵͚͑ͩͰ׬݁ ˠ ਖ਼نԽ͕៉ྷʹऴΘΔ Y ࣈ͋Γʢ࠷খ໋୊࿦ཧʣ ˠ Χοτআڈ͕ Y ࣈΛ௨ա͢Δͱ͖ ূ໌ͷҰ෦͕ෳ੡͞ΕΔ ˠ ෳ੡ʹ·ͨ Y ࣈ͕͋Ε͹ ͞Βʹෳ੡ʜʜ ˠ ऴྃੑͷূ໌ʹ ε0 ʢ௒ݶؼೲ๏ʣ͕ඞཁ ʮূ໌࿦తѱເʯͷՄࢹԽ Y ࣈϊʔυͷ഑ஔΛݟΕ͹ ͦͷূ໌ͷʮ೉͠͞ͷߏ଄ʯ͕Θ͔Δ ৄࡉ͸ୈ 12ʙ14 ճͰ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 24
25. 4. ԋश໰୊
26. ԋश໰୊ŠŠࠓ೔ͷԋश ໰୊ʢ→ ͷΈ࢖༻ɺA, B, C ͸೚ҙͷ໋୊ʣ ໰ 1 A → A ʢ࠷୹ͷূ໌͸ʁʣ ໰ 2 A → (B → A) ʢऑԽଇΛ࢖͏ʣ Ϩϯδʣ (A → B) → (B → C) → (A → C) ʢࡾͭԾఆʣ ֤໰ʹ͍ͭͯ (i) ࣗવԋ៷ͷূ໌໦Λॻ͚ʢ͖Ε͍ͳূ໌Ͱʣ (ii) ূ໌໦Λ proof net ʹม׵ͤΑ ʢͲͷϫΠϠ͕఺ઢͰɺͲͷϫΠϠ͕஦ͿΒΓΜ͔ʣ ώϯτɿٯࢉͷखॱ ূ໌໋͍ͨ͠୊ͷʮ࠷ޙͷ →ʯΛಛఆˠ ͦͷ௚લͷܗΛ֬ఆˠ Ծఆ·Ͱ૎Δˠ আڈنଇͰ૊ΈཱͯΔ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 26
27. ԋश ໰1ɿA → A ূ໌໦ [u : A] →+u A → A ٯࢉɿ࠷ޙͷ → ͸ A ͱ A Λ݁Ϳ ˠ Ծఆ [u : A] ͔Β A ΛಘΔ ˠ A ͸Ծఆͦͷ΋ͷͳͷͰଈ׬੒ ˠ →I ͰԾఆΛΩϟϯηϧ proof net [u:A] →I[u] A → A Ծఆ A ͷ఺ઢϫΠϠҰຊͷΈ ໋୊͕Ұछྨ͔͠ొ৔͠ͳ͍ ˠ ࠷΋γϯϓϧͳ proof net ೉қ౓ɿ˒ˑˑɹূ໌ωοτͷಡΈํʹ׳ΕΔͨΊͷ४උ໰୊ Y ࣈϊʔυͳ͠ɾऑԽͳ͠ɻϫΠϠ 1 ຊ͕ଈΩϟϯηϧɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 27
28. ԋश ໰2ɿA → (B → A) ূ໌໦ [u : A] →+v B → A →+u A → (B → A) ٯࢉɿ֎ଆͷ →ʢA ͱ B → Aʣ ˠ Ծఆ [u : A] ͔Β B → A Λূ໌ ࣍ɿ಺ଆͷ →ʢB ͱ Aʣ ˠ Ծఆ [v : B] ͔Β A Λূ໌ʜʜ A ͸طʹ [u : A] ʹ͋Δʂ ˠ [v : B] ͸࢖ΘΕͳ͍ʢऑԽʣ proof net [u:A] [v:B] →I[u] →I[v] A → (B → A) ᒵ఺ઢʹ weakening [v : B] ͷϫΠϠ͕஦ͿΒΓΜʢऑԽʣ ˠ ʮB Λಋೖͨ͠ͷʹ࢖Θͳ͔ͬͨʯ ࣄ࣮͕ϫΠϠͰՄࢹԽ͞ΕΔ ೉қ౓ɿ˒˒ˑɹऑԽଇͷՄࢹԽɻ஦ͿΒΓΜϫΠϠΛݟ͚ͭΑ͏ Y ࣈϊʔυͳ͠ɻऑԽϫΠϠ͋Γɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 28
29. ԋश ໰3ʢνϟϨϯδʣ ɿ(A → B) → (B → C) → (A → C) ূ໌໦ [u : A → B] [w : A] →− B [v : B → C] →− C →+w A → C →+v (B → C) → (A → C) →+u (A → B) → (B → C) → (A → C) ٯࢉͰԾఆΛܾఆɿ [u : A → B], [v : B → C], [w : A] আڈͰ C Λߏ੒ ˠ ॱʹΩϟϯηϧ proof net [u:A→B] [w:A] [v:B →C] →E B →E C 3 ຊͷϫΠϠ͕ॱ࣍ →E Λ ܦ༝ͯ͠ C ΁ྲྀΕΔ Y ࣈϊʔυͳ͠ʢॖ໿ͳ͠ʣ ೉қ౓ɿ˒˒˒ɹࡾͭͷԾఆΛٯࢉͰ֬ఆͤ͞Δɻূ໌ωοτ͕͖ͬ͢ΓྲྀΕΔ Y ࣈͳ͠ɾऑԽͳ͠ɻϫΠϠ͕ઢܗʹྲྀΕΔ࠷΋͖Ε͍ͳྫɻ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 29
30. 5. ॓୊
31. ॓୊ŠŠ → ͷূ໌ͱ proof net Ұൠ໰୊ʢA, B, C ͸೚ҙͷ໋୊ʣ ՄೳͳݶΓ͖Ε͍ͳূ໌Ͱࣔ͠ɺͦͷޙ proof net Λඳ͚ɻ ূ໌Ͱ͖ͳ͍৔߹͸ʮূ໌ෆՄೳʯͱ໌ه͢Δ͜ͱɻ (1) (A → A → B) → (A → B) ώϯτɿಉ͡Ծఆ A Λ 2 ճ࢖ͬͯΑ͍ʢॖ໿ଇʣ (2) A → (B → C) → (A → B) → C ώϯτɿԾఆΛઌʹܾΊ͔ͯΒʮٯࢉʯΛ࢝ΊΑ νϟϨϯδ໰୊ ҎԼͷূ໌໦Λ proof net ʹม׵ͤΑʢproof net ͔Βূ໌໦΁ͷٯม׵ʹ΋௅ઓʣ ɻ [u : A → B] [w : A] →− B [v : B → C] →− C →+w A → C →+v (B → C) → (A → C) →+u (A → B) → (B → C) → (A → C) Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 31
32. ॓୊ɿఏग़ཁྖ ఏग़ཁྖ ʲఏग़ظݶʳ5 ݄ 19 ೔ʢՐʣतۀ։࢝௚લ·Ͱ ʲఏग़৔ॴʳKULMS तۀαΠτͷ՝୊ΑΓ ʲܗࣜʳ • ఏग़ͷࡍ͸ɺKULMS ͷतۀαΠτʹೖΓɺࠨϝχϡʔͷʮ՝୊ʯ͔Β֘౰͢Δ՝୊Λ։͍ͯఏग़͍ͯͩ͘͠͞ɻ ʮఏग़ശʯͰ͸͋Γ· ͤΜͷͰɺ͝஫ҙ͍ͩ͘͞ɻ • ·ͨɺϑΝΠϧΛఴ෇ͨ͠ޙɺ ʮਐΊΔʯΛԡ͚ͨͩ͠Ͱ͸ఏग़׬ྃʹͳΓ·ͤΜɻ࠷ޙʹඞͣʮఏग़ʯΛԡ͠ɺఏग़ ID ͕දࣔ͞ΕΔ͜ ͱΛ֬ೝ͍ͯͩ͘͠͞ɻ • Wordɾtexɾpdfɺ·ͨ͸Ϩϙʔτ༻ࢴΛࡱӨͯ͠ఏग़ ๯಄ʹॴଐɾࢯ໊ɾֶ੶൪߸Λهೖ͢Δ͜ͱ ʢఏग़ശʹఏग़Ͱ͖ͳ͍৔߹͸ϝʔϧఏग़΋Մʣ • खॻ͖Ͱ௚઀ఏग़ͷ৔߹͸तۀ։࢝લʹߨࢣ΁ ˞ ॓୊Λղ͘ͷʹ͔͔ͬͨ࣌ؒΛඞͣهೖ͢Δ͜ͱʢ෼ྔௐ੔ͷͨΊʣ ࣍ճʢୈ 5 ճʣͷ༧ఆŠŠ 5 ݄ 19 ೔ʢՐʣ • ∧ʢ͔ͭʣͷಋೖنଇɾআڈنଇ • ∨ʢ·ͨ͸ʣͷಋೖنଇɾআڈنଇ • ॓୊ͷղઆ Պֶ఩ֶՊֶ࢙ (ԋश) ࿦ཧֶʢલظʣ ୲౰ɿ໼ా෦ढ़հ 32