Sometimes Richard Waldinger has gotten help from Rodrigo de Salvo Braz (http://www.ai.sri.com/people/braz) for webinar-style remote connections to AIC Seminars (while 16:00 PDT is inconvenient for European time zones, I thought the abstract might be worth a look nevertheless): http://www.ai.sri.com/seminars/detail.php?id=495 Harold From: Carl Hewitt [mailto:[email protected]] Sent: Tuesday, July 19, 2016 9:53 PM To: [email protected] Cc: Carl Hewitt Subject: Mathematical Foundations of Computer Science: where Gödel went wrong Folks, Please come to the seminar below. Thanks! Carl SRI AI Seminar August 2, 2016 EK255 (SRI E building) (Directions <http://www.ai.sri.com/visiting> ) Mathematical Foundations of Computer Science: where Gödel went wrong Carl Hewitt <https://plus.google.com/+CarlHewitt-StandardIoT> https://plus.google.com/+CarlHewitt-StandardIoT Kurt Gödel [19061978] was one of the world's greatest logicians. Although still strongly supported by many contemporary theoreticians, his conceptions of computation and logical foundations have been made obsolete by developments in computer science. For example, Gödel declared that it is absolutely impossible that anybody who understands the question [What is computation?] and knows Turings definition should decide for a different concept. However, the Turing Machine model of computation left out a crucial aspect of computation, namely, communication among computers. In the Internet of Things one computer is no computer. As an illustration, this talk presents a very simple effective concurrent computation that cannot be perform using a (nondeterministic) Turing Machine, which illustrates how nondeterministic branching in state machines (such as Turing Machines) is not a good model for message reception in IoT. Gödel claimed that the Turing Machine model was supported when it was shown to have equivalent computational power in computing mathematical functions. However, the parallel lambda calculus can be exponentially slower than computations making use of communication that is not restricted to being strictly hierarchical Humans are now very dependent on computer information systems. We have reached the point where increased automation in reasoning is required for humans to cope with the rapidly increasing complexity of information systems. Gödel considered first-order logic to be at the foundation of mathematics. However, model checking is foundational for computer science and first-order theories have models with highly undesirable infinite integers and infinitesimal real numbers. Using strongly typed theories (analogous to strongly typed programming languages), integers, real numbers and other computer data structures can be axiomatized so that the models provably do not have infinite integers, infinitesimal real numbers, etc. As humans increasingly rely on computer-automated reasoning, erroneous conclusions in Mathematics can lead to incorrect operation of computer-operated systems. For example, first-order logic is not a suitable foundation for the Internet of Things in which specifications require a device respond to a request. The specification that a computer responds cannot be proved in first-order logic. Gödel claimed that I'm unprovable. is necessarily a proposition of Principia Mathematica, which was claimed at the time to be a foundation for all Mathematics. However, using an argument explained in this talk, Wittgenstein showed that Gödel's proposition leads to inconsistency in Mathematics. In response, Gödel retreated to first-order logic in defense of his proposition. However in computer science, there are no known practical uses for Gödel's proposition. Worse yet, allowing Gödel's proposition has the false consequence that Mathematics cannot not prove its own consistency. In fact, this talk shows that Mathematics proves its formal consistency using a very short formal proof. Mathematics retains its consistency because strongly typed logic shows that Gödel's proposition is not a valid proposition of Mathematics. Also, strongly typed theories (adequate for the foundations of computer science) thwart all other known paradoxes such as Berry, Burali-Forti, Girard, Russell, etc. that can lead to erroneous conclusions in Mathematics. Bio for Carl Hewitt Carl Hewitt is an emeritus professor of computer science (MIT) who is best known for his work on the Actor model of computation, which is in widespread use in eBay, Microsoft, Twitter, etc. For the last decade, his work has been in the field of Inconsistency Robustness, which aims to provide practical rigorous foundations for systems dealing with pervasively inconsistent information. He is co-editor with John Woods assisted by Jane Spurr of the monograph Inconsistency Robustness (Vol. 52 of Studies in Logic). Hewitt is currently Board Chair of the International Society for Inconsistency Robustness (iRobust) and also Board Chair of Standard IoT, an international standards organization for the Internet of Things, which is using the Actor Model to unify and generalize emerging standards for IoT. _______________________________________________ RuleML-all mailing list [email protected] http://ruleml.org/mailman/listinfo/ruleml-all_ruleml.org
