…ることもできます（「古典論理は可換環論なんだよ」参照）。さて、Bはつまらないモノでしょうか？ そんなことはありません！ 古典論理はすべてB上で展開されます。今までは、古典論理を 1 + 1 = 0 という標数2の体を使って代数と関係付けました。しかし、1 + 1 = 1 という標数1の半体を使って代数と論理を架け橋する途もあります。むしろ、1 + 1 = 1 のほうが自然かもしれません。べき等半環の世界通常の体の上に環（や多元環）を考えたように、半体B上の半環を考えることがで…

…後にある論理（例えば古典論理）を使うことになります。つまり、ベースになる論理があって、そこにホーア式とそれに関する公理・推論規則を入れて拡張した論理体系がホーア論理（のインスタンス）です。今回は、「空文の公理」と「順次実行の推論規則」だけを付け加えた最小のホーア論理を導入しました。プログラムの正しさとはホーア式 p{f}q が「成立する」とはどういうことか考えてみます。「成立する」のひとつの解釈は次です。 演繹系としてのホーア論理のなかで、ホーア式 p{f}q が証明できる。…

…して、普通に、例えば古典論理ベースで等式的（equational）な形式的体系を作ったとします。さらに、半群の公理系（結合律だけ）を入れて形式的理論（セオリー）を作ったとしましょう。さて、単位元を含まない*4半群の形式的理論は矛盾するでしょうか？ 矛盾するならモデルは持てないはずですよね。でも、まさに郡司ペギオ-幸夫さんが提示している D = {f, ff, fff, ...} はこのセオリーのモデル（のひとつ）です。矛盾しているわけないじゃん。単位元とそれに関わる公理を入れ…

…で書いた問い合わせは古典論理の論理式に翻訳できます。逆に、“基本述語を原子論理式として組み立てられた古典命題論理”の論理式（集合ブール代数の元）は、JSONインスタンスで表現可能です。ということは、他のいかなる問い合わせ言語と比べてもなんら遜色がないのです。問い合わせコマンドの全体は次のようになるでしょう。 { "gender" : "female", "birth" : { "year" : @_AND [@_GTEQ 1980, @_LT 1990] }, "addr" …

…は特に仮定しないで、古典論理のシーケント計算が、プログラムの合成や変換と対応付けられることを説明します。包括的な説明ではなくて、二、三の例を出すだけですけどね。でも、その例に関しては詳しく説明します。内容： とても重要な注意 シーケントと推論図 シーケントと推論図とは何なのか カリー／ハワード対応 例外処理のコードパターン 例外コンバーターをパラメータとする例外処理 どこかで見たような推論規則 それにしても不思議だ とても重要な注意土曜の晩に、口汚く差別用語を使ってまで強調し…

…回定義した演繹系は、古典論理の演繹系NKに、ホーア・トリプルとその推論を突っこんだようなシステムですね。手と紙で証明するぶんには、この演繹系けっこう使いよい。が、あんまりコンピュータ向きじゃないので、次はコンピュータ向きの演繹系を考えることになります。でもその前に、もう少しチャントした形に整理したほうがいいかもな。 *1:正確に言えば、Jsonの部分集合を表すつもりの記号や記号列です。有り体にいってこの記事では、構文的対象と意味的対象をテキトーに混同しているのです。 *2:実…

…論 vs 意味論」「古典論理 vs 直観論理」みたいな分け方。いや、僕自身もこのテの分類に依拠しているし、教育コースとして伝統的でもあるんだけど、計算機のハナシだと、ここらへんが混じっちゃうんですよ。「分けたらクリアになる」って側面がないとも言えないけど、そういう分類に労力を使うのはかなりバカバカしい。「論理とはなにか？」で紹介したストラスバーガー（Lutz Strassburger）は、ナントカ論理とかカントカ論とかの区別は捨象した上で、「論理とはプレ順序集合」「論理とは圏…

…8日）のエントリー「古典論理は可換環論なんだよ」へのトラックバック、「なんだろな」とか病み上がりのモンヤリ頭でたどってみました。ンガッ。id:tri_iro さん、この書きっぷり、こりゃ基礎論のプロですよね -- 「ゲーデルの不完全性定理を代数学を使って表現してみた」僕は、古典論理と可換環の関係を、初等的計算を愚直にガリゴリやれば分かる範囲でとりあえず書いてみたのですが、tri_iroさんがより発展的で深い内容、なんと2007年の結果を示唆するようなところまで書いてくれました…

…216889463 古典論理は可換環論なんだよ http://d.hatena.ne.jp/m-hiyama/20061028/1162014043 自分のこと(株)はてなの近藤社長批判みたいだけど、敵意を持ってるわけじゃありません。近藤さんが、ちょうど僕と対極的な気質の持ち主のようなので、対照的に自分のことを語っているんです。 「バカなこと」は難しい http://d.hatena.ne.jp/m-hiyama/20051102/1130912889 いつまでも惑い悟れない…

…、そこで使われている古典的な定理（ヘンゼルの補題というらしい）の解釈がまちがっている気配ですね。Benschopさんが反論を展開するのか、このまま議論が終結しちゃうかわかりませんが。[追記 date="翌日"]英語がよくわからんけど、雰囲気だけ訳。Rather then は Rather than のtypoと解釈。 John Baez（ブログ主催者） こんなにも重大な（しかも2つ）の結果を証明したと誰かが主張したとき、その誰かさんは、このテのコメントを見て考えを改めるなんて…

…論を考えてみました。古典論理のシーケント計算をまねて作ったので自動的検証のアルゴリズムとかには向きません。とりあえず、人間が（って、僕だけど）紙と鉛筆で使う用途つうことで。とはいえ、人間用のシーケント計算としても、いまひとつシックリこない点が残っています。まーなんだ、現時点でもスナップショットということで書いておきますわ。後でゴッソリ修正するはめになるかも。内容： モデル シーケントの構文 推論規則：公理 推論規則：ガードとマーク 推論規則：構造規則 推論規則：論理規則 それ…

…多寡＜たか＞によって古典論理と直観主義的論理、その他のナンタラ論理に別れるし、様相記号や、さらにもっと目新しい論理記号を入れた体系もあります。（形式的）証明もヒルベルト方式、ゲンツェン方式（シーケント計算）、タブロー方式なんてのがありますね。こういう多様性は「論理の豊饒＜ほうじょう＞さ」を示すものでしょうが、僕は、「なんだか博物学・分類学みたいだなー」とも感じます。ストラスバーガーの質問と答えは、こういう不満感を多少は解消してくれます。 複数の演繹系を比較するのは良い練習問題…

…運動軌跡だと思うと、古典的あるいは相対論的な時空図やファインマン図だとも解釈できます。ここらへんが、論理の証明論が、結び目のトポロジーや場の量子論と直結する背景だろうと思います。（実はよくは分かってないけど、「バエズとステイのロゼッタストーン論文と現代のヒエログリフ」とかも参照。）常識的な省略とマクロ推論規則Kuwataレポートに戻って、Kuwataさん曰く： この図[檜山注：連立1次方程式を解く図]を見てドン引きしてる人もいるかもしれないけど、セミナーではマジでこういう図を…

…、論理の演繹定理、（古典的であれ現代的であれ）テンソル計算、結び目理論のライデマイスター移動やその拡張、量子テレポーテーションなども同様な現象として括れます。 論理とはなにか？ (4:完) -- 論理から圏へ コンパクト閉圏と奇妙な論理 ベル状態、少し分かった、がやっぱりよくは分からん 量子テレポーテーションのお絵描き ラムダ計算というものを考える動機。数学でも必要になってくるものなのか。 計算技法として使うのはインフォーマルラムダ計算のほうでしょう。例えば： ラムダ計算とイ…

…多くの人が行います。古典論理の立場からいうと「間違い」なんですが、多くの人が使っているし、それが通用する場面もあるということは、人間にとってなにかしらの「自然さ」があるように思えます。「自然だ」とは、このテの認識／推論による言明を言ってるほうも聞いたほうも、特に違和感なく済ましてしまうケースが多々ある、と、まーそんなことです。記述の道具として古典論理を使うことにして（あくまで記述のためね）、k(x) は「xは九州出身」、h(x) は「xは髭が濃い」を意味するとします。確認され…

…しい方法や、多項式の古典代数学が使われます。この手法を適用するなら、不動点方程式で定義される再帰的領域（の同型）に関する問題は、多項式イデアルの問題に翻訳されます。例えば、グレブナー基底を使った計算代数システムでイデアルの問題を解いてしまえば、領域の同型が保証されます。二分木のデータ領域Tは、T = I + T2 を満たすことから、データ領域の圏のなかで、「1の6乗根」の役割を演じていることになります。よって、I（単元集合）とT（二分木集合）から、足し算（直和）と掛け算（直積…

…係を書いておきます。古典論理論理記号（「論理記号のいろいろ」参照）として次を採用します。 ∧ 連言（かつ） ∨ 選言 （または） ¬ 否定（でない） ⊃ 含意 （ならば） T 真 記号「|-」は、証明可能性です。証明可能性に関しては「論理とはなにか？」や「さまざまな「ならば」達」で説明してます。まずは古典論理を考えることにして、次のような法則はお馴染みでしょう。 (A∧B)∧C ≡ A∧(B∧C) （∧の結合律） T∧A ≡ A∧T ≡ A （真との連言） ¬¬A ≡ A （…

…け算も保存する元x^」を対応付けることができます。x←→x^ という対応は、次の意味で同型です。 U*を最大値ノルムでノルム環とみなし、掛け算も保存する連続線形汎関数の全体をM(U*)とすると、x←→x^ の対応は位相も込めて同型を与える。 有限次元ベクトル空間のときとはドエラク事情が違うのですが、それでも僕は、ベクトル空間の同型 U←→U** と、すぐ上の事実（たぶんゲルファンドによる）は親類のような気がします。このテの双対性は「古典論理は可換環論なんだよ」でも書きました。

…たかった内容自体は「古典論理は可換環論なんだよ」にまとめて書いてあります。）上で出てきた「6と8から、足し算と引き算で作り出せる数」の全体は整数のイデアルに他なりません。一方、「足し算だけで作り出せる数」の全体のほうは半環イデアル（an ideal in semiring*1）と呼ばれます。引き算を使わなくても、大差ない概念や用語はまーいいとして、適当に2つの正整数を選んで、足し算だけで作り出せる数と足し算／引き算を使って作り出せる数を比べてみてください。いくつかの例にあたれ…

…から」という根拠が、古典論理の恒真命題や科学（もちろん通常科学 :-)）的法則のような確実性を持つわけではありませんが、日常的説得力なら持つでしょう。危険性を指摘するなら、「Aさんが言うのだから」が論理的真や科学的事実に匹敵するがごとき扱いを受けることでしょう -- ¬∃A.(∀α.(who(α) = A ⇒ |= α)) *1:この話では、因果関係の方向性は重要ではなくて、「木の葉のゆれ」と「風」が同時に起こることからちゃんと推論ができます。 *2:モーダスポネンスに出てく…

…足を書きました。） 古典論理は可換環論なんだよ は、セオリーの代数的な扱いです（プログラミングの話には、たいてい不要）。その手短なまとめとしては、 仕様、公理系、セオリー に対応表があります。●インターフェースの実例次のインターフェース（＝指標）を考えます。 interface AB { int a(); void b(); }それと、次のインターフェース： interface IJK { boolean i(); void j(); int k(); }こんなものを見せられ…

…グリフ（象形文字）、古典ギリシア語。そのため、ヒエログリフの解読に役立ったとのこと。 （写真：Wikipedia「ロゼッタ・ストーン」より）そんな話に続けてバエズ／ステイ曰く： At present, the deductive systems in mathematical logic look like hieroglyphs to most physicists. Similarly, quantum field theory is Greek to most comp…

…です。でもね、例えば古典論理の論法（reasoning ）を理解しようとすると、神様を仮定せざるをえない、神様なしでは成立しえない論法だと思うのです。とはいえ、信仰・信心とは無関係に、人間にはできないことをやり遂げる能力を有する存在を受け入れれば、それで済むハナシです。「神様」より「超越者」といったほうが少しは宗教臭さがぬけるかな？デスパレートな関数たち [追記 date="2008-05-10"] これを書いた当時、「デスパレートな妻たち」という海外ドラマをNHKで放映して…

…らへんから、集合論的な関数／部分関数と、関数や部分関数を定義するプログラム、そのプログラムの実行などの区別が曖昧になります。厳密に区別すると煩雑になりすぎるので適当に書きますから、適当に解釈してください。 *2:JavaScriptだとスタックとヒープの区別がありませんが。 *3:⊥は「ボトム」と呼びます。ボトムを上下逆にした形Tはトップです。異常事態をTで表すときもありますが、それは趣味の問題です。 *4:古典的なand/or以外に短絡的and/orも考えることができます。

… = Φ) について言っているのでしょうが、含意の左側が Φ≠Φ なんだから、これは単に「矛盾 ⇒ なんでもいい」（この場合は「矛盾 ⇒ 矛盾」）という、古典論理では当たり前のことを言っているに過ぎません。「お日様が西から昇るんだから、なんでもあり」というバカボンのパパの論法ですね。 言いたいことはわからんでもないけど 僕は、何を言いたいのかサッパリわからないなぁ。 *1:したがって、引用文がなにか特殊な文脈内で語られている、という状況は（仮にあったとしても）無視しています。

…督のこの論法(?)、古典論理の法則を使っています（本人がそう思っているかどうかは別）。「Aではない」（Aの否定）と「Aならば矛盾」が同じ意味だという法則ね -- これは論理のなかでも分かりにくいと不評な部分ですが、日常会話でけっこう使ったりしてるんですよ。古典論理の否定と矛盾まず、問題の古典論理の法則とは； 「Aではない」と「Aならば矛盾」は論理的に同値だという法則です。「Aではない」と「Aならば矛盾」が主張している内容に変わりはないのです。「ではない」を記号¬で、「ならば」…

…んです。それで結局、古典論理（ブール代数）も直観論理（ハイティング代数）もデカルト閉圏の枠組みで扱うことが可能なわけ（「可能」なのであって、それが良いかどうかは別問題）。古典／直観論理における A∧B |- A （A∧Bを仮定してAを演繹できる）とか、A∧B⊃A が正しい命題だとかの話は、ブール／ハイティング代数における対応する話に翻訳できます。それをデカルト閉圏の枠組みで眺めてやると、射影p1の性質に他ならない。と、そういうことです。これで、太陽光線の影を比喩としてはじまっ…

…なると、人間の論理（古典論理*1や直観論理）から見ていくら奇妙でも、自然現象の論理は線形論理になっていると認めざるをえないようです。そして、計算現象の論理もどうも線形論理みたいなのです。その理由のひとつは、コンピュータによる計算が実際にリソースに敏感だとういうこと。また別な理由として、計算も結局は自然現象（物理現象）に支えられているという事実があるでしょう。手作業で行う計算でも、紙がなくなったり鉛筆が折れたら中断しちゃうし、やってる人間が疲労して間違ったりと、確かにリソースに…

…直観主義論理の証明は古典論理の証明とみなせます。こういった相互関係は、圏（として定式化した論理）のあいだの関手として表現可能です。2つの論理が事実上同じことはよくあるのですが、この事態は、“2つの圏が同値である”という形でうまいこと表現できます。圏の同値性には自然変換が必要なので、系統的な命題の書き換えとしての自然変換も“自然に”出現します。「証明とは何か？」とは何か？最後に、ストラスバーガーの問題意識を（僕が理解できる範囲で）少しだけ説明しましょう。論理と圏の対応関係がうま…

「古典論理は可換環論なんだよ」のなかに、 愚直にrudimentary calculationを実行してください。 これまたひたすら単純計算をすれば、… これも、紙と鉛筆と手で単純計算あるのみ。 という表現がありますが、僕は実際には計算してなかったので、やってみました（疲れた）。計算で確認すべきことは： MICR（乗法的ベキ等可換環）からBL（ブール束）がちゃんと作れること BLからMICRがちゃんと作れること MICR→BL→MICRでもとに戻ること BL→MICR→BLで…