2003-03-13
λ. Syllable
ふとノートPCにインストールしてみる。インストールはラクチンだったけど、PCカードのネットワークインターフェースを認識してくれなかったのであまり遊べず。仕方ないからデスクトップの方に入れようか……
PythonはPerlはパッケージが用意されているけど、Rubyはまだ無いようだ。それからw3mやzshなんかのパッケージもあった。
λ. gtk2 on cygwin
結局、win32 backend 用と x11 backend 用はパッケージを分けることにした。でも、librsvgのように依存部分が本体でなくてかつサイズも小さい場合には両方入れてしまってもいいかな。
GImageViewだけど、DnDには自前でfile:〜を扱わないでg_filename_from_uri()を使った方が、URIのunescapeとUTF-8の変換をやってくれるので、よさげ。g_filename_from_uri()を使ったら、日本語ファイル名や空白を含むファイルも他のアプリケーションからドラッグできるようになった。次にパッケージを出すときはこれを使おっと。
(UTF-8に変換するのは余計なお世話のような気もするけど、RFC2718にはUnless there is some compelling reason for a particular scheme to do otherwise, translating character sequences into UTF-8 (RFC 2279) [3] and then subsequently using the %HH encoding for unsafe octets is recommended.
なんて書いてあるのか……)
λ. LUNO
TRPG: メモ書き (2003-03-11)より。WishListに追加。
2006-03-13
λ. instance Bounded Double
そういやDoubleとFloatってBoundedのインスタンスになっていないんだな。 知らなかった。
<URL:http://www.haskell.org/pipermail/haskell/2005-March/015490.html>
2007-03-13
λ. 不完全性定理に関して混乱中 (3)
前回のエントリで元々の疑問は大体解決しました。 色々とコメントや言及をありがとうございます。
特に、竹内さんと通りすがりさんのコメント、かがみさんのエントリ(モデルでの真偽, さらにω矛盾)は疑問を解消する上で大いに役立ちました。
また、あろはさんにも二つのエントリで言及していただきました。
以下、色々と余談みたいなものを。
何故こんな疑問を持ったか?
そもそも、何故こんな疑問を持ったかというと、きっかけはTaejun(태준)さんという方のブログTaejunomicsの「数学と法律はかなり近い？」というエントリに以下のように書いてあったこと。
述語論理の公理系に、等号の公理と数の公理が加わっただけで、その体系は数学の公理系になります。 ちなみに、この二つを加えることによって、完全な述語論理の体系が、不完全になってしまうらしく、これをゲーデルの不完全性定理というそうですね。 （完全とは、その公理系が妥当な論理法則の全てを証明することが出来る事を指します）
これに「完全性定理と不完全性定理の『完全性』は違う意味*1で、等号の公理と数の公理を加えることによって『完全性』が損なわれるわけではない」というような内容のコメントを書こうとして、「そういや、算術の体系に完全性定理を適用するとどうなるんだっけ?」と思い、9日の混乱(不完全性定理に関して混乱中)に至ったのでした。
不完全性定理に言及することについて
あろはさんの二つのエントリは幾つか勘違いしている気がするけど、それはとりあえず横に置いておいて、ちょっと別の話を。
あろはさんは真なのに証明できない命題 ？？？というエントリで「数学をちゃんとやってない俺が書いて良いような内容じゃないし… おこがましすぎる」と書いている。 けど、不完全性定理自体は基礎的な定理だし、前提知識も少ないので、ちょっと論理学を勉強すればすぐに理解できるはず。 「おこがましすぎる」等と言う前に、ちょっと勉強すれば良いだけだと思います。
実際、今回使ったのは向井先生の「数学と論理」*2という授業で得た知識くらいで、この授業は主に学部1年生が履修する授業です。
「通りすがり」さんの問題
「通りすがり」さんのコメントの「あと、健全性を示す∃x. prove(x,[P])⇒Pも証明できませんが、これの否定が真であるモデルは、当然非健全です」について考えてみる。
T ⊢ provable([G])→G と仮定する。 T ⊢ G≡¬provable([G]) より T ⊢ ¬provable([G])→G 。 T ⊢ provable([G])∨¬provable([G]) なので T ⊢ G 。 これは第一不完全性定理に矛盾するので、背理法より T ⊬ provable([G])→G 。 というわけで、T ⊢ provable([P])→P は一般には言えない。
次に、あるPについて provable([P])→P の否定が真であるモデルMを考える。 すなわち M ⊧ T∪{¬(provable([P])→P)} で、¬(provable([P]→P) ≡ provable([P])∧¬P だから、 当然 M ⊧ provable([P]) かつ M ⊭ P になる。 モデルが非健全という言い方には少し違和感を感じるけど、言わんとすることは理解できる。
残る疑問点
今回のことで不完全性定理についてだいぶ理解を深められた気がするが、まだ残っている疑問も幾つかある。
その一つはロッサーの不完全性定理が何故成り立つのかという事。 ゲーデルの証明ではω無矛盾性を条件としていたが、後にロッサーがω無矛盾性を無矛盾性に弱めている。 今回、ω無矛盾性を条件としたのは、これが何故成り立つのか知らなかったから。 聞くところによると、ゲーデル文とは違う文を考えるらしいが……
あとは、論理学にまつわるトンデモ言説「自分自身の無矛盾性を主張する文は証明できない」の以下の記述について。
標記の主張は、自分自身の無矛盾性を主張するすべての文は、証明できない、ということになってしまします。これは少くとも、通常ゲーデルの不完全性定理の対象とされるペアノ算術では正しくありません。実際に、自分自身(つまりペアノ算術)の無矛盾性を主張している(と理解できる)が、しかしペアの算術で証明できてしまう文が存在するのです。
これらはまたの機会にでも考える。
【追記】 と書いたら、かがみさんの「ロッサーの不完全性定理」でどっちも解決してしまった。もきゅ(´・ω・`)
*1 「完全性」の複数の意味については、檜山さんの「完全性／不完全性」は多重定義のし過ぎ！」を参照のこと。
*2 数学と論理(2006)に2006年度の講義資料がある。私が履修した2001年度とは内容もだいぶ変わってるけど。
ψ 通りすがり [＞非健全という言い方には少し違和感を感じるけど、 確かに・・・普通は「不健全」といいますね。]
ψ 通りすがり [ところで、無矛盾性を健全性として定義した場合、どんな算術的述語Pを持ってきても、任意の命題XについてP("x")⇒X..]
ψ 通りすがり [まあ、普通は無矛盾性は、P("x")⇒¬P("¬x")のように表すでしょうから、その場合、不完全性定理に抵触しない抜..]
ψ さかい [> 確かに・・・普通は「不健全」といいますね。 違和感を感じたのはそこではなくて、健全性は通常は「T |- φ ..]
ψ 通りすがり [＞健全性は通常は「T |- φ ならば M |= φ」のように「構文的な証明可能性」と「意味論的な真偽」との関係につ..]
ψ さかい [> ただし真偽についてはMの中で考えていると思いますが この辺りはまだ混乱中なのですが、Mの中での証明可能性が「M..]
ψ 通りすがり [述語trueの定義は、任意の命題φについてφ⇔true("φ")だから、M |= φでもM |= true("φ")..]
ψ タナカコウイチロウ [おそーいコメントですが、「数学と法律はかなり近い？」について。 最高裁では「少数意見」や「反対意見」があるので、一意..]
2008-03-13
λ. “Continuations in Natural Language” by Chris Barker
自然言語における継続 - sumiiの日記 で住井さんに教えてもらって、ずっと積読になっていたんだけど、今度の Continuation Fest 2008 の予習のために読んだ。「自然言語」で「継続」ときて連想したのは「そういえばPTQでの名詞句と量化子の扱いはCPS変換に似てるな」だったんだけど、ちょうどそれが最初の例として取り上げられていた。他の例としてはfocus, 等位接続(coordination), misplaced modifiers が取り上げられていた。これは面白い。
ψ いっちー [大丈夫、読めなかったのはあなただけじゃないよ。思わず Google サーチしちゃった。 それで、なぜか「かっぱえびせ..]
ψ キリコ [何で かっぱえびせん ていうの？]
ψ さかい [なぜ、『かっぱえびせん』という名前なのですか？ http://www.calbee.co.jp/soudanshit..]