Email Gateway (Aug 18 2022 at 20:14): Email Gateway (Aug 18 2022 at 20:14):From: Jens Doll <jd@cococo.de>
Hello all,
now I've got 50 JAVA/C functions similar to
----------- function 1 out of 46 -------------------
//--------------------------------------
// 1. Proposition
// x is divisible by y
//--------------------------------------
BOOL divisible(NAT x, NAT y) {
NAT i;
for (i=1;(i<=y);i++)
if (x==y*z)
return TRUE;
return FALSE;}
--------------------- end of function------------------------------
and I don't know how to transpose them into Isabelle proofs/theorems
effectively.
Is anyone interested and willing to help me investigate the stuff?
Jens
http://cococo.de
Email Gateway (Aug 18 2022 at 20:15):From: Jens Doll <jd@cococo.de>
Thanks, John, it was an error in transcription. Here are the first three.I
hope the html marking will also be transmitted ..
//--------------------------------------
// 1\. Proposition
// x is divisible by y
//--------------------------------------
BOOL divisible(NAT x, NAT y) {
NAT z;
for (z=1;(z<=y);z++)
if (x==y*z)
return TRUE;
return FALSE;}
//--------------------------------------
// 2\. Proposition
// x is a prime number
//--------------------------------------
BOOL Prim(NAT x) {
NAT z;
for (z=1;(z<=x);z++)
if (z!=1)
if (z!=x)
return TRUE;
return FALSE;}
//--------------------------------------
// 3\. Function
// the n-th prime number contained in x
//--------------------------------------
NAT Pr2(NAT n, NAT x) {
NAT y;
if (n==0) return 0;
else {
n=0;
for (y=1;(y<=x);y++) {
n=n+1;
if (Prim(y))
if (divisible(x,y))
if (y>Pr2(n-1,x))
return y;
}
}
return 0;}
Best Regards
Jens Doll
Am 26.06.2012 09:08, schrieb John Wickerson:
Goedel.jpg
Email Gateway (Aug 19 2022 at 08:06):From: Jens Doll <jd@cococo.de>
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](cid:part1.06090203.07080202@cococo.de) 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
\-----------------------------------------------------------------------------------
attachment 1
\--------------------------------------------------------------------------------------------------------------
goedel pow 12 1500
59138332051041477857792134235669290840410130588006373166053589671727698902916332833359397148803993897326677281721126293
773322423135275557345849997217508590192922491779070006392158472368759550821361036830323955751973780218814376420216153519
444121554642854107036061566289075722709397810120974839954179767258632289195024519205509694080262900521148298534500308836
228876765787453701167920379162857176687286340763959746406235760412522950737073600247960698254336951727417275609613120056
199956484282376092960847737164871933048651915361763622502861856670844477897863919036299845630307083886241812099204540122
356123742770559899747662595199231054488075097120984387716230576312978851398903482548204192854217775231839022397844642249
321323335873821528321457923265174332452579814652247072248949939717987506210928283520107615692805468018645403583104833774
321208226469210661260950278195394513731620511861842755325021854326749106268701235527111099367254720975509915629874031819
337717818251600578695148127904560239367372840989928402126283340592389716241820479292549567005942358636245308522397253833
009002641353055574299068860700295780015482612532490963318106560702127029406761735969721424132866689818076189313325449397
570119979359463935796193912131761781764130424353007487147238491878151521444129055997301653419265677104023531656402985486
902183104538959054135560788052294316761263825475659487083934449007284230375395247340049658371249407956911218599149612295
816324812669282540591466965258714382472865123435168091921785414589354644004421298502167791054479852892289356228264738978
948231124905010634616596869417552426431301715552391844069376
--------------
Email Gateway (Aug 19 2022 at 08:07):From: Lawrence Paulson <lp15@cam.ac.uk>
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
Email Gateway (Aug 19 2022 at 09:00):From: Jens Doll <jd@cococo.de>
Hello all,
having published Version 0.87 of my program Goedel
I would like to
ask the community for help:
*** Who is willing and able to produce Isabelle sources out of the 46+
functions,
which I implemented in the C language?
It might be interesting for proof technology and looks quite simple: take the
macros,
use the C preprocessor and generate Isabelle functions from them.
Go ahead, it's thrilling ...
Jens
Last updated: Apr 26 2024 at 20:16 UTC