{"id":109,"date":"2006-08-10T10:53:57","date_gmt":"2006-08-10T10:53:57","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2006\/08\/10\/metamath-and-the-peano-induction-axiom\/"},"modified":"2006-08-10T10:53:57","modified_gmt":"2006-08-10T10:53:57","slug":"metamath-and-the-peano-induction-axiom","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2006\/08\/10\/metamath-and-the-peano-induction-axiom\/","title":{"rendered":"Metamath and the Peano Induction Axiom"},"content":{"rendered":"<p>In email, someone pointed me at an automated proof system called [Metamath][metamath]. Metamath generates proofs of mathematical statements using ZF set theory. The proofs are actually relatively easy to follow, which is quite unusual for an automated theorem prover. I&#8217;ll definitely write more about Metamath some other time, but I thought it would be interesting today to point to [metamaths proof of the fifth axiom of Peano arithmetic][meta-peano], the principle of induction. Here&#8217;s a screenshot of the first 15 steps; following the link to see the whole thing.<br \/>\n<img data-recalc-dims=\"1\" loading=\"lazy\" decoding=\"async\" alt=\"peano5-proof.jpg\" src=\"https:\/\/i0.wp.com\/scientopia.org\/img-archive\/goodmath\/img_31.jpg?resize=625%2C516\" width=\"625\" height=\"516\" \/><br \/>\n[metamath]: http:\/\/us.metamath.org\/mpegif\/mmset.html#overview<br \/>\n[meta-peano]: http:\/\/us.metamath.org\/mpegif\/peano5.html<\/p>\n","protected":false},"excerpt":{"rendered":"<p>In email, someone pointed me at an automated proof system called [Metamath][metamath]. Metamath generates proofs of mathematical statements using ZF set theory. The proofs are actually relatively easy to follow, which is quite unusual for an automated theorem prover. I&#8217;ll definitely write more about Metamath some other time, but I thought it would be interesting [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":false,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[24,33,43],"tags":[],"class_list":["post-109","post","type-post","status-publish","format-standard","hentry","category-goodmath","category-logic","category-numbers"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-1L","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/109","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=109"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/109\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=109"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=109"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=109"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}