会場に私は30分遅れで到着、18時半より21時半まで。参加者3人、終了30分前にN君が到着する。p.12第2段落-p.15第2段落。 不完全性の話、証明不可能な算術の命題やCHに関するコーエンの証明など。不完全性定理については（わざわざ）ロッサー・タルスキ・モス…

よく晴れる。相変わらず10月とは思えない暑さ。 起床は8時、とても眠い。郵便局に寄ってから出勤。コード書きの続き、午後に上司と打ち合わせ。昨日の Type が Set1 になる件は、Set1 のまま続行することになった。17時に退所、大学へ。読書会出席後、帰宅は…

現在、Agda2で某論理体系を実装中、本日からタイプチェックを始めた。論理体系なので、列計算を定義したいと考えるのは自然な考えでしょう。というわけで、命題の列を定義しようとしたのだが・・・ Agdaのベースとなる直観主義的タイプ理論では、Proposition…

雨。気温が高く、湿度も高い。 起床は8時15分。とても眠い。出勤してコード書き。本日から実装に入るが、直観主義タイプ理論の型の厳しさに泣く（KTさん、ありがとうございます）。いろいろで遅くなり、21時まで残る。22時半に帰宅、夕食はキャベツのオリー…

1997年、まだスカパーに入っていたのでBBCニュースをよく見ていた。アフリカのシエラレオネで無能な政府軍が壊滅し、残虐な反乱軍が首都に侵攻直前、大虐殺の危機だというニュースを見た直後、なぜか反乱軍が退却し危機が回避されたというニュースを聞いて、…

よく晴れた日、気温も10月末とは思えない暖かさ。 起床は8時15分、出勤してコーディングと本読み。夕方は談話会、台湾の教授。終了後も読書。一日中 de Bruijn representation について悩むが、少しはわかった気がする。20時半に退所。 帰宅は22時、Ib君が先…

10月22日付けのエントリにつきまして、Teoさんからご質問をいただきました。ありがとうございます。長くなりそうなのでこちらで回答させていただきたいと思います。 (i)論理と理論の違いとは？ 確かにこの両者には「主観的」には全然異なるものですが、その…

よく晴れる。10月後半とは思えない陽気。 起床は11時半、昼食は昨日の残り物のサバ寿司。本を読んだりエントリを書いたりして過ごす。21時に夕食、豚バラ肉とトマトのパスタ。

東京は台風とか。こちらも湿度が高く、強い風が吹く。 起床は12時、義父母が姪二人を連れてくる。昼食は店屋物、15時頃まで。 18時より、Cの友人二人と、大学の後輩二人を呼んで簡易お茶会。 フローリングなのでなんちゃってお茶会ではあるが。 夕食はCの実…

寝ている間に非常に強い雨が降る。一日中湿度が高い。 起床は8時15分、本日はCが健康診断のため、途中まで一緒に出勤。コード書き、夕方から講演会（システム開発における形式的技法の導入例）と懇親会。その後Ktさんと議論をしていて遅くなり、21時に退所。…

気温は低め、しかし湿度が高い。8時半に起床、出勤してコード書き。会議の後、deep embedding/shallow embeddingの違いについてktさんに教えていただく。夕方に談話会。その後は書類等、21時半まで。帰宅は23時。

よく晴れる。起床は8時15分、出勤してコード書きと打ち合わせ。早退して読書会に向かうが、会場に着くとh師から本日は急遽中止になったと知らされる。がっかり。雑談をして20時に帰宅。 夕食はモツ鍋、久しぶりに調理を手伝う。缶ビールを二本あけ、ぼーっと…

起床は8時半、眠い。出勤してコード書き。Agda2のプログラム例を探す。帰宅は21時15分、夕食はタリアッテレのクリームソース。

昨日の不完全性定理についてのエントリ、短時間でお答えがいただけるとは思っていませんでした（(mt)^2さん、ありがとうございます）。今回は、いただいた答えの中で、気になった点を時間がないので二カ所だけコメントしたいと思います。 (3.1) 純構文論的性…

起床は9時、出勤して論文読みとコード書き、20時半まで、帰宅は22時頃。夕食はサツマイモのスープと、ピーマンとウィンナーのトマトソースパスタ。

以前、ラッセル・パラドックスへの証明論的アプローチ（グリシン論理など）を取り扱った際に忘れていた話を紹介いたします。もう一つ、古典論理を認めるものの、ある特別な種類の証明図（正規化できない証明）を証明として認めないことにより、ラッセル・パ…

前回はファジイ論理と多値論理の関係について取り上げました。今回は、ファジイ論理の数学的な定義と、ファジイ論理上の集合論について手短にご紹介したいと思います。 （狭い意味での）ファジイ論理とは 他の業界ではともかく、数理論理学におけるファジイ…

h師の日記経由。朝日新聞 の昨日の朝刊28面より。 「リスクに対処するための金融商品自身が新たなリスクになる」という論文のロジックは、数学や論理学の世界で有名な「ゲーデルの不完全性定理」と関係しているのではないか、と私は考えてきた。 「私の発言…

よく晴れる。しかし空気が冷たい。起床は11時。Cとうどん屋に行き昼食。 阪急駅前の本屋とスーパーによって帰る。

晴れているが、気温は低めで、少し風邪気味。起床は12時半、一日休養。今週は疲れました。夕食は二日目のカレー。 来ていただいた方には申し訳ありません。「ラッセル・パラドックス」の続きの更新は明日になります、ご了承ください。

いつのまにか、私は様相述語論理の専門家ということになってしまった。内容は面白い。っていうか Kripke frame が役に立たない。だから証明論的な体系をコンピューター上の定理証明支援系(Agda)に実装することになる。・・・これって、「意味論」と呼んでい…

朝から雨、昼にかけて強くなる。起床は9時、日ごとに時間が遅くなる。出勤して雑用と論文読み、20時半まで。帰る頃には雨があがっていた。 画像がぼけていてわかりにくいが、Oxford Textbooks of Logic は、通称 OTL らしく、背表紙に OTL と銘打ってあるの…

日差しが強いが気温は低め。しかし湿度が低いので動くと汗ばむ。 起床は8時半、非常に眠い。出勤してコード書き、それから会議と談話会。残って書類を書いているうちに21時になってしまう。梅田経由で23時頃に帰宅。夕食はローストビーフ・サンドイッチとマ…

19時から22時、参加者3人。p.10第2段落-p.12第1段落。 Putnumは Syntaxとしてのmodal logic を考え、Box （必然性）をprimitiveとして取る。Putnum はどんな概念を抽象化してこの Box を導入したのか、Quine流Logical Validity と証明可能性のどちらだと解釈…

天気は晴れ、日差しも強めで少し汗ばむ。所内ではTシャツで過ごす。起床は8時半。出勤してコード書き。午後に打ち合わせ、緊張していたが問題なく終了。それから、先日の文字化けの原因についてTyさんに聞いたところ、NTemacsのバージョンの問題らしい。 帰…

いつもCは6時に起きるが、本日は目が覚めたら7時だったが、それでも7時13分の電車に飛び乗ったそうだ。家から駅まで歩いて15分、いったいどうやったんだろうか。 起床は8時、病院に行って健康診断結果を受け取ってから出勤。Agda2のインストールの続きをする…

起床は8時、よく寝た。出勤途中に健康診断のため研究所近くの市立病院に行く。月曜なので混んでいて、午前中いっぱいを棒に振る。午後から出勤、Agda2をインストールする。今日はCが会社の歓迎会のため、21時近くまで残り、夕食を食べて22時半に帰宅。

先日は、[0,1]の実数値を真理値としてとるウカシェーヴィチ無限値述語論理では、包括原理を仮定しても無矛盾であるという話をご紹介しました。今回は、それと非常に紛らわしいファジイ論理一般の話をご紹介しましょう。 ファジイ論理・・・狭い意味と広い意…

曇り空、気温も低め。起床は11時半。昼食は久しぶりにプッタネスカ。夕方CとJR駅まで出かけ、ラーメン屋で夕食。商店街の肉屋によって帰る。帰宅後Cと録画した「絶望先生」を最後まで見る。

前回は、ウカシェーヴィチ3値論理 L3 において包括原理を仮定した場合、ラッセルのパラドックスだけなら解決できるが、莫少揆のパラドックスにより結局矛盾を導いてしまう、という話を紹介いたしました。今回は、その続きとして、ウカシェーヴィチ3値論理を…