-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
また一方で、Γ├Δと書いたとき、「Δの依存リストがΓに包含されている」というだけであって、解消済の仮定や使っていない仮定がΓに混じっていてはいけない、という意味ではないということにも注意が必要。記号の定義の問題だが。
2013-09-28 10:24:14
ぼんてんぴょん(Bontenpøn)
@y_bonten
要約：「仮定が立っている／解消されている」というのは、証明機械の内部状態のようなものではなく、個々の論理式に付随したデータである、と考えたほうがよい。
2013-09-28 10:28:15
ぼんてんぴょん(Bontenpøn)
@y_bonten
「→導入」の「Aを仮定してBが導かれたら、無仮定でA→Bを導いてよい」という文言に対して、「証明の履歴をたどらないと、導出してよいかどうか決まらないのか？」とか、「推論規則が『├』という概念を使って記述されているんじゃないか？」といった気持ち悪さを、ずっと感じていた。
2013-09-28 11:16:41
ぼんてんぴょん(Bontenpøn)
@y_bonten
これも、仮定への依存リストが個々の論理式に付随していると考えれば、要するに「C」(upon A)から「A→C」を導出してよい、また「C」(upon A, B)から「A→C」(upon B)を導出してもよいし、「B→C」(upon A)を導出してもよい、という局所の話に過ぎない。
2013-09-28 11:18:46
TS
@ta_shim_at_nhn
仮定をいくつ消すかというのは構造規則の話になります。古典論理や直観主義論理の場合はどちらでもかまわないので、全部消してしまうのが規則を述べる上では単純になります。消さなくてもよいという規則は、導出図を見れば簡単ですが文章だけで述べようとすると面倒なことになります。
2013-09-28 11:55:34
TS
@ta_shim_at_nhn
上江洲先生や鹿島さんの本は全部消すという流儀だったと思います。全部消すので、解消された仮定にわざわざマークを付ける必要はありません。∃ の除去で固有変数が何かに言及しておきさえすれば、どの推論を行なった時点で仮定が何かは一意に定まります。
2013-09-28 12:09:04
ぼんてんぴょん(Bontenpøn)
@y_bonten
もしも「解消できる仮定の一部を残す」という行為が「全部解消した直後に改めて立てる」という行為と等価なら、わざわざ一部だけ解消することを規則で許すメリットって乏しいんじゃないかなぁ、と感じてしまう。そう単純ではないのだろう。
2013-09-28 12:19:29
TS
@ta_shim_at_nhn
導出図の結論が「この仮定」に依存していると言いたいときに、「この仮定」を指定する方法は、結論からその仮定に至る path を指定するぐらいしか方法がないので、仮定を消さなくてもよい導出図を正確に定義すると、導出図の木と解消されていない仮定へ至る path の集合の組になります。
2013-09-28 12:26:52
ぼんてんぴょん(Bontenpøn)
@y_bonten
全部消す流儀に限っては、個々の論理式に情報を預ける必要がない、と言うべきか。一部を消す流儀でも依存リストを持たせればPATH要らないような気もするなぁ。
2013-09-28 12:33:05
ぼんてんぴょん(Bontenpøn)
@y_bonten
あぁ、「pathの集合の組」というのは、導出図から直列の形式的証明の列を作る話ではなくて、導出図そのものを定義する話だったのか。
2013-09-28 12:38:20
TS
@ta_shim_at_nhn
直観主義論理の構造規則に制限を付けた論理 (substructural logic) の研究というものがあります。その立場から見ると、一律に仮定をすべて消すのは、ある種の構造規則を使っているかどうかがわからなくなるので、仮定を残してもよいという推論規則の方が自然に見えます。
2013-09-28 12:40:18
ぼんてんぴょん(Bontenpøn)
@y_bonten
次回は脚本もなさると RT @tenapi: なので(?)次は松山でなんかやりましょう。「企画監督主演ゼルプスト殿下」じゃないやつ。 RT @y_bonten: ひょえー、いろいろ面白い世界が待っているのだなぁ。
2013-09-28 13:43:36
ぼんてんぴょん(Bontenpøn)
@y_bonten
あと一年くらいしたら、不完全性定理を「使って」導けることを普通に会話できるTLにしたい。体系の強さを比べるのに使えること以外、何も知らない。
2013-09-29 12:04:14
カオナシ(T. MATSUMOTO)
@CharStream
@y_bonten 二階述語論理の推論体系についてのこんな結果（http://t.co/Irkjwdx8ZS）なんかが、例えば『不完全性定理を「使って」導けること』の例の一つですね。
2013-09-29 16:39:01
ぼんてんぴょん(Bontenpøn)
@y_bonten
@CharStream ありがとうございます。この事実は同定理の系として容易に導けるのですね。こういうことをたくさん学びたいです。
2013-09-29 16:52:37
ぼんてんぴょん(Bontenpøn)
@y_bonten
「項への項の代入」「論理式への項の代入」の帰納的定義を自分で考えているのだが（合宿資料の演習問題）、こんなものでもいざ書くとなると時間が掛かるな。項・論理式そのものの帰納的定義を全く記憶していないことが分かる。
2013-09-30 09:59:46
ぼんてんぴょん(Bontenpøn)
@y_bonten
合宿講義資料p3の「メタ記号」という語の用法がよく分からない。「人間が読んだり書いたりする場合の読みやすさのために、変数記号のどれかを適宜表現するメタ記号を補助的に利用する」といった感じのことが書いてあるのだが……
2013-09-30 12:43:40
ぼんてんぴょん(Bontenpøn)
@y_bonten
メタ記号というと公理図式などのシェーマに使う記号がまず思い浮かぶが、それとこれとは違う話のように見える。
2013-09-30 12:43:47
ぼんてんぴょん(Bontenpøn)
@y_bonten
@shinji_kono 本来 v0,v1,v2,…… という変数記号を形式言語に導入しているが、読み易さのために適宜x,y,zなどを使って書く、という文脈でした。
2013-09-30 12:50:55
ぼんてんぴょん(Bontenpøn)
@y_bonten
@noukoknows その通りだと思います。同じ言葉で別のものを指している、というだけなら完全解決なのですが。
2013-09-30 12:51:55
ぼんてんぴょん(Bontenpøn)
@y_bonten
@functional_yy @noukoknows うぉ、そうなのですか！？お手数ですが、詳しく聴かせていただけませんか。
2013-09-30 12:58:59
ぼんてんぴょん(Bontenpøn)
@y_bonten
@functional_yy @noukoknows ありがとうございます。なるほど、「ここではv_0の別名としてxを、v_1の別名としてyを、v_2の別名としてzを用いる」などという但し書きがあるのでないかぎり、確かにそう考えられますね。
2013-09-30 13:04:45