{"id":3133,"date":"2015-02-26T18:57:28","date_gmt":"2015-02-26T23:57:28","guid":{"rendered":"http:\/\/www.goodmath.org\/blog\/?p=3133"},"modified":"2015-02-26T18:57:28","modified_gmt":"2015-02-26T23:57:28","slug":"propositions-as-proofsets-unwinding-the-confusion","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2015\/02\/26\/propositions-as-proofsets-unwinding-the-confusion\/","title":{"rendered":"Propositions as Proofsets: Unwinding the confusion"},"content":{"rendered":"

My type theory post about the different interpretations of a proposition caused a furor in the comments. Understand what’s going on that caused all of the confusion is going to be important as we continue to move forward into type theory.<\/p>\n

The root problem is really interesting, once you see what’s going on. We’re taking a statement that, on the face of it, isn’t about sets. Then we’re appyling a set-based interpretation of it, and looking at the subset relation. That’s all good. The problem is that when we start looking at a set-based interpretation, we’re doing what we would do in classical set theory – but that’s a different thing<\/em> from what we’re doing here. In effect, we’re changing the statement.<\/p>\n

For almost all of us, math is something that we learned from the perspective of axiomatic set theory and first order predicate logic. So that’s the default interpretation that we put on anything mathematical. When you talk about a a proposition as a set, we’re programmed to think of it in that classical way: for any set S, there’s a logical predicate P_s such that by definition<\/em>, \\forall x: x \\in S \\Leftrightarrow P_s(x). When you see P \\Rightarrow Q in a set-theory context, what you think is something like \\forall x: x \\in P \\Rightarrow x \\in Q. Under that intepretation, the idea that P \\supset Q is equivalent to P \\rightarrow Q is absolutely ridiculous. If you follow the logic, implication must<\/em> be the reverse of the subset relation!<\/p>\n

The catch, though, is that we’re not talking about set theory, and the statement P \\Rightarrow Q that we’re looking at is emphatically not<\/em> \\forall x : P(x) \\Rightarrow Q(x). And that, right there, is the root of the problem.<\/p>\n

P \\rightarrow Q always means P \\rightarrow Q – it doesn’t matter whether we’re doing set theory or type theory or whatever else. But in set theory, when we talk about the intepretation of P as a set<\/em>, right now, in the world of type theory, we’re talking about a different set<\/em>. <\/p>\n

Super set doesn’t suddenly mean subset. Implication doesn’t start working backwards! and yet, I’m still trying to tell you that i really meant it when i said that superset meant implication! how can that possibly make sense?<\/p>\n

In type theory, we\u00b4re trying to take a very different look at math. In particular, we’re building everything up on a constructive\/computational framework. So we’re necessarily going to look at some different interpretations of things – we’re going to look at things in ways that just don’t make sense in the world of classical set theory\/FOPL. We’re not going to contradict set theory – but we’re going to look at things very differently.<\/p>\n

For example, the kind of statement we’re talking here about is a complete, closed, logical proposition, not a predicate, nor a set. The proposition P is a statement like “‘hello’ has five letters”. <\/p>\n

When we look at a logical proposition P, one of the type theoretic interpretations of it is as a set of facts: P can be viewed as the set of all facts that can be proven true using P. In type theory land, this makes perfect sense: if I’ve got a proof of P, then I’ve got a proof of everything<\/em> that P can prove. P isn’t a statement about the items in Ps proof-set. P is a logical statement about something<\/em>, and the elements of the proof-set of P are the things that the statement P can prove.<\/p>\n

With that in mind, what does P \\Rightarrow Q mean in type theory? It means that everything<\/em> provable using Q is provable using nothing but P.<\/p>\n

(It’s really<\/em> important to note here that there are no quantifiers<\/em> in that statement. Again, we are not<\/em> saying \\forall p: P(x) \\Rightarrow Q(x). P and Q are atomic propositions – not open quantified statements.)<\/p>\n

If you are following the interpretation that says that P is the set of facts that are provable using the proposition P, then if P \\Rightarrow Q, that means that everything that’s in Q must also be in P. In fact, it means pretty much exactly<\/em> the same thing as classical superset. Q is a set of facts provable by the statement Q. The statement Q is provable using the statement P – which means that everything in the provable set of Q must, by definition!<\/em> be in the provable set of P.<\/p>\n

The converse doesn’t hold. There can be things provable by P (and thus in the proof-set of P) which are not provable using Q. So taken as sets of facts provable by logical propositions, P \\supset Q!<\/p>\n

Again, that seems like it’s the opposite of what we’d expect. But the trick is to recognize the meaning of the statements we’re working with, and that despite a surface resemblance, they’re not<\/em> the same thing that we’re used to. Type theory isn’t saying that the set theoretic statements are wrong; nor is set theory saying that type theory is wrong. <\/p>\n

The catch is simple: we’re trying to inject a kind of quantification into the statement P \\Rightarrow Q which isn’t there; and then we’re using our interpretation of that quantified statement to say something different.<\/p>\n

But there’s an interpretation of statements in type theory which is entirely valid, but which trips over our intuition: our training has taught us to take it, and expand it into an entirely different statement. We create blanks that aren’t there, fill them in, and by doing so, convert it into something that it isn’t, and confuse ourselves.<\/p>\n","protected":false},"excerpt":{"rendered":"

My type theory post about the different interpretations of a proposition caused a furor in the comments. Understand what’s going on that caused all of the confusion is going to be important as we continue to move forward into type theory. The root problem is really interesting, once you see what’s going on. We’re taking […]<\/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":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[292],"tags":[],"class_list":["post-3133","post","type-post","status-publish","format-standard","hentry","category-type-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-Ox","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3133","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=3133"}],"version-history":[{"count":3,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3133\/revisions"}],"predecessor-version":[{"id":3136,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3133\/revisions\/3136"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3133"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3133"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3133"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}