Re: [isabelle] Goedel's Proof

It isn't that surprising that you can't compute these functions if they represent logical formulas by integers. However, Gödel-numbering can equivalently be done using Lisp S-expressions. (Strictly speaking, these should be the hereditarily finite sets, where order is ignored.) If you allow yourself a number of distinct atoms as a starting point, your data structures and proofs might actually become intelligible. 

The danger perhaps is that it would start to look too much like an ordinary proof checker coded in Lisp. Shankar's 1986 formalisation of Gödel's incompleteness theorem using nqthm comes to mind. As I recall, he wrote an entire proof-checker for first-order logic within nqthm's Lisp-like formalism.

Larry Paulson

On 7 Jul 2012, at 17:15, Jens Doll wrote:

> 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.