Mathematical Logic Advent Calendar 2023 10日目の記事として線形論理の簡単な紹介を書きました！ 論理学の知識がない人でも読めます。線形型システムの話もちょっと書いてますのでプログラマの方にもオススメです！ drive.google.com

久しぶりに雑誌『現代思想』を隅々まで読みまっせ（「隅々」は言い過ぎだけど）。「〈計算〉の世界」という興味深い特集があったので。私は線形論理という計算機科学の文脈から出現した論理を研究しているわけだけど、論理の哲学というと言語との関連から語…

古典命題論理は決定可能である。すなわち、与えられた命題(あるいはシークエント)が任意のモデルで真どうか、もしくは証明可能かどうかを判定するアルゴリズムが存在する。わが研究室ではこれを↓の小野寛晰先生の解説論文で勉強するのが伝統らしいので読んだ…

慶應大学で開催されたジャン=イヴ・ジラール先生のセミナーに自力で行ってきた。初めてお会いした。私にとってのジラール先生はハロプロ志望の少女にとってのつんく♂のようなものである。緊張した。しかし持っていったご著書にサインも頂けたので満足。トゥ…

やりました。 drive.google.com のところがもう少し上手く書けないものかという感じがあるけれどまあまあまあ（追記：直してみました）。 （追記）いろいろ間違いや不備が見つかっているのであまり信じないように。 The Blind Spot: Lectures on Logic 作者:…

ランキング参加中フランス語を学ぶ ↓これの続き。 cut-elimination.hatenablog.com ランガールことジラール先生の「マスタード・ウォッチ」本編を読んだ。4ページだし英語なのですぐに(ある程度)読めるが、ちょっと私の知らないロジックの難しい話題も出てき…

ジャン=イヴ・ジラール(Jean-Yves Girard)先生の「マスタード・ウォッチ 時間と食べ物に対する統合的アプローチ」（英題"Mustard watches, an integrated approach to time and food"、仏題"Les montres à moutarde, une approche intégrée au temps et à la…

↓これの続きでごんす。 cut-elimination.hatenablog.com フィルカルの矢田部俊介「哲学的論理学入門」第3回と最終第4回を読みました。 フィルカル Vol. 5, No. 3―分析哲学と文化をつなぐ― 作者:木下頌子,和泉 悠,八重樫 徹,三木那由他,峯島宏次,飯塚理恵,佐…

ワシって自分が専門的にやってる分野はごく狭い範囲しか読んでいなくて関係ない哲学分野の事ばかり書いているなあと思い、自分の専門*1である線形論理（を中心とした証明論と計算の理論）に近い所の読書をする事にした。 リーディングス 数学の哲学―ゲーデル…

drive.google.com ジラール先生の論文"Locus Solum"をまだ読んでいる途中だが、ルディクスについて解った事だけ纏めておく。（追記：後で読み返したらいろいろ微妙な点があるので注意！） ↓これに載っている照井先生の論文でルディクスの存在を知ったと思う…

drive.google.com フル線形論理のカット除去定理の証明をそこそこ詳しく書きました…。古典論理や直観主義論理のカット除去定理をある程度知っている人向け。 ↓参照文献 数理論理学 (現代基礎数学) 作者:鹿島 亮 朝倉書店 Amazon Lectures on Linear Logic (L…

drive.google.com おるうぇ (@Alwe Logic@twitter) さん主催の「数学基礎論アドベントカレンダー」の22日目の記事です。私は哲学科の学生です。あまり数学基礎論ぽくなくてごめんなさい。 予備知識はシーケント計算とカット除去定理とカリー=ハワード同型を…

ちょっとした思い付きです。 ネッカー・キューブというのは誰しも一度は見たことがあるであろう錯視図である。 ja.wikipedia.org 表示されてるかな？ これは一つの平面図形が二通りの見え方をする、二通りの立方体に見える、という錯視である。一つの感覚入…

前回こんなことを書いたけれど更に完全性定理について cut-elimination.hatenablog.com Troelstra先生の本を読んで線形論理の代数的意味論の完全性定理を勉強しているところなのだけれど、 Lectures on Linear Logic (Lecture Notes Book 29) (English Editi…

Troelstra先生の"Lectures on Linear Logic"を読んで線形論理の代数的意味論を勉強している。 Lectures on Linear Logic (Lecture Notes Book 29) (English Edition) 作者:Troelstra, A. S. Center for the Study of Language and Inf Amazon いま本では大幅…

↓これの続きです。 cut-elimination.hatenablog.com 今回は安定関数が出てくるはずです。 用語の整理 いろいろ用語、記法が出てきている。 用語・記法：整合空間 の要素を の点(point)という。 のクリークを整合部分集合(coherence subset)とも言う。点とは…

↓これの続きっちゃあ続きである。 cut-elimination.hatenablog.com "Proofs and Types"を読んでいくシリーズだったが、第7章のSystem Tの導入をちょっと飛ばして第8章の整合空間(coherence space)を詳細に読みたいのよ。 整合空間から線形論理を解説している…

↓これの続きでこざる。 cut-elimination.hatenablog.com シーケント計算 シーケント計算は自然演繹ほど計算との対応が明確ではないとのことだった。しかしPROLOGの基礎になっていたり自動定理証明に使われるタブローの一般化でもあるという。これは知らなん…

↓これの続きでっせ。 cut-elimination.hatenablog.com 3章は型とは何かという哲学的な考察を含んでいる。4章は正規化定理を解説したテクニカルな内容である。 Chapter 3 カリー=ハワード同型 命題を型と対応させる。型付項のシステムにおいても sense と den…

この本で線形論理の勉強をしているよ。 Lectures on Linear Logic (Lecture Notes Book 29) (English Edition) 作者:Troelstra, A. S. Center for the Study of Language and Inf Amazon 加法も乗法も量化子も指数も全部入れたフル線形論理のカット除去定理…

私は現代最高のロジシャンはJean-Yves Girardだとガチで思っている。 ジラール先生の論文や本は、理論的なものであっても個人の論理に対する考えが混入していることがよくあるように思う。時には本線のテクニカルな議論からやや離れたお話のようなことが書か…

ランキング参加中フランス語を学ぶ ジャン=イヴ・ジラール先生は大量の映画短評を書いておられる。ジラール先生のサイトの"alter ego"というところから読める。 girard.perso.math.cnrs.fr オルター・エゴというだけあって、Yann-Joachim Ringardという変名…

ルディクスに興味があるのだけれどあんまりよくわからない*1。わかったことをメモしておく。 ジラール先生が最初に提案したのは1999年の論文らしいのだが、本格的に論じられているのは2001年の"Locus Solum"という長い論文である。こちらのほうが基本文献と…

デカく構えたタイトル！！ 後期に専門が違う人向けに研究の説明をする演習があるようなので、ロジックが専門でない人向けの線形論理の解説を考えたい。 自然演繹からシーケント計算へ 論理学の入門講義をとったことがある人は多そうなので、自然演繹から入っ…