I’m incredibly busy right now adjusting to my new job and my new commute, which is leaving me less time than usual for blogging. So I’m going to raid the archives, and bring back some interesting things that appeared on the old Blogger blog, but were never posted here. As usual, that will involve some cleanups and rewrites, so this won’t be identical to the original posts.<\/p>\n
I’ve written about logic before, and mentioned intuitionistic logic at least in passing. Intuitionistic logic is an interesting subject. Intuitionistic logic is a variation of predicate logic which is built on the idea that there should be a stronger notion of “truth” in logic: that the strict categorization of all statements in classical logic as either true or false is too strong<\/em>. In intuitionistic logic, a statement is only true if you can prove<\/em> that it is true. It is not<\/em> enough to prove that it’s opposite is false: In propositional logic, it is not<\/em> the case that ¬¬P→P.<\/p>\n <\/p>\n In fact, truth is intuitionistic logic is defined by proof: A is true means<\/em> that there exists a proof of A. A is false<\/em> means that there is a proof that there is no proof of A. Most of the differences between intuitionistic and classical logic comes from that distinction between the classical meaning of true and false, and the intuitionistic meaning of true and false.<\/p>\n The intuitionistic meaning has the implication that many inferences that we’re used to in propositional logic are no longer valid in intuitionistic logic:<\/p>\n One way to think of intuitionistic logic is to think of it as if there were actually three values that can be assigned to a predicate: it can be in one of two definite states (proved true or proved false) or it can be in an indefinite state (unproven). If a predicate P is unproven, then we can assert neither that P is true nor that P is false. But if the predicate is in an indefinite state, and we can show a proof, then we can move it to a definite state: if we can find a way to provide a proof of P, then it becomes true; or if we can show that it’s unprovable, then it becomes false.<\/p>\n It’s worth reiterating: one of the really wonderful properties of intuitionistic logic is that it’s strongly constructionist. A proof that “¬A” in intuitionistic logic will always<\/em> generate at least<\/em> one concrete counterexample of A. There are entire programming languages built on this fundamental point. (Not to get too far off topic, but a prolog program basically works by negating<\/em> a statement for which you want concrete examples, and then using intuitionistic inference to generate counterexamples for that negative – which are concrete examples of where the statement is true.)<\/p>\n The formal semantics of intuitionistic logic are more complicated than the semantics of predicate logic. They tend to involve things like lattice theory. In my next post, I’ll talk about one way of describing the semantics of intuitionistic logic called Kripke Semantics. Kripke semantics is useful not just for intuitionistic logic, but for a lot of other things, like temporal logics, modal logics, model checking – and providing models for many of the calculi that fascinate me. Kripke semantics provide the definitive model for λ-calculus, and by extension, for other fascinating calculi like the π-calculus. <\/p>\n","protected":false},"excerpt":{"rendered":" I’m incredibly busy right now adjusting to my new job and my new commute, which is leaving me less time than usual for blogging. So I’m going to raid the archives, and bring back some interesting things that appeared on the old Blogger blog, but were never posted here. As usual, that will involve some […]<\/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":[33],"tags":[],"class_list":["post-361","post","type-post","status-publish","format-standard","hentry","category-logic"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-5P","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/361","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=361"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/361\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=361"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=361"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=361"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\n