Abstract Go?del’s proof of his famous ?rst 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, Go?del did something that by any metric must be classi?ed 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 Go?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 ?nd a proof of the incompleteness of Peano Arithmetic, can such a machine, provided this description as input, produce as output a complete and veri?ably correct proof of G1? In this paper, we summarize engineering that entails an af?rmative 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 Go?del’s Fixed Point Lemma, from which G1 follows quickly.