[comp.lang.lisp] Help.Goedel.Lisp

koen@ut-emx.UUCP (Billy Koen) (06/06/90)

~7
	During the mid-60Us at MIT, one of our professors (Minsky? Bobrow?) ask us to demonstrate/prove GoedelUs Proof in Lisp.  Now three decades later I would like to use it in the class room, but cannot remember the exact problem statement or the demonstation.  As we know GoedelUs Proof is constructive and presumeably the problem asked to construct the conditions under which the sentense RArithmetic is consistent.S is true in an environment of the axioms of arithmetic yielding as a condition RArithmetic is not

 consistentS or some such.    Any help with this problem or leads would be appreciated.  Thanx.

Billy Koen
koen@emx.utexas.edu

!@-:LaserWriter

jack@cs.glasgow.ac.uk (Jack Campin) (06/06/90)

koen@ut-emx.UUCP ( Billy Koen) wrote:

> 	During the mid-60Us at MIT, one of our professors (Minsky? Bobrow?)
> ask us to demonstrate/prove GoedelUs Proof in Lisp.  Now three decades
> later I would like to use it in the class room, but cannot remember the
> exact problem statement or the demonstation.

Dunno about that one, but there is an explicit proof of Godel's theorem
using Lisp in Gregory Chaitin's "Algorithmic Information Theory" (Cambridge
University Press).  It's a long way from Godel's own proof, though.

[ Incidentally, take your terminal emulator outside and shoot it. That was
  possibly the nastiest formatting I've ever seen in a Usenet article. ]

-- 
--  Jack Campin   Computing Science Department, Glasgow University, 17 Lilybank
Gardens, Glasgow G12 8QQ, Scotland   041 339 8855 x6044 work  041 556 1878 home
JANET: jack@cs.glasgow.ac.uk    BANG!net: via mcvax and ukc   FAX: 041 330 4913
INTERNET: via nsfnet-relay.ac.uk   BITNET: via UKACRL   UUCP: jack@glasgow.uucp

ycy@walt.cc.utexas.edu (Joseph Yip) (06/08/90)

Hi, I am looking for a public domain Lisp compiler or interpretor. Does
GNU has a Lisp compiler available. I will be running lisp on a Sun 3 or
Sun 4.

Thank you.
Joseph Yip