←→を含む述語論理の定理4
←→を含む述語論理の定理1 | 宇宙とブラックホールのQ&A←→を含む述語論理の定理3 | 宇宙とブラックホールのQ&A---------------------------------------------------------------- 7.三連環 (三連環)(9-29) 14, 3,11,7,3 ☆8 三連環反対 ¬:. ∀Ax←→¬Bx: ∧ :∀x. Bx←→¬Cx: ∧ : ∀x. Cx←→¬Ax .(9-30) 30,3,11,7,3 ☆8 三連環矛盾 ¬:. ∀Ax←→¬Bx: ∧ :∀x. Bx←→¬Cx: ∧ : ∃x. Cx←→¬Ax .(9-31) 20, 3,11,0,3 ☆6 三連環小反対 ∃x. Ax←→Bx: ∨ :∃x. Bx←→Cx: ∨ : ∃x. Cx←→Ax .(9-32) 24, 3,11,0,3 ☆6 三連環排中 ∀x. Ax←→Bx: ∨ :∃x. Bx←→Cx: ∨ : ∃x. Cx←→Ax .次の式たちは、以前の記事で取り上げた命題論理の式ですが、ABCの3つの単位命題(命題変数)が輪環の順となっており、対称性が高いため美しさを感じます。α6, 06, 3,11,7M ¬: A←→¬B. ∧ .B←→¬C. ∧ .C←→¬A .α1, 04, 3,11,0☆ A←→B. ∨ .B←→C. ∨ .C←→A .複雑な命題論理式2 | 宇宙とブラックホールのQ&A特に、α1は否定を使わずに排中律、つまり2値論理の本質を表していて、命題論理屈指の美しさです。(と私は感じるのですが、こういう美意識を分かってくれる人はいるのかな・・・)これらの式をこのブログでは「三連環(さんれんかん)」と呼ぶことにします。つまり、「三連環」とは、「同値←→を3個含む対称性の高い式」を意味します。三連環の2つの式のうち、α6は矛盾律類似式、α1は排中律類似式です。矛盾律類似式、排中律類似式、反対、小反対という表現は、2つの“部品”をもつ式についての表現でしたが、3つの“部品”をもつ三連環についても用いることにします。α6について(←→矛盾)と同様に述語論理化・量化を行うと、とりあえず次の2式が得られます。 ¬∀x: Ax←→¬Bx. ∧ .Bx←→¬Cx. ∧ .Cx←→¬Ax . ¬∃x: Ax←→¬Bx. ∧ .Bx←→¬Cx. ∧ .Cx←→¬Ax .まず上式については ∀x. Ax∧Bx: ←→ ∀xAx ∧ ∀xBx .を使って、次の式が得られます。 ¬:.∀x.Ax←→¬Bx: ∧ :∀x.Bx←→¬Cx: ∧ :∀x.Cx←→¬Ax .(三連環反対)次に下式については ∀xAx∧∃xBx → ∃x. Ax∧Bxの対偶 ¬∃x. Ax∧Bx: → :¬.∀xAx∧∃xBxと先の式を適用して、次の式が得られます。 ¬:.∀x.Ax←→¬Bx: ∧ :∀x.Bx←→¬Cx: ∧ :∃x.Cx←→¬Ax .(三連環矛盾)ちなみに次の式は成り立ちません。× ¬:.∀x.Ax←→¬Bx: ∧ :∃x.Bx←→¬Cx: ∧ :∃x.Cx←→¬Ax .「Ba←→¬Ca」をみたすaと「Cb←→¬Ab」をみたすbが異なる場合があるからです。α1について述語論理化・量化を行うと、とりあえず次の2式が得られます。(6) ∀x: Ax←→Bx. ∨ .Bx←→Cx. ∨ .Cx←→Aa .(7) ∃x: Ax←→Bx. ∨ .Bx←→Cx. ∨ .Cx←→Aa .まず(7)については(5-3,4) ∃x. Ax∨Bx: ←→ ∃x Ax ∨ ∃x Bx .を使って、次の式が得られます。(9-31) ☆ ∃x. Ax←→Bx: ∨ :∃x. Bx←→Cx: ∨ : ∃x. Cx←→Ax .(三連環小反対)また、(6)については(5-8) ☆ ∀x. Ax∨Bx: → ∀x Ax ∨ ∃x Bx .を2回適用して、(9-31) ☆ ∀x. Ax←→Bx: ∨ :∃x. Bx←→Cx: ∨ : ∃x. Cx←→Ax .(三連環排中)となります。ちなみに、次の式は成り立ちません。× ∀x. Ax←→Bx: ∨ :∀x. Bx←→Cx: ∨ : ∃x. Cx←→Ax . 8.対応する命題論理の式述語論理の式には対応する命題論理の式が存在します。「対応する命題論理の式」とはどういう意味かについては、述語論理の追加1 | 宇宙とブラックホールのQ&A 「3.命題論理の対応する式」の箇所をご覧ください。まあ、こういうことを知っていると、述語論理式の成立の可否について見通しが良くなるとか新たな命題論理式が見つかるとかいいこともあります。これまで取り上げた32本の式の大部分について、対応する命題論理の式を掲げます。 (←→含意1)(9-1)’ 08, 3,11,2 A←→B.∧.C←→B: → :A∧C.∨.¬A∧¬C .(9-2)’ 02, 3,13,0 A←→B.∧.C←→B: → :A∧C ←→B .(9-3)’ 04, 3,13,0 A←→B.∧.C←→B: → :A∨C ←→B .(9-4)’ 08, 3,17,2 A∧B.∨.¬A∧¬B: ∧ :A∧B←→C:. → :A←→C. ∧ .B←→C .(9-5)’ 08, 3,17,2 A∧B.∨.¬A∧¬B: ∧ :A∨B←→C:. → :A←→C. ∧ .B←→C .(9-6)’ 04, 3,19,0 A∧B←→C. ∧ .A∨B←→C: → :A←→C. ∧ .B←→C .(9-7)’ 08, 3,15,2 A∧B.∨.¬A∧¬B: ∧ .A∧B←→C: → .A∨B←→C .(9-8)’ 08, 3,15,2 A∧B.∨.¬A∧¬B: ∧ .A∨B←→C: → .A∧B←→C .(9-9)’ 08, 3,15,2 A∧B←→C. ∧ .A∨B←→C: → :A∧B.∨.¬A∧¬B(9-10)’ 08, 3,11,2 A∨B.∧.¬A∨¬B: → :A←→C.∨.B←→C .(9-11)’ 04, 3,13,0 A∧B←→C. → :A←→C.∨.B←→C(9-12)’ 04, 3,13,0 A∨B←→C. → :A←→C.∨.B←→C .(9-13)’ 08, 3,17,2 A←→B.∨.C←→B: → :. A∨C.∧.¬A∨¬C: ∨ .A∧C←→B .(9-14)’ 08, 3,17,2 A←→B.∨.C←→B: → :. A∨C.∧.¬A∨¬C: ∨ .A∨C←→B .(9-15)’ 04, 3,19,0 A←→B.∨.C←→B: → :A∧C←→B. ∨ .A∨C←→B .(9-16)’ 08, 3,15,2 A∨B.∧.¬A∨¬B: → :A∧B←→C. ∨ .A∨B←→C .(9-17)’ 08, 3,15,2 A∧B←→C: → :.A∨B.∧.¬A∨¬B: ∨ .A∨B←→C .(9-18)’ 08, 3,15,2 A∨B←→C: → :.A∨B.∧.¬A∨¬B: ∨ .A∧B←→C (←→含意2)(9-19)’ 02, 4,15,0 A←→B.∧.C←→D: → :A∧C←→B∧D .(9-20)’ 04, 4,15,0 A←→B.∧.C←→D: → :A∨C←→B∨D .(9-21)’ 04, 4,15,0 A∧B←→C∨D. → .A←→C. ∨ .B←→D . (←→矛盾)(9-23)’ 08, 4,15,5 ¬:.A←→B.∧.C←→D: ∧ :A←→¬B.∨.C←→¬D .(9-24)’ 08, 4,15,5 ¬:.A←→B.∨.C←→D: ∧ :A←→¬B.∧.C←→¬D . (←→排中)(9-26)’ 08, 4,15,4 A←→B.∧.C←→D: ∨ :A←→¬B.∨.C←→¬D .(9-27)’ 08, 4,15,4 A←→B.∨.C←→D: ∨ : A←→¬B.∧.C←→¬D .グループ(三連環)に属す式(9-29)~(9-32)の命題論理版は、単位命題がA~Fの6種類に増え、また長くなりすぎるので、省略します。また、「←→反対」(9-25)と「←→小反対」(9-28)の命題論理版は、それぞれ「¬:A←→B.∧.A←→¬B」と「A←→B.∨.A←→¬B」を弱くしたもので、意味がないため掲載しません。 9.ゲンツェン流シーケント計算による証明同値←→を含む式は見た目と違って内容が複雑であり、その分証明も他の式と比べて難しく、簡単な式のように「考えなくても手が勝手に動いて証明してくれる」ことはありません。だからこそできるだけ多く掲載したいのですが、困ったことにとにかくかさばるのですね。その上、式の数が32本にもなると、証明を掲載する式の数を絞らざるを得ません。もちろん私の手もとにはすべての式の証明があります。(前節で載せた対応する命題論理の式については、必ずしもすべての式が証明済みではありません。でも大丈夫でしょう)☆〇Mの後の数字は「頭」(一番上に来る論理式)の数です。証明のし方により異なってきますが、最も少ないものをとる方針です。(9-1)☆3 ∀x. Ax←→B: → ∀x Ax ∨ ∀x¬ Ax . 左∀ Aa ⇒ Aa 左→ B ⇒ B ∀x.Ax ⇒ Aa 左換 B,B→∀x.Ax ⇒ Aa 左∧2 B→∀x.Ax,B ⇒ Aa 左換 ∀x.Ax←→B,B ⇒ Aa 右∀ B,∀x.Ax←→B ⇒ Aa左→ Aa ⇒ Aa B,∀x.Ax←→B ⇒ ∀xAx左∧2 Aa,Aa→B,∀x.Ax←→B ⇒ ∀xAx左∀ Aa→B,∀x.Ax←→B,Aa ⇒ ∀xAx左減 Aa←→B,∀x.Ax←→B,Aa ⇒ ∀xAx左換 ∀x.Ax←→B,∀x.Ax←→B,Aa ⇒ ∀xAx右∀ ∀x.Ax←→B,Aa ⇒ ∀xAx右¬ Aa,∀x.Ax←→B ⇒ ∀xAx右∀ ∀x.Ax←→B ⇒ ∀x Ax,¬ Ab右∨’ ∀x.Ax←→B ⇒ ∀x Ax,∀x¬ Ax右→ ∀x.Ax←→B ⇒ ∀x Ax ∨ ∀x¬ Ax ⇒∀x.Ax←→B: → ∀x Ax ∨ ∀x¬ Ax //(9-3) M4 ∀x. Ax←→B: → .∃xAx←→B .左→ Aa ⇒ Aa B ⇒ B左換 Aa,Aa→B ⇒ B左∧1 Aa→B,Aa ⇒ B左∀ Aa←→B,Aa ⇒ B左換 ∀x.Ax←→B,Aa ⇒ B左∃ Aa,∀x.Ax←→B ⇒ B *左換 ∃xAx,∀x.Ax←→B ⇒ B 左換 B,∀x.Ax←→B ⇒ ∃xAx右∧ ∀x.Ax←→B ⇒ ∃xAx→B ∀x.Ax←→B ⇒ B→∃xAx右→ ∀x.Ax←→B ⇒ ∃xAx←→B ⇒ ∀x.Ax←→B:→.∃xAx←→B * 右∃ Aa ⇒ Aa左→ B ⇒ B Aa ⇒ ∃xAx左換 B,B→Aa ⇒ ∃xAx左∧ B→Aa,B ⇒ ∃xAx左∀ Aa←→B,B ⇒ ∃xAx左換 ∀x.Ax←→B,B ⇒ ∃xAx B,∀x.Ax←→B ⇒ ∃xAx //(9-4) 〇5 ∀x Ax∨∀x¬Ax. ∧ .∀xAx←→B: → :∀x. Ax←→B .左→ ∀xAx ⇒ ∀xAx B ⇒ B 左¬ Aa ⇒ Aa左換 ∀xAx,∀xAx→B ⇒ B 左∀ ¬Aa,Aa ⇒左∧1 ∀xAx→B,∀xAx ⇒ B 右増 ∀x¬Ax,Aa ⇒左換 ∀xAx←→B,∀xAx ⇒ B 左増 ∀x¬Ax,Aa ⇒B左増 ∀xAx,∀xAx←→B ⇒ B 左換 ∀xAx←→B,∀x¬Ax,Aa ⇒B右→ Aa,∀xAx,∀xAx←→B ⇒ B 右→ Aa,∀x¬Ax,∀xAx←→B ⇒B左∨ ∀xAx,∀xAx←→B ⇒ Aa→B ∀x¬Ax,∀xAx←→B ⇒ Aa→B右∧ ∀xAx∨∀x¬Ax,∀xAx←→B ⇒ Aa→B *左∧’ ∀xAx∨∀x¬Ax,∀xAx←→B ⇒ Aa←→B右∀ ∀xAx∨∀x¬Ax.∧.∀xAx←→B ⇒ Aa←→B右→ ∀xAx∨∀x¬Ax.∧.∀xAx←→B ⇒ ∀x.Ax←→B ⇒ ∀xAx∨∀x¬Ax.∧.∀xAx←→B:→:∀x.Ax←→B * 左∀ Aa ⇒ Aa左→ B ⇒ B ∀xAx ⇒ Aa右→ B,B→∀xAx ⇒ Aa左∧2 B→∀xAx ⇒ B→Aa左増 ∀xAx←→B ⇒ B→Aa ∀xAx∨∀x¬Ax,∀xAx←→B ⇒ B→Aa //--------------------------------- 続 く ---------------------------------★ 最近は中国経済の専門家である柯隆(か・りゅう)氏のyoutubeをよく見ています。日本については、1.高市首相の高い発信力に比べて、他の閣僚・周囲のスタッフの発信力・フォローが極めて不十分、2.中国と比べて、日本の主張を英語、中国語、スペイン語、アラビア語など多言語でタイムリーに発信することができていない、これでは国際的情報戦を戦えない、3.首相が代わっても不変な日本の長期的国家戦略が必要、といった主張が参考になります。米国の場合、共和・民主両党ともシンクタンク・ブレーンをもっていますが、日本もそういう仕組みが必要な時代なのでしょう。優秀な若者は外資系コンサルタント会社に就職するというのでは、日本の将来が危ぶまれます。★★ 今日のロジバン 不思議の国のアリス314 .i lo ro mei ca zi zutse gi’e barda djine .i la smacu cu midju 皆すぐに、大きな輪になって座り、ネズミを囲みました。mei : 濃度化。数詞から「x1はn個」という述語をつくる。MOI類。-mem-, -mei-djine : 環/輪/円である,x1は x2(内直径)・x3(外直径)の; x1は 環状/円環状 [空間・線]midju : 中央/中心/中枢/真ん中だ,x1は x2の。-mij- [空間・相対位置]最初の文は gi’e による複述構文で、共通のx1は { lo ro mei } 「皆」です。数詞 ro → 述語 { ro mei } → 体言 { lo ro mei } という成り立ちですね。{ ca zi } は [現在] [短時間] で、ネズミの発言内の { ba zi } が実現したものなので、同様に「すぐに」という意味になります。djine は「環/円」という意味ですが、その中心を意味する項を持たないため、次の文で補っています。次の文の主述語 { cu midju } のx1は { la smacu } ですが、省略されているx2は { lo ro mei } ですね。出典は、lo selfri be la .alis. bei bu'u la selmacygu'e (lojban.org)