ゲーデルの不完全性定理の証明のアレをRacketで書いてみる (25)
もうほとんど「Racketで書いてみる」という部分には意味がなくなっている気がする
今日このごろですが続けます
10.8.5 公理・定理・形式的証明
やっと次の節に入りました
最近はただ式をコードに置き換えてるだけって感じになってましたが
どうもそれ以前の問題が発生
定義34 xは公理Iから得られる"論理式"である
公理 I-1 ¬(fx1=0)
公理 I-2 (fx1=fy1)→(x1=y1)
公理 I-3 x2(0)∧∀x1(x2(x1)→(x2(fx1))→∀x1(x2(x1))
まずわからないのは変数が固定されてしまっている（ように見える）こと
x1って書いてるけど好きな変数使っていいよ、ってことには見えません
「公理 I-1、I-2、I-3に対応するゲーデル数を、それぞれα1、α2、α3とする」って
書いてありますからゲーデル数が確定しているはず
x1と言ったらx1です
てことは¬(fx1=0)は公理だけど¬(fy1=0)は公理じゃない、ってことになりませんか
それでいいんでしょうか
どこかに論理式の変数をsubstしていいって書いてあったかな？
次に出てくる命題論理の公理では、pやqが任意の論理式を表してるんですけど
なぜここでは任意の第1型の変数をvとして¬(fv=0)、とかやってないんでしょうか
x1についてだけ言えれば証明には十分なんでしょうか
数学的帰納法がx1にしか使えないとなればけっこうやりづらい気がします
わかりませんがとりあえず大丈夫だと信じることにして進みます
さらに
等号が使われていますが等号は定数としても省略形としても導入されていません
これも不思議なところ
なにかしら定義してやる必要があります
ミルカ「ゲーデルの論文では」プリンキピア・マテマティカを参照していて、
x1=y1は∀u(u(x1)→u(y1))と定義していた。《どんな集合uを持ってきても、
x1が属しているならy1も属している》ということ」
しかしこの等号の定義、使い勝手がいい気がしません
1+1=2を証明するのに、どんな集合を持ってきても1+1が属しているならば
2も属している、ってことを証明しなければならないとしたらけっこう
めんどくさそうじゃないですか？
そうでもないんですかね
ひとつできればあとはパターンでできそうな感じではありますが
ていうか矢印は両方向いてなくて大丈夫なの
x1だけが属する集合がないことだけ言ってて
y1だけが属する集合がないことは言わないってそれでいいの
正しくない例は思いつかないけど非対称で気持ち悪いんですが
みんなこれですっきりしてるの
とは言え、「x1、y1は」と言っているからさっきよりはユルくて
x1、y1は任意の変数、ただし第1型に限る、くらいでいいのかな？
uは第2型の任意の変数？
それとも第2型以上でもいいのかな？
とするとuはもうひとつ上の型の任意の変数？
でもこのuも確定させないと公理のゲーデル数が確定しませんね
でも確定させてしまうとどこかの変数とカブってしまうかもしれないんじゃ？
うーん
型が違うからx1やy1とカブることはなくて大丈夫？
ならz2にしておくか・・・
gensymの公理とかいりませんか？
xやyが第1型の変数であることのチェックはいるかな？
そういえば基本論理式かどうかを判定する述語はありましたが
基本論理式を作る関数がないですね
ついでに作ります
x、yは第1型ってことにしときます
uのところはz2で固定
なーんかイヤーな感じがしますが・・・
(define (ElementForm a b)
(** a (paren b)))
(define (Equal x y)
(ForAll (var 3 2) (Implies (ElementForm (var 3 2) x)
(ElementForm (var 3 2) y))))（Equalはxとyが等しいかどうかを判断する述語ではなく）
（x=yという式のゲーデル数を返す関数）
（自分が混乱しそうなので念押しで書いておく）
しかし定義32で省略形を定義したとき、なぜ等号も定義しなかったんでしょうか？
まさか難しくて避けたってことはないでしょうし
プリンキピア・マテマティカに詳しく書いてあるから不要、ってことなんですかねえ
省略形としてでなく、等号を定数として定義した場合はどうなるんですかね
その場合は等号の公理を定義してやらないといけないのか
それはそれで書きにくいのかな？
反射律・対称律・推移律だけじゃ等号にならないか・・・えーとどうするんだ？
さて全部開き直れば公理の定義は作業
(define AxiomI-1
(Not (Equal (succ 1 (var 1 1)) (￣ 0))))
(define AxiomI-2
(Implies (Equal (succ 1 (var 1 1))
(succ 1 (var 2 1)))
(Equal (var 1 1)
(var 2 1))))
(define AxiomI-3
(Implies (And (ElementForm (var 1 2) (￣ 0))
(ForAll (var 1 1)
(Implies (ElementForm (var 1 2) (var 1 1))
(ElementForm (var 1 2) (succ 1 (var 1 1))))))
(ForAll (var 1 1) (ElementForm (var 1 2) (var 1 1)))))このへんは関数ではなく定数
> AxiomI-1
1724525548553843697788893564187467728584956605329005012311592512493987999515387138077915500560245777191373344293359256266083115587743775502491727813073521895200330055504324012013567068865736268982732558216744759397891467627493190075855309727016824163461680086287319232258470462236599783948273340853763005212095335947859254609907511219372555855889685185034232445051587299488525826665321751049739303950164144693091628306182442781108436217562512255448319536885379876967859696223188180842769719437228228400481692481107264561540694324925339918081717490942800465845008609409214328447623641246956102681024457111697519478985612747747448816949078950096305162141492097658434053404017513500130419428531396802206818879603017635164464424316122373432466437500000
> AxiomI-2
746390244163595496151739759488677866680245082591779108967324036080407747471910180661419110151580060013178876708607332892247926605825629494374832643597359490578149258495875934685524237516889744145445508501119026104103871647401240951447342669217654584021887270516456516779184294052604865343364415570755090305641026630013385919388212597438622137720934590352838417304890909787889863479828195820049870234985740995526737824720792992404612883611304448222320492783319019716838568790236697881648536334379483139799031112496704308825163705831207890573818780739814227317587230480336382357600460593760440389712750046047993584513788839123336488863963828906505893785566548902120577274749309721408889821036069510584169477651334077561089738460860983437532528921269904336334341223141853367786407208283998387613659918396200014789609829780099450725771051068595032291356884496131638395752777995381430258425918152526086381308138673677080505434924264641837737671516562794458579580684965698418774799868784176653543384610815336135364188365462671706659178581532222787978514030835406128052770060452016153086377720874468631312311048564771168315358518777535971207751585926621278961806778887718903790222795860126692286267810559512757620819925653987906225450070032671683990240138881677303863561399624245243422746283124293795381507583565728102384387901200762976691384067600453242992015574097637720446121358613647500323193041045476441318823488702633596420363621639065523681615792620844393565969845750079560325243108809880569549842550228843369002915487962776420247117745502323690408980678335549966720898266790115009080727128139336229467715389722372741006426151454420969384081048672744640560634556781938619794970212686189782938813050686862445596054520871045217920240985745979781717334846306381907723693235138520783865306879780034546557709509996656117472082610665484119470945055268728138253407240008446205095424737806299958152085397132839075522839573932480030334709377794270386491314582570458294852580477669711673878090681090363910456837376836147092725101134000510020759250641732420990926388298808690451692801640981084016935185829240858279289013562755879144579965570223111029103722523033664168378204676808978281337367058076993109982536700187571539628438479568457231861262439561094525918020254270550465006053056126565911761660351650782788503954045123801363489088061682684245086431038160326684097902853029403228537491311209718984101774745598045352152162236965381468877253170930725887469622300000000000
> AxiomI-3
47473735314208867229977204039657359771178826705424403852339975843183622384105238477879615786730311869282798421202922263944218416337623091875417595705736164729943490047686962950182861638331319394664760669795758358828140292743373825617404779433707191916322363160057261540581150267956491130691068346925003798313764734279730255890117222511147497185346156777321441325009487759061546745166163769041566216659598661754464078887720454844116969828487693979302259194633626357034474664974996315376938593233124674312801346447956154875341019575303105121538773408029987574266469237517375274724068849778562198366025473364398696572487704338499345000650970846633365096943891830533047191418988456547868115381221661542055246114525951104552461661927662972400795423929169130157178486471515527171950394526706032245206206545152132783317548350553157005168198003489196443641546260408090970335364631615618489731557702010437463258198898196002058371140778991940161861649801832293594325342914233640190484979201300000000000証明で公理を使おうとすると、最低でも2^AxiomI-2みたいな数を扱わなければいけないわけで
楽しいとしか言いようがありません
はい目的の述語
(define (IsAxiomI x)
(or (= x AxiomI-1)
(= x AxiomI-2)
(= x AxiomI-3)))¬(fy1=0)は公理ですよね! #f
