付近の山へハイキング。 最初はいい天気だったのだが… 徐々に曇ってきて、最後は土砂降りに。半数はその時点で脱落、しかし最後まで6人が残り、頂上に登ったのであった。おかげでズボンがビショビショです。

本日のトピックはTrさんの代数的意味論とその限界に関する講演。やっぱり面白い。

自分の発表が終わったので気もゆるみ、起床は7時半。午前は会議、昼食後はエクスカーション。夕食後はバンケット、遅くまでワインを飲む。

私の発表は16時20分より40分間。要旨は以下の通り。 Objective: to analyze the conception of truth (with a total truth predicate) in an arithmetic in Łukasiewicz infinite-values predicate logic ∀Ł. The problem: the modest liar paradox implies …

本日の午前は lecture series, 午後はチェコ組のファジイ数学案内 Real and Ideal Enitities in a Minimalist Constructive Foundation (2) (Giovanni Sambin) シリーズ二日目、今日は構成的数学のminimal な枠組で実際の数学（特に位相空間論）が展開できる…

起床は5時半、発表準備の続きと発表練習。8時過ぎに朝食、一日会議。夕方、"Round table" で「非古典数学は古典論理をメタ理論として展開されるべきか」を巡り、Avron vs Sambin のバトルロワイアル再び。 夜は「コンゴ」に行ってから就寝。

今回の会議は、実はスポンサー付きなんです。会社は "Becherovka company"…って、酒の会社じゃんか！そういえば、会議の配付資料に混じって、一人一本Becherovkaが支給されてたなぁ。 というわけで、今晩のパーティーは、Becherovka 社提供による、Becherovka…

会場は、ヘイニツァにあるかつての修道院で、 International Center for Spiritual Rehabilitationと言うところ。内部はかつての修道院の僧坊を塗り直したもの。かつては有名な修道院だったのだが、社会主義時代に弾圧にあい、修道僧らは逮捕され、施設は付…

午前8時45分スタート。 Opening 4月ごろになくなられた、Robert K Meyer さん（3月末に、この会議へ、招待講演の要旨を送ってきて、その後だったとか）に、みんなで黙祷。 Theories, Co-theories and Bi-theories in Non-Classical mathematics (Greg Restal…

起床は5時半、発表原稿書き。8時から朝食。午後は日本人枠の二人の講演を聴いた後、サボって原稿の修正をしていました。

チェコスロバキア建国の父、第一共和国初代大統領トーマス・マサリクの銅像。「城」の前の大広場に立ち、プラハ市内を見下ろしています。 マサリクとの対話―哲人大統領の生涯と思想作者: カレル・チャペック,Karel Capek,石川達夫出版社/メーカー: 成文社発…

「城」（現在は大統領官邸）の構内にある有名な大聖堂。 スパンドレル。

現在はチェコ科学アカデミーの会議場兼ゲストハウスとして使われているが、19世紀末に工業資本家の邸宅兼本社として建てられた建物である。 朝食用の食堂（昔は小会議室だったらしい）。 大会議室（三年前はここで学会があった）。 二階の、社長執務室の前に…

5時に起床、発表原稿書き。朝食後、邸内を散歩してからまた原稿書き。昼は近所のイタリア料理店に数人で行き、ビール二杯を飲む。その後日本人参加者4人でプラハ市内を散策。 城→国民劇場のルートで歩き、劇場近くのカフェで一服。その後中央駅にトラムで向…

出かける度に思い出すフレーズ。 今度はまたつい気取って、地外省の評議会で、ちっとも行きたくなんかないんだ、吾輩を餓鬼扱いして銀河に使い走りに出せるなどと勘違いされては迷惑だと、見得を切ってしまったが、実を言うと、図書館の敷居をまたいだ瞬間か…

国際会議で発表のため、チェコに出張します。帰国は7月4日（土）の予定です。その間、当Blogも更新がなかなか出来ないかもしれませんが、ご了承ください。

本日読み始め、機内で読了。「ふかえり」は、長門有希ではなく綾波レイなのか。

6時半起床、関空に行き、12時間弱でスキポールへ。機内では読書および発布用原稿準備。スキポールでは3時間飛行機を待つ。下画像は待合室。 それからプラハへ。空港でチェコの人に迎えに来ていただき、車で宿舎へ（三年前に宿泊した、懐かしのvilla lana）。…

話者はブラジルの矛盾許容論理の人。非常に面白い話でした。（後で追加します）

湿度の高い日。朝はよく晴れるが、夕方は雨模様。 午前中は久々に共同研究先と会議で大阪へ。カンを大分失っている。終了後、非常勤先の大学へ。授業をし、その後懇親会に出て帰宅。それからスーツケースのパッキングをする。

よく晴れる。朝は冷えるが、昼からは夏のよう。出勤して各種処理、面倒な話色々。 20時半に帰宅、夕食は麻婆茄子。録画した「ユーゴスラビア連邦の崩壊(1)」を見てから非常勤授業の準備。

曇り空。一日中パジャマ姿で原稿書き、他に非常勤授業の準備。夕食はナポリタン、その後スーツケースのパッキング。

暑い日、よく晴れる。洗濯をした後、家で20日の学会発表の準備（某学会はサボり）。なぜかTexshopで標準モードでBeamerの変換が出来てしまった。 夕食は豚ロース肉のオーブン蒸し。

先日MacBookAirにインストールしたAgda、とても快適に動くのだが、困ったことにtexモード（texコードを打ち込むとAquaemacs上でUnicodeの数学記号を出力する）の変換が出来ない。Ktさんに相談した結果、Texコードの変換機構は動いているが、emacsと日本語入…

湿度の高い日。出勤してコード書き、他に面倒なことが色々起こる。夜はCと梅田で待ち合わせ、「ストーク」でハンガリー風牛肉のソテーを食べる。大満足。帰宅は23時。

さて、S教授は、私が非常勤先で教えている授業（最小論理の自然演繹）の教科書の作者です。懇親会から帰る時に、授業について聞かれました。 (S)最近、授業はどうかね？ (ytb)ええ、生徒はみんな熱心です。でも、最小論理の意味論は難しいので、意味を教える…

最小論理(minimal logic)を実装した interactive proof system MINLOG上で、bioinformaticsの定理の自動証明に挑戦する話。 最小論理とは、直観主義論理から矛盾律を除去した体系であり、最小論理における命題の証明は*1λ項によって完全に対応づけられ*2、従…

雨は止んだが、蒸し暑い日。コーディングと会議。某会議で自分の論文の対外発表許可申請についてプレゼンするが、自分のプレゼン下手に落胆する。しかし、なんとか申請が許可されたので一安心。後は、実際に論文を書いてacceptされるだけ（って、そこが最大…

強めの雨、もう梅雨のようだ。出勤してコード書きと打ち合わせ。Tkさんに書いたコードについて色々コメントを頂く。21時半に帰宅、夕食はカレー。

今回は対公理の話、対公理で任意の集合x,yにたいし、xとyを元として含むような集合zをとり、z内部で内包公理によってx,yしか元がない公理を作り、外延性公理によってその一意性を証明する。一意に存在するので、集合x,yしか含まない集合を{x,y}と書いてよい。…