G(o)del’s proof of his famous first incompleteness theorem (G1) has quite understandably long been a tantalizing target for those wanting to engineer impressively intelligent computational systems.After all,in establishing G1,G(o)del did something that by any metric must be classified as stunningly intelligent.We observe that it has long been understood that there is some sort of analogical relationship between the Liar Paradox (LP) and G1,and that G(o)del himself appreciated and exploited the relationship.Yet the exact nature of the relationship has hitherto not been uncovered,by which we mean that the following question has not been answered: Given a description of LP,and the suspicion that it may somehow be used by a suitably programmed computing machine to find a proof of the incompleteness of Peano Arithmetic,can such a machine,provided this description as input,produce as output a complete and verifiably correct proof of G1? In this paper,we summarize engineering that entails an affirmative answer to this question.Our approach uses what we call analogicodeductive reasoning (ADR),which combines analogical and deductive reasoning to produce a full deductive proof of G1 from LP.Our engineering uses a form of ADR based on our META-R system,and a connection between the Liar Sentence in LP and G(o)del’s Fixed Point Lemma,from which G1 follows quickly.
展开▼
