アーカイブ konn-san.com

記事一覧

全ての実数の集合をLebesgue可測にする 〜Solovayモデル入門〜 - 2024/10/12 14:00:00 JST

「$\mathrm{ZF}+\mathrm{DC}$ + 任意の実数の集合がLebesgue可測」になる集合論のモデルSolovayモデルについてalg-dチャンネルで喋った時の資料です。

数理論理学の基礎からはじめる強制法入門──2024年自主ゼミ発表資料 - 2024/09/18 13:27:51 JST

2024年後半におるうぇ君、るじゃ氏、こりーさんなどとやっている強制法自主ゼミの発表資料です。 私とおるうぇ君とで、ロジックの基礎からはじめて強制法の基本を他の参加者に叩き込もうという会です。目標は$\mathrm{CH}$の独立性証明。

Talks - 2024/03/10 15:00:00 JST

これまでに行った講演

スカッと故事成語にっき20240127 - 2024/01/28 03:30:00 JST

かぜとたらこスパにっき20230516 - 2023/05/16 22:30:00 JST

Disco Elysium - 頽廃の都マルティネーズで世界の迷宮に迷い込もう - 2023/01/01 17:35:00 JST

Disco Elysium が前評判に違わず素晴しかったのでみんなプレイしましょうという話です。

古典的実現可能性モデルノート - 2022/09/16 21:00:00 JST

古典的実現可能性モデル（classical realisability）の手法は，Curry–Howard対応を拡張する形で$\mathrm{ZF}$のモデルを与える方法であり，Krivineによって導入された． 強制法を特別な場合として含むが，$\mathrm{ZFC}$から開始しても$\mathrm{ZF}+\neg \mathrm{AC}$のモデルが得られるという点で強制法を真に一般化するものになっている．

Boole値モデルと強制法 [PDF版] - 2022/06/11 18:00:00 JST

集合論における無矛盾性証明で用いられる主要な手法である強制法と，密接に関連するBoole値モデルの手法について，本稿では幾らか証明を省略しつつ概略を採り上げます．また，Hamkinsら [Hamkins:2012qv] の説明に基づいて，超冪とBoole値モデルの関係についても簡単に解説します．

うたにっき20211227 - 2021/12/27 18:25:00 JST

プロフィール - 2021/06/29 16:20:00 JST

わたしについて。

ゆめにっき20200526 - 2020/05/26 23:45:00 JST

Raspberry Pi + VPS で自宅グローバル IP の変更自動検知をやった話 - 2019/03/10 18:00:00 JST

光インターネット契約したらルータに VPN 機能が付いていたが、固定グローバル IP を買うのが面倒だったので、Raspberry Pi と VPS の自前 DNS サーバで何とか頑張った話。

CaTeX（軽鳥／怪鳥）で快適 LaTeX ライフ in VSCode - 2018/11/26 23:10:00 JST

YaTeX の補完機能を Visual Studio Code で実現する CaTeX 機能拡張のご紹介。

VSCode で YaTeX のイメージ補完やユニコード数式記号を入力する為の拡張をつくった - 2018/11/17 03:54:00 JST

VSCode で YaTeX のイメージ補完相当の機能を実現したり、Agda や Lean などの定理証明系で必要となるユニコード数式記号の入力を補助するための機能拡張を作った話しです。

Emacs から Visual Studio Code に乗り換える作業のメモ - 2018/10/16 00:05:00 JST

Emacs にそろそろ辟易してきたので、VSCode に乗り換えようとしています。その作業記録。

Haskellerの私的Rustチートシート - 2018/08/29 18:47:20 JST

Rustに入門したので、適宜HaskellのこれはRustのこれ、ということをここに蓄積していって、個人的なチートシートにする。

欲望の赴くままRustで型レベルPeano自然数とサイズ付きベクトルを書いた - 2018/08/29 18:45:17 JST

あるていど強い型システムを持った言語を見ると、型レベルペアノ自然数とサイズ付きベクトルを書きたくなる、というのは人類普遍の欲求だと思います。 という訳で欲求に忠実であることとし、型レベルPeano自然数とサイズ付きベクトルRustで実装しました。実用性？皆無です。

ぜみにっき20180614 - 2018/06/14 23:43:22 JST

ぎょうむにっき20180613 - 2018/06/14 23:39:44 JST

しむにっき20180612 - 2018/06/12 22:00:10 JST

いえにっき20180611 - 2018/06/11 23:58:01 JST

かいものにっきとか20180610 - 2018/06/10 21:18:46 JST

おうちにっき20180609 - 2018/06/09 22:09:10 JST

こーどにっき20180608 - 2018/06/08 22:16:38 JST

じすぜみにっき20180607 - 2018/06/08 01:17:10 JST

けんきうにっき20180606 - 2018/06/06 21:50:09 JST

かれーにっき20180605 - 2018/06/05 23:39:23 JST

りんごにっき20180604 - 2018/06/05 23:00:00 JST

そばにっき20180603 - 2018/06/05 22:30:00 JST

かいていにっき20180602 - 2018/06/02 20:10:11 JST

きょうのにっき20180601 - 2018/06/02 00:36:40 JST

かんぺきにっき20180531 - 2018/06/02 00:36:37 JST

まじでおぼえてないにっき20180530 - 2018/06/02 00:23:30 JST

いえにっき20180529 - 2018/05/29 20:19:53 JST

活にっき20180528 - 2018/05/29 20:17:23 JST

たいかいしゅにっき20180527 - 2018/05/29 20:13:42 JST

だっしゅつにっき20180526 - 2018/05/29 20:03:18 JST

おしごとにっき20180525 - 2018/05/29 19:24:00 JST

ゼミにっき20180524 - 2018/05/29 19:18:30 JST

にっき20180523 - 2018/05/23 23:33:54 JST

にっき20180522 - 2018/05/22 23:00:00 JST

ゆめにっき未遂20180521 - 2018/05/21 23:34:00 JST

きゅうせいしゅ（みすいにっき）20180520 - 2018/05/20 23:00:00 JST

おてつだいにっき20180519 - 2018/05/19 21:53:45 JST

ほげふがにっき20180518 - 2018/05/18 20:51:26 JST

すいりにっき201517 - 2018/05/18 00:25:40 JST

じむにっき20180517 - 2018/05/17 02:04:17 JST

わせだにっき20180515 - 2018/05/15 23:36:56 JST

のみにっき20180514 - 2018/05/14 23:06:27 JST

おうちにっき20180513 - 2018/05/13 20:55:56 JST

にっき20180512 - 2018/05/12 20:20:00 JST

にっき20180511 - 2018/05/11 22:40:30 JST

でーたにっき20180510 - 2018/05/11 03:10:00 JST

カツにっき20180509 - 2018/05/11 01:55:34 JST

ゆめにっき20180508 - 2018/05/08 22:50:00 JST

ほげにっき20180507 - 2018/05/07 22:45:00 JST

文フリにっき20180506 - 2018/05/06 23:45:00 JST

いどうにっき20180505 - 2018/05/05 22:00:00 JST

にっき20180504 - 2018/05/05 13:21:29 JST

かいものにっき20180503 - 2018/05/03 22:01:27 JST

えらかったにっき20180502 - 2018/05/03 18:24:22 JST

あついんだがあほなのかにっき20180501 - 2018/05/01 21:13:46 JST

ほんかくにっき20180430 - 2018/04/30 23:10:00 JST

ぱすたにっき20180429 - 2018/04/30 23:00:00 JST

きゅうせいしゅにっき20180428 - 2018/04/28 23:46:44 JST

きのうにっき20180427 - 2018/04/28 23:15:40 JST

いえにっき20180426 - 2018/04/26 23:10:11 JST

ほげにっき20180425 - 2018/04/25 22:27:27 JST

あめにっき20180424 - 2018/04/24 22:04:56 JST

いえにっき20180423 - 2018/04/24 00:00:35 JST

いえにっき20180422 - 2018/04/22 23:38:41 JST

すちゅーにっき20180421 - 2018/04/22 01:13:30 JST

はやおきにっき20180420 - 2018/04/20 23:01:37 JST

ふつかぶんにっき20180418-19 - 2018/04/19 23:17:12 JST

社会派にっき20180417 - 2018/04/18 01:13:42 JST

かじょうがきにっき20180416 - 2018/04/17 02:50:12 JST

うたわないにっき20180415 - 2018/04/15 23:59:59 JST

うたにっき20180414 - 2018/04/14 23:44:46 JST

うたにっき20180413 - 2018/04/13 23:59:59 JST

サーバのデータが消えました - 2018/02/24 01:24:34 JST

サーバ管理はちゃんとしましょうという話。

こんさんドットコムを TLS (HTTPS) に乗り換えた話 - 2018/02/09 22:35:00 JST

こんさんドットコムを TLS ベースに乗り換えたのでその顛末を。 特に、はてなブックマークの数が移行されないのでちょっと工夫したという話をする。

集合論の地質学4：下方有向性原理の証明 [PDF版] - 2017/12/11 21:00:00 JST

集合論の地質学に関する記事の第四回目． 今回はいよいよ，マントルや生成多宇宙の構造の大部分を確定させる基本定理である下方有向性定理を証明します．
前回はこちら． 初回はこちら．

集合論の地質学3：Bukovskýの定理──強制拡大の特徴付け [PDF版] - 2017/11/30 00:20:34 JST

集合論の地質学に関する記事の第三回目． 最終目標の下方有向性原理の証明の準備として，Bukovskýによる強制拡大の特徴付けを証明します． 前回はこちら． 初回はこちら．

集合論の地質学2：マントルの構造と下方有向性原理 [PDF版] - 2017/11/29 23:39:39 JST

集合論の地質学に関する記事の第二回目．今回は地質学の基本定理である下方有向性原理の紹介と，そこから得られるマントル$\mathbb{M}$に関する帰結を紹介します．前回はこちら．

強い選出原理としての強制公理 [PDF版] - 2017/11/14 00:49:10 JST

強制公理（Forcing Axiom）とは，ある種類の強制法による拡大と現在の宇宙がある意味で「近い」ことを述べる公理ですが，これは現代数学で用いられる選出原理であるZornの補題や従属選択公理（$\mathrm{DC}$）の一般化と見ることも可能です．後者の説明は，強制法の理論に関する知識が必要ないため，集合論以外の分野の人にもある程度理解しやすいことが期待されます．
そこで本稿では，強制公理の強い選出原理としての側面に焦点を当てて，強制法に馴染みの無い人にも強制公理がどんなものなのかを解説し，ついでに強制法とは何かについても軽く説明していきたいと思います．対象読者層としては，学部三〜四年程度の数学を知っていてZornの補題を使って何かを作る議論をしたことがあれば十分なようにしたつもりです．

集合論の地質学1：概観と基礎モデルの定義可能性 [PDF版] - 2017/11/09 20:05:31 JST

集合論の宇宙$V$は何らかの内部モデルの強制拡大になっているか？そもそもそういった基礎モデルは幾つあるのか？——こうした問題を考えるのが集合論の地質学（Set-theoretic geology）です．本稿では，その入門的な部分の解説を行います．
次回はこちら．

Cohen実数はSuslin木を付加する [PDF版] - 2016/11/25 15:00:00 JST

Shelahは実数の集合の性質に関する記念碑的論文 [Shelah:1984] において滅茶苦茶いろいろな事を示していて本当にヤバいんですが，その中で一節割いて「Cohen実数を付加するとSuslin木も足される」という事を示しています．原論文における構成は結構煩雑に見えますが，後にTodorčevićは彼の発明したの手法を用いて自然で比較的簡単な構成を与えました．minimal walkの手法はAronszajn木の構成にも使えますが，これとCohen実数を単に合成してやる事でSuslin木が得られるのです．本稿ではこの方法について（強制法の基礎理論は別にして）証明します．

絶対性チートシート [PDF版] - 2016/05/26 19:00:00 JST

公理的集合論においてあるモデルの性質を調べる際，様々な概念の絶対性を利用します．このプリントは，どのような条件下でどんな概念が絶対性を満たすのかをメモした個人的な覚書です．あくまで手軽に使うための覚え書きなので，そこまで踏み込んだ証明などは載せず，寧ろ一覧表のような体裁になる予定です．

On Regularity Properties of Sets of Reals and Inaccessible Cardinals (実数の集合の正則性と到達不能基数) - 2016/02/01 18:02:38 JST

修士論文。Solovayによる「ZF+弱い選択公理+“任意の実数の集合が可測”」という体系の無矛盾性証明と、およびKhomskiiによる一般化、そしてSolovayの逆向きの結果であるShelahの結果についてのサーヴェイ論文。また、上述の体系における代替的な解析学の結果も簡単に紹介。

可算推移的モデルの存在について [PDF版] - 2015/12/03 00:57:26 JST

ZFの可算推移的モデルの存在がCon(ZF)よりも真に強いことに関する説明です．

zsh hooks を使って ssh / mosh の接続先によって Terminal.app のテーマを変える - 2015/08/04 00:00:00 JST

この記事はQiitaからの移行記事です。情報は古いので、記録以上の価値はありません。

空から Mandelbrot 集合を見てみよう - 2015/01/24 02:26:00 JST

Mandelbrot 集合はよく知られたフラクタル図形ですが、これを「上から」（あるいは「下から」）見てみたらどう見えるのか、というお話。

latexmk で楽々 TeX タイプセットの薦め（＆ biblatex+biberで先進的な参考文献処理） - 2015/01/06 23:48:54 JST

TeX ファイルの変更を監視して、必要な回数だけ自動タイプセットしてくれる latexmk の紹介です。OMake はもう古い。あとbibtexの代替である biber と biblatex についても紹介。

Haskell ではじめるふわとろ Cocoa アプリ開発 - 2014/12/29 23:27:30 JST

Haskell による Cocoa アプリ開発の実際についての記事。Haskell Advent Calendar 2014 参加記事です。

F4, F5 アルゴリズムに関するサーベイ（A survey on F_4 and F_5 algorithms） - 2014/07/19 02:27:08 JST

Gröbner基底の効率的な計算法である F4, F5 アルゴリズムに関するサーベイ、メモ（A note on F4 and F5 algorithms to efficiently compute Gröbner bases）。

Definability lemma と Truth lemma [PDF版] - 2014/06/19 21:57:00 JST

研究室の集合論ゼミで，強制法の理論を支える基本的な定理である Definability lemma と Truth lemma の証明を発表したときの資料。

Martinの公理，範疇定理，小さな基数 [PDF版] - 2014/05/30 13:08:25 JST

研究室の集合論ゼミで，集合論の種々の独立命題を示す方法である強制法の理論の最初の方について発表した時の資料．

強制法のはじめのほう(1) [PDF版] - 2014/05/25 01:59:00 JST

研究室の集合論ゼミで，集合論の種々の独立命題を示す方法である強制法の理論の最初の方について発表した時の資料．

初等部分構造を用いたErdős-Radoの定理の証明 [PDF版] - 2014/05/01 23:00:42 JST

Erdős-Radoの定理はRamseyの定理に代表されるような，無限組合せ論における分割・彩色性質の一つです．ここではオリジナルの純粋に組合せ論的な証明ではなく，初等部分構造を用いたより簡単な方法を紹介します．

一意分解整域とその商体における Eisenstein の既約判定法 [PDF版] - 2014/01/24 22:04:00 JST

Eisenstein の既約判定法は Q[X] や Z[X] の既約多項式の判定法として広く知られていますが，実は係数環が一般の一意分解整域やその商体であっても使えることはそこまで知られていません．この事実を使うと，例えば多変数多項式環の既約元判定を簡単に行える場合があります．

計算機代数ゼミ発表資料 - 2014/01/24 18:52:02 JST

2013年度の計算機代数ゼミの発表資料です。主にGröbner基底の基礎理論から、それを応用した消去理論、連立代数方程式の解法などについてを取り扱っています。

定理証明系 Haskell - 2013/12/20 00:00:00 JST

Haskell Advent Calendar 2013 および Theorem Prover Advent Calendar 2013 参加記事。Haskell における依存型プログラミングおよび定理証明について解説した数少ない日本語文献です。C85 の TCUG に寄稿させて頂いた Haskell で定理証明を行う記事の販促記事でもあります。

第四回選択公理オフ：数理論理学の初歩の初歩の初歩の…… [PDF版] - 2013/10/16 00:48:34 JST

第四回選択公理オフでの発表資料．選択公理と関連するモデル理論の初歩の話です．初学者向けに論理式やモデルの定義から入り，超積や超冪と選択公理，超準解析の関わりなどを論じています．実は Łoś+超フィルター定理と選択公理は同値だよとかそういう話もあり．

Measure Problem と可測基数 [PDF版] - 2013/10/04 15:23:18 JST

選択公理の下で Lebesgue 可測でないような R の部分集合が存在することは広く知られた事実である．本稿では，測度の条件を幾らか緩めることで，Rの全ての部分集合が可測になるように出来ないだろうか？という問題と，そこから派生した集合論・測度論的な話題について紹介する．

Hausdorff Gap の証明 [PDF版] - 2013/09/01 23:38:34 JST

集合論における Hausdorff Gap の証明．

Extensible Effects はモナド変換子に対する救世主になり得るか？ - 2013/07/21 21:26:00 JST

Oleg らによる、モナド変換子に対する大体手法、Extensible Effects の論文を読んだ感想紹介記事です。

絶対に理解出来ないモナドチュートリアル - 2013/06/28 02:04:09 JST

絶対に理解出来ないモナドチュートリアルです。

はてなの数式を綺麗にする Chrome 拡張機能をつくった（※はてな以外も※） - 2013/05/18 01:54:42 JST

はてダなど mimetex を使っている数式をMathJax経由で綺麗にレンダーするようにする Chrome 拡張。

今年の冬は Gröbner 基底でスーパー大学受験ガール！ - 2013/04/01 00:00:00 JST

受験問題の大半は、 Gröbner 基底を使うことで楽々解き切ることが出来ます！今回はそうしたGröbner基底の技をドドドーン！とご紹介！！今年の受験数学は Gröbner 基底で乗り切りましょうそうしましょう！

８つの質問で、GHC の type-level language 業界の現状を知る - 2013/03/20 15:01:50 JST

「８つの質問」という釣り記事が技術クラスタで昔流行って、それに便乗してGHCの型システムの話を書いた。

『夏と冬の奏鳴曲』論 ──或いは喪われた中心と探偵小説 - 2013/03/11 13:00:56 JST

麻耶雄嵩『夏と冬の奏鳴曲』を一種のメタ・ミステリと捉え、本編において提示された世界観や構造を基に、近代科学の台頭とキリスト教的世界観の崩壊とミステリ文学の勃興について新たな視点を提供する。

イガスレイヤー 最終エピソード ザ・ラスト・ジャッジメント - 2013/03/11 12:19:09 JST

山田風太郎『甲賀忍法帖』をニンジャスレイヤー文体に翻訳したもの。

konn-san.com を刷新した - 2013/03/11 03:19:07 JST

今みてる konn-san.com 設立当時の設立宣言。こっちがメインになるとは思わなかった。

超積によるコンパクト性定理の証明と超準モデル ──君の知らない自然数── - 2013/03/09 00:00:00 JST

超積によるコンパクト性定理の証明と、無限大を含む自然数の超準モデルの構成法について。

2012年度集合論ゼミ発表資料 - 2013/01/22 23:59:59 JST

2012年度の研究室集合論ゼミでの発表資料。

さらば愛しき JavaScript —— 愛と欲望の果てに Haskell は fay と出逢う。 - 2012/12/25 14:11:11 JST

Haskell のプログラムからJavaScriptを自動生成する Fay という言語処理系についての紹介記事。Haskell Advent Calendar 2012 の七日目の記事。

夢野久作の世界 ～破格の異色作家と本格ミステリ～ - 2012/07/14 00:00:00 JST

夢野久作の短編についての考察と久作の作品世界についての紹介。ドグラ・マグラの布教。

GHC 7.4.1 の型レベル新機能を使い倒す 〜GADTs、型族 と DataKinds、ConstraintKinds の円環〜 - 2012/06/07 00:48:45 JST

GADTsや型族が入って、GHCの型システムがリッチになりはじめた頃の解説記事。

Haskell で LK の定理証明系を書いた - 2012/05/30 17:54:18 JST

Haskellの型機能をふんだんに使って、古典命題論理の体系であるLKの定理証明系を書いた話ぞ。

Haskell で Gentzen の LK - 2012/05/24 00:00:00 JST

この記事はQiitaからの移転記事です。 大昔に書いた、シーケント計算をHaskellの型システムを使って上手くエンコードした実装の記事ですが、正直何も整理されていないので、記録以上の意味はありません。

QuickCheck / SmallCheck の紹介 〜オートマトンの例を通して〜 - 2012/04/27 01:09:37 JST

オートマトンの検証という例を通して、QuickCheck や SmallCheck による性質ベースのテスト手法を紹介します。

How wonderful to be (statically) typed 〜（静的に）型がつくって素晴しい〜 - 2012/04/12 22:19:08 JST

Haskellの型システムの強力さとその工学的な応用例についての発表。

Yesod を支える技術 - 2012/03/24 14:41:14 JST

大昔のYesodの内部構造についての紹介。

Twitter 波括弧事件についてまとめてみる - 2012/03/13 02:03:39 JST

大昔にTwitterで波括弧を書くとテンプレートとして展開されるという事件があって、その時の話をまとめた今となっては考古学的な資料。

初めてのブログ - 2012/03/12 15:00:59 JST

ブログを作った報告。技術的な詳細解説。

コントの中に観るミステリ精神 〜Monty Python とラーメンズから〜 - 2012/03/10 17:41:00 JST

Monty Python やラーメンズのコント作品を、ミステリ的視点から鑑賞する。

圏の骨格と選択公理 - 2012/03/04 23:17:00 JST

圏の骨格の存在定理が選択公理と同値であることの証明。

Pos 圏の射影的対象と選択公理 [PDF版] - 2012/03/02 23:17:00 JST

「Pos圏における射影的対象のなす充満部分圏が集合圏と同型である」ことと選択公理の同値性の証明。

本格ミステリと『真相』の問題 〜三津田信三『作者不詳 ミステリ作家の読む本』〜 - 2012/01/14 00:00:00 JST

三津田信三『作者不詳』を題材に、本格ミステリにおける真相の問題について考察する。あわせて、ミステリにおける「論理」とはいかなる推論様式であるのかについて明らかにする。