tag:blogger.com,1999:blog-264226589944705290.post1580396491355807719..comments2022-08-07T01:05:01.413-07:00Comments on God Plays Dice: Logic as machine languageMichael Lugohttp://www.blogger.com/profile/15671307315028242949noreply@blogger.comBlogger6125tag:blogger.com,1999:blog-264226589944705290.post-44045529720254614052011-10-27T13:31:04.182-07:002011-10-27T13:31:04.182-07:00I was just Googling this very subject!
Perhaps on...I was just Googling this very subject!<br /><br />Perhaps one should point to Russell and Whitehead's <em>Principia</em> as an example of when logic behaves like the "machine language of mathematics".<br /><br />It does lead into an interesting situation for people trying to construct automated theorem provers: why not bootstrap something "high-level"? <br /><br />After all, we have high level languages which compile to machine code...why can't we do likewise for automated proof checking (or "theorem proving")?pqnelsonhttps://www.blogger.com/profile/12779680952736168655noreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-71021308103242870142008-12-04T15:15:00.000-08:002008-12-04T15:15:00.000-08:00I don't exactly agree. Higher level programming la...I don't exactly agree. Higher level programming languages still offer the necessary primitives so that the language is Turing complete, but it also comes with better abstraction mechanisms, nicer syntax, etc. In other words, it's another formal system, just a more pleasant one.<BR/><BR/>What mathematicians use day to day is not a full replacement formal system. Whenever you give a proof sketch, or don't completely formalize the proof, by analogy you're omitting to fill the body of a function that you think can be easily written by the competent reader.<BR/><BR/>The full analogy is called the Curry-Howard correspondence where omitting a proof corresponds to asserting that there probably is at least one programming language term (e.g. a function) that inhabits the static type, which corresponds to the proposition.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-76519264615640566292008-12-04T08:15:00.000-08:002008-12-04T08:15:00.000-08:00Of course, most mathematicians do work in some for...Of course, most mathematicians do work in some formal system, if not ZFC. And even then, they may work in a higher-level language than the 'assembly language' of the foundations of their own field.<BR/><BR/>The idea that there could be a unified foundation in ZFC is perhaps a statement about 'intermediate languages' --- or, if we identify each 'assembly language' with the 'machine' it corresponds to, the statement that ZFC provides a broad foundation is akin to saying that ZFC's machine is adept at virtualizing the machines of many other branches of mathematics.AgainstWordshttps://www.blogger.com/profile/14682868442299622498noreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-61794368504937165252008-12-04T05:47:00.000-08:002008-12-04T05:47:00.000-08:00One of the problems with machine generated proofs ...One of the problems with <A HREF="http://www.mcs.anl.gov/AR/otter/" REL="nofollow">machine generated proofs</A> is that they do derive everything from first principles. Another problem is that automatically figuring out which deductions are 'interesting' is very hard.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-29610290138688587552008-12-04T01:24:00.000-08:002008-12-04T01:24:00.000-08:00A followup to my earlier comment: I don't actually...A followup to my earlier comment: I don't actually think that most mathematicians (myself included) really think of what we do as based on first order logic and ZFC. It's just that we maintain an awareness that we might, in principle, reduce everything we do to those terms if we ever wished to. (Speaking as an analyst here ... I am sure not all mathematics actually happens inside ZFC, even in principle.)Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-264226589944705290.post-20507918552692291412008-12-04T01:18:00.000-08:002008-12-04T01:18:00.000-08:00I like it. Back in the late '80s when I taught a l...I like it. Back in the late '80s when I taught a logic class, I put together a little program to compute a proof of the tautology (A→(B→C))→(B→(A→C)), a proof in this context meaning a sequence of formulas that are either axioms or follow from preceding formulas by an application of modus ponens. The resulting proof, after weeding out duplicates, is 31 formulas long. That such a trivial statement requires such a lengthy proof is already a good demonstration of the need for abstraction and higher level concepts. Of course, the work by Russell and Whitehead is the ultimate demonstration of same.Anonymousnoreply@blogger.com