-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
@functional_yy @noukoknows なるほど、束縛変数に対するメタ記号ですか……言われてみれば、と言う感じです。
2013-09-30 13:11:09
ぼんてんぴょん(Bontenpøn)
@y_bonten
@functional_yy 「x＝xを公理とする」を「何でもいいのでひとつ」と考え、例えば 「v_3=v_3」を公理として、それをオブジェクトレベルの推論規則にある全称化で「∀x(x＝x)」を得ればよいわけですね。
2013-09-30 13:27:48
ぼんてんぴょん(Bontenpøn)
@y_bonten
そう言えば講義資料にも「ある反証可能な論理式を任意に一つ固定してそれを『人』であらわす」というのがあって、ずっと頭に残っていた。
2013-09-30 13:30:47
ぼんてんぴょん(Bontenpøn)
@y_bonten
合宿講義資料p7の演習問題、これで合ってますかね…… http://t.co/b5XQuPy0yu
2013-09-30 17:35:11
拡大
ぼんてんぴょん(Bontenpøn)
@y_bonten
推論規則がmodus ponensだけの体系というのをよく聞く気がするけど、ヒルベルト流ではMPと「全称化」の2本の推論規則を採用している。「A→∀vAを公理にして、推論規則はMPだけ」にしてもいい気がするが、なんぞメリットがあるのかしらん。
2013-09-30 18:13:06
TS
@ta_shim_at_nhn
代入を定義した後、代入可能なケースを別に定めるとかしていなければ、演習問題の解答は罠にかかっています。 初めての演習問題ならば、1日かかっても不思議はないレベルの問題ですね。
2013-09-30 19:41:45
ぼんてんぴょん(Bontenpøn)
@y_bonten
合宿講義資料では、代入可能性の議論は後回しにして、とりあえず「代入」を定義して、それを「正当な代入」と「正当でない代入」に分類するスタイルを採っています。いずれにせよ、どこかで直面しないといけない問題ですね。
2013-09-30 19:47:59
TS
@ta_shim_at_nhn
Q: 代入の定義が面倒なのですがどうしたらよいでしょう。 A: 束縛変数と自由変数に同じ記号を使わなければいいんじゃね? (Gentzen) A: 変数を使うのが悪い。箱でも書いておきなさい。(Bourbaki)
2013-09-30 20:01:01
ぼんてんぴょん(Bontenpøn)
@y_bonten
合宿資料に戻ると、p39ではレベルの違う演算子が一緒くたになって序列づけられている。この順序自体は間違っていないが、例えばa＋b＝cが(a＋b)＝cでありa＋(b＝c)でないのは、またa＝b∧φが(a＝b)∧φでありa＝(b∧φ)でないのは、優先順位以前の問題であることにも注意。
2013-09-30 21:43:36
ぼんてんぴょん(Bontenpøn)
@y_bonten
.@kobae964 そこが気になってます。＋≫＝≫∧という優先順位を使う機会がないのは、項や論理式の定義がたまたまそうなっているからですね。この定義をすげ替えるときに備えて優先順位を決めておく、ということに利便性があるのかどうか、よく知らないです。
2013-10-01 04:14:07