背理法は不要なのか2at MATH背理法は不要なのか2 - 暇つぶし2ch■コピペモード□スレを通常表示□オプションモード□このｽﾚｯﾄﾞのURL■項目テキスト104:１３２人目の素数さん 26/08/03 07:52:19.76 tdy2H9Cz.net >>100 『背理法被害者の会』の関係者は、放置して （＾＾ 先へ進む ハイティング代数と直観主義 下記 ご参照 要するに、ハイティング代数は直観主義論理を形式化するために アレン・ハイティングにより導入された ということ これは大事だね 直観主義論理は、形式化できる (参考) https://ja.wikipedia.org/wiki/%E3%83%8F%E3%82%A4%E3%83%86%E3%82%A3%E3%83%B3%E3%82%B0%E4%BB%A3%E6%95%B0 ハイティング代数 (抜粋) ハイティング代数は 1930年に直観主義論理[2]を形式化するために アレン・ハイティングにより導入された。 ハイティング代数は束として分配的である。 ￢a の直観的内容は、a を仮定することで矛盾が導かれることである。この定義から が判る。更に a≦￢￢a が示されるが、その逆向きの不等式 ￢￢a≦a は一般には正しくない。つまり，ハイティング代数において二重否定の除去は一般には成立しない。 ハイティング代数は、ブール代数の一般化である。つまり、ハイティング代数に排中律 、または二重否定の除去 を課したものがブール代数である。ハイティング代数 H の ￢a の形の元はブール束をなすが、それは一般に H の部分代数とはならない(以下で説明する)。 ハイティング代数は、ブール代数が古典論理[3]のモデルとなるのと同じように、直観主義命題論理のモデルとなる。初等トポスの内部論理は、終対象 1の部分対象 (1 から subobject classifier（英語版） Ω への射と同値)に包含で順序をつけてできるハイティング代数を基にしている。 直観主義論理の公理を使った特徴づけ 直観主義命題論理のリンデンバウム代数（英語版）はハイティング代数。 初等トポスのsubobject classifier（英語版）Ωのglobal element（英語版）全体はハイティング代数をなす。これはトポスから誘導される高階直観主義論理の真理値からなる代数である。更に、一般にトポスの任意の対象 X の部分対象の集合はハイティング代数をなす。 証明可能な等式 上記の条件をみたすハイティング代数は、一般にハイティング代数が直観主義論理と関係づけられるのと同じ意味で、中間論理と関係づけられる。 普遍構成 直観主義論理を念頭においた命題論理式のハイティング代数 直観主義論理とハイティング代数 https://en.wikipedia.org/wiki/Heyting_algebra Heyting_algebra (google訳) (抜粋) ハイティング代数は、ブール代数が命題古典論理をモデル化するのと同様に、命題直観主義論理の代数モデルとして機能する。[ 3 ]基本トポスの内部論理は、包含によって順序付けられた終端オブジェクト1の部分オブジェクトのハイティング代数、つまり 1 から部分オブジェクト分類子Ω への射に基づいている。 直観主義論理の公理を用いた特徴付け 直観主義論理に適用されるヘイティング代数 関連項目 ・超直観主義（中間）論理 次ページ最新レス表示レスジャンプ類似スレ一覧スレッドの検索話題のニュースおまかせリストオプションしおりを挟むスレッドに書込スレッドの一覧暇つぶし2ch