当ブログは論理学を中心とした哲学・数学・計算機科学の勉強記録と、アニメの批評・感想を中心に書いております。おすすめの記事は以下です。
cut-elimination.hatenablog.com
アニメにもジェンダーやフェミニズムを考えるうえで示唆に富んだ作品はたくさんありますよ、という記事です。いろいろな作品を紹介しています。本当の目的はアニメ一般に対する「前時代的」という批判への反論です。私の調べが進むにつれてアップデートされていきます。
私の研究対象である線形論理というのの入門解説です。
cut-elimination.hatenablog.com
cut-elimination.hatenablog.com
藤井聡太先生の脳内には将棋盤がないという説を、様々なインタビューや棋士の証言をもとに検証しています。
cut-elimination.hatenablog.com
マンガ『チェンソーマン』第43話に出てくるロシア語の歌を翻訳しています。元ネタはなんなのかもちょいと考察しています。
あとはカテゴリーから見てみてください。
けっこうおもしろかった！
意外と客が入っていた！
私は昔のテレビアニメ版の、出﨑統監督による後半のファンである（全40話のうち19話から出﨑監督に代わる）。
cut-elimination.hatenablog.com
出﨑版には独特のアングラ感がある。謎の吟遊詩人が出てきたりとか。しかし今回の新作映画はもっとキラキラしている。なんかミュージカルだし（声優って歌うまいよね）。また宮殿内の装飾がかなり細かく描かれていて、色が明るい。当時のベルサイユはあれくらいあざやかだったのかもしれない（知らんけど）。
尺の都合上、前半がかなり駆け足でアントワネットの葛藤は省略される。デュバリーとかポリニャック夫人とかちょっとしか出てこない。しかしこれはこれでいいのかもしれない。ぶっちゃけ原作も旧テレビアニメも、おもしろいのは衛兵隊〜革命あたりなので。ただしロザリーもチラッとしか出ないし黒い騎士の話もなかったので、オスカルが革命側につく動機は弱めかも。
フランス革命の原因というのは、本作とか教科書では王宮や貴族の贅沢に庶民が怒ったからという感じだが、実際はどうなのだろう。王宮の財政と庶民の貧しさは別のような気がする。こういう歴史のなかの経済を調べるとおもしろそうである。ルイ16世にアベノミクスみたいな経済政策があったら革命は起きなかったのだろうか。というか革命のあと庶民の暮らしはよくなったのだろうか。戦争になったはずだが。
安倍晋三の一族とか麻生太郎の一族とか、私にはベルサイユの貴族みたいに見える。物価高がもっと進んでも対策が取られなかったら、日本でも革命が起きるかも。
（前回はこちら）
札幌に来る外国人観光客にムカついていた加藤晋太郎だったが、特に嫌なのが晋太郎の通うH大学のキャンパスに来る人たちである。キャンパスは広大なので雪遊びができる。それ目当てで外国人が集まってくる。しかし、学ぶために来ている学生たちが忙しなく歩いているその横で、雪だるまを作ったり雪合戦をしたりとか、失礼ではないか。晋太郎はそんなふうに思っている。しかもキャンパスは入場料を取らないわけで、金が掛からないから観光地に選ばれているのではないか。それは入学料と授業料を払っている我々を舐めているだろう、来るならちゃんと大学グッズを買ったりして金を落としていけよ、とか。
この「金を落とせ」という表現はよく聴くが、晋太郎は経済学など学んだこともないので、その正確な意味はよくわかっていない。なんかそう思っておけば、自分のなかの差別感情が経済の問題に落とし込まれて正当化されるように感じているだけなのであった。
さらに勢いで↓これの続き。
cut-elimination.hatenablog.com
今回はJean-Baptiste Joinet, Thomas Seiller "From abstraction and indiscernibility to classification and types: revisiting Hermann Weyl’s theory of ideal elements"という論文をちょっと紹介。
Joinet先生は線形論理の世界では昔から有名なベテランである。Seiller先生は前にも論文を紹介したが、GoI(相互作用の幾何学)や超越論的シンタクスなど現代的な線形論理・ジラール理論を研究している人。どちらもフランス人だが、本論文は日本科学哲学会の雑誌『科学哲学』に掲載された。科学哲学会での企画がもとになったらしい。
本論文は「型」についての考え方を論じたもの。前回の規則のパラドクス論文でも前々回の型なし証明論の論文でもそうだったが、ジラール学派では型（あるいは論理定項）を、なんらかの証明(っぽいもの)との相互作用によって定義する。「相互作用」「計算の停止」を表す関係や集合を定め、相互作用して停止するような相手を持っているものが型とされるのである。これについてテクニカルな細部が論じられている。前回の論文でもそうだったが、なぜかテクニカルな議論はどれも相意味論(phase semantics)と同じなので、それを専門にしている私には易しかった*1。
本論文では、そうした型の考え方の根拠をヘルマン・ワイルの哲学的理論に求める。ヘルマン・ワイルは20世紀前半に活躍した数学者・数理物理学者で、数学の哲学への影響も大きい。ヒルベルトの弟子だが直観主義の論者として有名である。そのワイルが「分類(classification)」について論じたものがあり、それがジラール学派の型概念に近いようである。というかワイルの理論がジラール理論によってもっとすっきりと表現できるらしい。私は知らないことだらけだったのでワイル解釈としてどうなのかはわからない。しかしGoIやルディクスや超越論的シンタクスでよくでてくる「相互作用における振る舞いが同じなものは識別できないので同一視する」という考え方がワイルにも見られるらしい。ジラール先生は自説を補強するのによくカントやヘーゲルを持ち出すが、それよりは筋が良さそうである。
歴史についても要勉強であるなあ。
*1:は
を含む最小の型というのは知らなかったので勉強になった……
肛門の調子が悪くてしばらく映画をひかえていた。痛みが引いてきたのでひさびさに劇場へ。
本作は、ガンダムジークアクスに席数を奪われているものの、ジークアクスに引けを取らないくらいヒットしているらしい。私が行った回も小さい箱ながらめちゃくちゃ入っていた。男女同じくらいで十代二十代の若い人ばかり。
観て驚いたのだが、なにがなんだかまったくわからなかった。キャラクターが誰が誰かわからないし、世界観も物語もなにも理解できない。プロセカという初音ミクのゲームがあることくらいしか知らなかった私は、完全にお呼びじゃなかったっぽい。もっと予習しておくのだった。アニメも以前にいくつか作られていたらしい。見ておくべきだった（どこで見れるのかわからないが）。
それにしても映画という媒体でこんなにも一見さんお断りで作るのはすごい攻めの姿勢である。i☆Risやすとぷりの映画は知らないなりに楽しめたのだが、それすらなかった。
cut-elimination.hatenablog.com
cut-elimination.hatenablog.com
それでこれだけヒットしているのだから、プロセカってすごいコンテンツなのだなあ。まったく意識していなかった。Z世代のことなにもわかっていなかった。
前に「型なし証明論」について紹介したので、勢いでもう一つ線形論理を使った哲学の論文を読んで紹介しまっせ。
cut-elimination.hatenablog.com
Paolo Pistone "Rule-Following and the Limits of Formalization: Wittgenstein’s Considerations Through the Lens of Logic"という論文（私が読んだのはもしかしたらプレプリントかもしれない）。
著者はイタリア出身でいまはフランスにいるらしい。テクニカルな研究をしているが哲学にも精通している模様。
記事のタイトルに「超越論的シンタクス」を掲げたが、本論文では星座などの超越論的シンタクスの概念は登場しない。GoI（相互作用の幾何学）までである。しかし発想は超越論的シンタクス的である。また文中ちらほら「超越論的シンタクス」という語も出てきている。
本論文のテーマは、ウィトゲンシュタインやルイス・キャロルの著作に登場する規則のパラドクスである（クリプキのやつとは違う、と思う）。例えば、と
から
を導いてよい、というモーダス・ポーネンスの規則を考えよう。なぜ、いかにしてこの規則に従うのかと考えると、
という公理もしくは定理があり、それと
と
という前提から
が導かれるのだ、としたくなる。しかしこの推論にもモーダス・ポーネンスが使われていて、議論は無限後退してしまう。じゃあなぜ我々は規則に従えるのか？ とパラドクスになる。
この問題に、前回紹介した文献と同じように、やはり計算、それも相互作用としての計算で挑むのである。規則に従うことが成功するのは、規則を表す論理式の証明と前提=入力とが相互作用し、その相互作用的計算が停止するときと解釈される。
相互作用を定義するにはどうするか。このあたりは前回の文献と同じような議論になる。ただしこの論文はモチベーションがわかりやすい。本論文で明確に説明されているのは、論理式や証明から相互作用を定義するのではなく、相互作用が上手くいくようなものを論理式=型や証明と定義するということである。
ちょっとテクニカルな細部もメモしておく。停止を表す集合を任意に取る。相互作用演算
も定義しておく。
が型であるのは、
となる
が存在するときである。すなわち、相互作用して停止する相手=テストを使って特徴づけられるものが型である。定義のなかで論理や規則についてなにも前提していないのがポイントである。この定義はテストのテストがもとの集合に含まれるというメリットもある（これは相意味論の「ファクト」の概念と一致している。何故かはわからないが）。このメリットは規則のパラドクスの解決に有用となる。
パラドクスは規則を以下のように説明することで解決する。まず次のように考える。
しかし入力をテストとして信用していいのだろうか？
議論は無限に循環しているが、後退はしていない。どちらかというと均衡のようなものになっている。また、先述の「テストのテストがもとの集合に含まれる」という性質から、この循環は閉じていることが言える。
ただし著者は、別に複雑性という問題が残るとしている。計算を正当化するためにそれ以上に複雑な議論がいるのではないか。例えばチャーチ数の指数演算の計算には指数スケールの簡約ステップが必要で、これでは問題を還元できていない。
この問題を回避するため、GoIを紹介している（本論文は行列を使ったGoI解釈の具体例が豊富でありがたい。しかしGoIの概念的説明ははしょってあるので、↓のEngさんの博論の5章を参照すべし）。まず線形論理はカット除去=相互作用の複雑さをコントロールできる（構造規則が制限されるので）。さらにGoIは、計算量の上界を、意図した時間・空間スケールに抑えることができる。超越論的シンタクスの今後も複雑性の議論が期待されるらしい。私は計算複雑性の議論は学びたてなので、今後GoIや超越論的シンタクスのそう言った側面も調べたい。Seiller先生がやっているはず。
cut-elimination.hatenablog.com
この論文の議論が正しいかどうか、規則のパラドクスについてもうちょと調べないと解決かどうかわからない。同じような提案はすでにあるかもしれない。
疑問として、計算の実行にも計算規則が必要でやはり無限後退するかも、という点がある。これは計算という概念に関する問題だと思う。
先日、一橋大学で↓こういうイベントがあった。
講演者の豊岡正庸さんは私の直の先輩にあたる。たいへん優秀な方で、分析哲学・哲学的論理学の世界では注目の存在である。
豊岡さんの講演のなかで線形論理やジラール先生に触れた箇所があり、それに関連する文献は私が少しお教えした。そうしたら豊岡さんは謝辞で私の名前を挙げてくだすった。それに対する私の気持ちが↓こちら。
きのう豊岡さんに謝辞で名前を挙げていただいて、売れてない芸人が売れてる先輩にテレビで名前を出してもらったときの気持ちがわかりました……
— 鈴木盲点潤(線形論理) (@cut_elimination) 2025年1月26日
きのう豊岡さんに謝辞で名前を挙げていただいて、売れてない芸人が売れてる先輩にテレビで名前を出してもらったときの気持ちがわかりました……
— 鈴木盲点潤(線形論理) (@cut_elimination) 2025年1月26日
このトゥイートはけっこうウケた。
で、私が豊岡さんにお教えして講演のなかで触れられていた文献にAlberto Naibo, Mattia Petrolo, Thomas Seiller "On the Computational Meaning of Axioms"というのがある（論文ではなくブックチャプターらしい）。今回の記事はこれをちょっと紹介する。どこかで発表or論文化するかもしれないので、ちょっとだけ。文献はSeiller先生の個人ページからダウンロード可。
全体のテーマは、ダメット=プラウィッツの推論主義（証明論的意味論）を乗り越えよう、ということになる。ダメット=プラウィッツの路線には、タイトルにあるような公理の意味を上手く扱えないという難点がある。ここでいう公理とは非論理的公理のことで、例としてペアの算術の公理なんかが挙げられている。こうした公理はいわば恣意的なものなので、「カノニカルな証明」などダメット=プラウィッツの道具が通用しないわけだ。
じゃあどうするかというと、計算論的な振る舞いを意味として与える。その際に取る方針が相互作用(interaction)としての計算の概念と「型なし証明論(untyped proof theory)」である。
ダメット=プラウィッツは論理的公理や推論規則を中心概念に据えて、論理定項の意味を考えていく。こうすると証明はトップダウンな規則適用で作られ、その一つ一つの規則と論理定項の意味とは切り離せない（たぶん）。
対して本文献は、論理定項や証明をプリミティブとしない。証明以前の構造であるパラ証明(paraproof)なるものを許し、パラ証明同士の相互作用によって起こる結果から、証明が定義される。カリー=ハワード同型対応により、証明はプログラムと、証明される論理式はプログラムの型と同一視できる*1。パラ証明は「なんの証明か」が定まっていない。つまり型=論理式が定まっていない。しかしそのおかげで、非論理的公理という破格なものも表現できる。またこの文献が示すのは、型がなくても計算における意味が定まるということである。それもトップダウン的でない相互作用的な計算を考えることによって定まる。
これらは線形論理の証明ネットを使って理論化される。ジラール先生のGoI (Geometry of Interaction)プロジェクトの後期やルディクス、最近の超越論的シンタクスといった理論も線形論理の証明論の応用として型なし証明論と同様の考え方が見られる。このあたりの解説はこの前の記事↓を参照。
cut-elimination.hatenablog.com
これらの理論では、証明ネット(証明構造)公理リンクをパラ証明、公理リンク以外の部分をテストすなわち反証の試みとみなす。型が事前に決まっていたらテストはひと通りに定まるが、型なしなので、テストはいくらでも変えられる。パラ証明とテスト(反証の試み)の相互作用を数学的に定義して、そこから型を定めるのである。
本文献は非論理的公理も扱うので、証明ネット(証明構造)の公理リンクだけではパラ証明に足りない。これを扱うために、興味深いことに、ルディクスのダイモーン規則を取り入れている（ダイモーンについても↑の記事を参照）。確かにダイモーン規則は非論理的公理とみなせる。ルディクスにおいてダイモーンが導入された動機は説明しがたいが、非論理的公理にまで議論が拡張できるのだなあと合点が言った。
本文献の後半では、Krivineの古典論理の実現可能性やダメットの哲学との比較がさらに検討されている。このへんは難しくてよくわかっていない。ただし、ジラール理論によく現れる「意味や真理はもとからあるのではなく、主張や反論(パラ証明とテスト)のやりとりのなかでできていく」という言語・論理観が論じられているのがありがたい（ジラールの哲学として論じられているわけではないが）。ジラール先生はヘーゲルを使ってそうした議論を補強しているが、もっとダメットのような英語圏の人との比較も気になるところなのである。ジラール先生は英語圏の論者にはめったに言及しないので。
（前回はこちら）
加藤晋太郎は、札幌の中心部、札幌駅のすぐ近くに住んでいる。最近そのあたりは外国人観光客が多い。晋太郎は感覚がアップデートできていないので、外国人という存在に対し普通にイラついてしまう。特にアジア圏からの観光客に。まさに「THE ジャップ」と言ったような、排外主義的でかつ他のアジア人を見下した態度である。
しかし晋太郎も少しはアップデートできているので、外国人に対してイラついてしまう排外主義的な自分にも嫌気がさしている。そのせいで二重にイラつく日々を送っている。
晋太郎の感覚としては、観光地に人が集まるのならばいいが、晋太郎の普段の生活の圏内に外国人観光客が集まってくるのには腹が立つ。最近の観光客は、高い店や施設でなく、チェーン店や晋太郎の通う大学キャンパスに出没する。普段の生活の場を珍しいところかのように見てバシャバシャ写真を撮ってはしゃぐさまにイラつくのであった。と考えれば晋太郎にも少しは理がある。
しかしそれだけではなぜ外国人にだけイラつくのか説明できていない。日本人の観光客だっているではないか。晋太郎はやはりダブスタ最低排外主義野郎なのだろうか。
まあそうである。だがもう少し具体的な理由を挙げておくと、外国人観光客はやたらと数が多く、また見た目が違って目立つというのがある。晋太郎が特にアジア系にイラつくのは、彼らの容姿は日本人ぽいのに雰囲気とか言語が違うからというのがあるだろう。そういう人らが生活圏に踏み込んでくると、晋太郎は弱ってしまう。
先述のとおり二重にイラついてしまうので、晋太郎の外出への意欲はまたしても下がるのだった。
