[isabelle] Goedel's Proof



Dear Isabelle users,

in order to have an imagination of what Kurt Goedel achieved in 1930 when he proved that formally undecidable propositions (of Principia Mathematica) exist, I  did some implementation work based on his 46+ functions used in the proof. I constructed macros EXISTS and FORALL and implemented them practically as C functions (with some natural number arithmetic), where an EXISTS consists of simple counting and testing all possibilities.  Soon after having implemented and run some of these functions I came to a very practical border: functions like Gl n x or Typ x, where x is a supposed to be a sequence of numbers, are practically not computable. Despite of that I have an intermediate result consisting of

  • the 46+ functions as EXISTS/FORALL macros, a formal language (aiming at Isabelle)
  • a little windows program* which implements these functions (caveat, only the simple ones come to completion!)
  • a command line interface for natural number processing, e.g.  >goedel pow 12 1500 gives the digit sequence of attachment 1
If anyone should be interested in these software artefacts or is willing to make an Isabelle proof out of them (!!), he/she is invited to comment them or give a different feedback to me - thanks.

Happy reasoning,
Jens

* an additional Linux implementation should be easy ...

----------------------------------------------------------------------------------- attachment 1 --------------------------------------------------------------------------------------------------------------
>goedel pow 12 1500
59138332051041477857792134235669290840410130588006373166053589671727698902916332833359397148803993897326677281721126293
773322423135275557345849997217508590192922491779070006392158472368759550821361036830323955751973780218814376420216153519
444121554642854107036061566289075722709397810120974839954179767258632289195024519205509694080262900521148298534500308836
228876765787453701167920379162857176687286340763959746406235760412522950737073600247960698254336951727417275609613120056
199956484282376092960847737164871933048651915361763622502861856670844477897863919036299845630307083886241812099204540122
356123742770559899747662595199231054488075097120984387716230576312978851398903482548204192854217775231839022397844642249
321323335873821528321457923265174332452579814652247072248949939717987506210928283520107615692805468018645403583104833774
321208226469210661260950278195394513731620511861842755325021854326749106268701235527111099367254720975509915629874031819
337717818251600578695148127904560239367372840989928402126283340592389716241820479292549567005942358636245308522397253833
009002641353055574299068860700295780015482612532490963318106560702127029406761735969721424132866689818076189313325449397
570119979359463935796193912131761781764130424353007487147238491878151521444129055997301653419265677104023531656402985486
902183104538959054135560788052294316761263825475659487083934449007284230375395247340049658371249407956911218599149612295
816324812669282540591466965258714382472865123435168091921785414589354644004421298502167791054479852892289356228264738978
948231124905010634616596869417552426431301715552391844069376

--------------


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.