-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
公理図式に現れるメタ変数にメタ項を代入すれば公理図式が得られる。このことは直感的には明らかだが、どう正当化されるのか、ずっと疑問だった。
2019-03-21 21:30:24
ぼんてんぴょん(Bontenpøn)
@y_bonten
『現代数理論理学序説』p4～5では、この手順を(1)公理図式に現れるメタ変数に、まず（通常の）項を代入する(2)得られた公理に現れる（通常の）変数にメタ変数を代入するという二段構えで説明している。「なるほどこうするのか」と感じる一方、それでなにか正当性が高まるのかどうか、よく分からない。
2019-03-21 21:30:24
ぼんてんぴょん(Bontenpøn)
@y_bonten
「公理図式が得られる」ちゃいまんがな、「定理図式が得られる」だ。twitter.com/y_bonten/statu…
2019-03-22 08:37:18
ぼんてんぴょん(Bontenpøn)
@y_bonten
派生規則や許容規則以前に、推論規則自体が「これとこれが証明可能ならこれも証明可能である」というメタ定理なのだな。シェマで与えられているということとは別の問題だ。
2019-03-27 15:51:16
ぼんてんぴょん(Bontenpøn)
@y_bonten
現代数理論理学序説p7問題1.1.6、「証明論の証明（メタ証明）は帰納法だらけ」と基礎論サマースクールで聞いたが、その入門編だ。証明は具体的な証明図の構成法を与えていることが多いので、こういう易しい問題で構成法まで納得しておくと、何をやっているのかつかみやすい。
2019-03-27 16:07:16
ぼんてんぴょん(Bontenpøn)
@y_bonten
M>Nを得るには公理(ρ)か規則(τ)を使うしかないので、M>Nの証明図を上に辿っていくと必ずN>Nに行き着く。その左には「何か >1 N」が書いてあるはず。これとN>Rおよび(τ)を繰り返し用いればM>Rが得られる。 pic.twitter.com/svCVOJ9HOO
2019-03-27 16:07:19
拡大
ぼんてんぴょん(Bontenpøn)
@y_bonten
これは「推論規則なら許容規則でもある」と言っているだけだな。すると推論規則・派生規則と許容規則（だが推論規則でも派生規則でもないもの）の違いは何か、ということになる。直感的には証明図式をポンと与えられるものが前者、そうでなくそのつど構成しないといけないが必ず構成できるものが後者。
2019-03-27 16:13:59
ぼんてんぴょん(Bontenpøn)
@y_bonten
「証明を、書かれている通りに納得できる」ということは皆無だな。自分の書いたものでさえ、いったん書き直さないと理解できない。結局もとに戻るんだけど。
2019-03-27 16:33:54
ぼんてんぴょん(Bontenpøn)
@y_bonten
メタ変数とメタレベルは無関係ではないけど、証明可能な具体的な論理式の頭にターンスタイルをつけて「これは証明可能である」というのは立派なメタレベルの言明だ。シェマになってるかどうかとはやっぱり区別しないといけないよね。
2019-03-27 17:32:36
ぼんてんぴょん(Bontenpøn)
@y_bonten
派生規則の定義は「A1,A2,…,An├Bのとき」で始まり、許容規則の定義は「A1├BかつA2├Bかつ…かつAn├Bのとき」で始まる。この書き分けの意図はよく分かるのだが、肝心の「├」の定義が「証明図が存在するとき」で済まされている。
2019-03-28 17:54:25
ぼんてんぴょん(Bontenpøn)
@y_bonten
メタ変数A,Bで書かれた「A├B」という、メタレベルの言明でしかもシェマであるものについて、「証明図が存在する」の定義が問題となる。A,Bに入る式ごとに証明図の枠組みが変わっても、とにかく存在すればよいのか、あるいは単一の「証明図シェマ」が存在しないといけないのか。
2019-03-28 17:54:25
ぼんてんぴょん(Bontenpøn)
@y_bonten
天の声からご指摘をいただきました、許容規則は「├A1かつ├A2かつ…├Anならば├B」で始まるのでした。twitter.com/y_bonten/statu…
2019-03-28 19:05:58
ぼんてんぴょん(Bontenpøn)
@y_bonten
『現代数理論理学序説』p7、「この変形のことをweak変形といいます」って、「>」による変形だけなのかか「>1」も入るのか分からんが、「=_w」が「weak変形でわたりあえる同値関係」とあるのでたぶん「>」だけなのだろう。
2019-03-29 13:30:24
ぼんてんぴょん(Bontenpøn)
@y_bonten
「=_w」は確かに同値関係だが、「渡りあえる」といっても「>」自体に対称律が成り立つわけではないので、M>NとM>Rが証明できても（M=NとM=Rを経てN=Rは証明できるのに）N>RもR>Nも一般には証明できないだろうと思う。
2019-03-29 13:50:50
ぼんてんぴょん(Bontenpøn)
@y_bonten
まぁ馴染みのない体系を使って「知らないふりゲーム」の練習をしてみましょう、という主旨であって、combinatory logicの説明を真面目にやるつもりはないのだろう。
2019-03-29 13:51:26
ぼんてんぴょん(Bontenpøn)
@y_bonten
A >1 B、B >1 C、C >1 D、……という一連の式が証明できたとき、派生規則によってすべての「>1」を「>」に直し、しかるのち許容規則の「>」推移律を使えば、望みの組み合わせの「前>後」が証明できる。しかし、「後」を固定してよいなら許容規則まで引っ張り出さなくても良い。
2019-03-29 20:12:04
ぼんてんぴょん(Bontenpøn)
@y_bonten
例えばEを後端にすると、D >1 EからD > E（派生規則）、これと C >1 DからC > E、これとB >1 CからB > E、これとA >1 BからA > Eとなる。後端をE以外にするとまた初めからやり直さないといけないが、その面倒くささを押し込めているのが許容規則の「>」推移律であったとも言える。
2019-03-29 20:12:04
ぼんてんぴょん(Bontenpøn)
@y_bonten
いまだに「>」と「>1」の違いを悟っていない。事実として言えるのは ・SやKの公理は「>1」で与えられる。 ・M>Mという反射的な公理(ρ)は「>」で与えられる。 ・推論規則(τ)はM>1 N と N>R から M>Rを得る形。
2019-04-03 19:48:41
ぼんてんぴょん(Bontenpøn)
@y_bonten
・(τ)でR=Nとすれば M>1 NからM>Nが導ける。逆は導けそうにない。 ・「>」の推移性は許容規則として得られる。「>1」の推移性は言えそうにない。 ・「>_1」で次々に繋ぐことができれば、前述のとおり「前>後」はすべて証明できる。
2019-04-03 19:48:41
ぼんてんぴょん(Bontenpøn)
@y_bonten
最後の原理が分かっていないと、解答例にあるような「>1w」でどんどん繋いでいく書法の意味が理解できない。証明図をきちんと書くととても大変だが、一度は書いておくのがお勧め。
2019-04-03 19:48:42
ぼんてんぴょん(Bontenpøn)
@y_bonten
問題1.1.9の2つ目の証明図。(τ)の左上の式（斜めに並んでいる）を順に書いたものが著者による解答例に相当する。(μ)は後ろに同じものをくっつける操作。 pic.twitter.com/1AG5rjdS1V
2019-04-04 08:28:10
拡大
ぼんてんぴょん(Bontenpøn)
@y_bonten
(μ)を見ると一気に付け足したくなるが、括弧がないときは左から結合するので一つずつやらないといけない。
2019-04-04 09:00:52
ぼんてんぴょん(Bontenpøn)
@y_bonten
問1.1.10も、x＝yを導くために一所懸命x > yあるいはx >1 yを導こうと頑張っていたが、無理だな。M>xとM>yを両方導けるようなMを見つければいいんだ。
2019-04-04 11:59:46
ぼんてんぴょん(Bontenpøn)
@y_bonten
今回は解答例に証明図があるので略式で： ・KIyx >1 Kyx >1 y（KI >1 Kによる） ・KIyx >1 Ix >1 x（問1.1.9の結果による） 同じ式からyとxが出たので同値関係にある。
2019-04-04 12:24:08