Even though this post seems to be shifting back to axiomatic set theory, don’t go thinking that we’re
\ndone with type theory yet. Type theory will make its triumphant return before too long. But before
\nthat, I want to take a bit of time to go through some basic constructions using set theory.<\/p>\n
We’ve seen, roughly, how to create natural numbers using nothing but sets – that’s basically what Of course, we haven’t defined arithmetic – we’ve just defined numbers. You might think it would be <\/p>\n If we want to define arithmetic, first we need to define what it is. What is natural number addition?<\/p>\n It’s a total function from a pair of integers to a single integer. <\/p>\n One problem: what’s a function? We haven’t really defined functions yet. We know about In set theory, a function is a special kind of relation. A relation, in turn, is a set of That sounds a tad confusing: but just look at a simple example. Say that we want a function We’ve still got a problem, though. What’s an ordered pair? We’ve only built sets and numbers; we’ve defined functions in terms of these “ordered pair” things, but we can’t use that definition until we’ve got pairs.<\/p>\n The naive thing to do is to say that a pair is a set: (x,y) = {x,y}. But that doesn’t work: (x,y)≠(y,x), but {x,y}={y,x}. There’s no notion of ordering in sets, but an ordered pair is ordered – that’s why it’s called an ordered pair! So we need some way of distinguishing between the first and second Let’s look at a quick example. Suppose we wanted the ordered pair (2,1). That gives us ordered pairs – and therefore relations, and therefore functions.<\/p>\n Now we’ve got the hardware we need. To define arithmetic, we’re going to define If A is a natural number, then by our construction of the natural numbers, we know Addition: <\/b> Addition is a function from a pair of numbers to a number. So it’s That last line is a simple example of what I was talking about. We don’t worry Multiplication:<\/b> multiplication is very similar, and relies on addition. Multiply is Even though this post seems to be shifting back to axiomatic set theory, don’t go thinking that we’re done with type theory yet. Type theory will make its triumphant return before too long. But before that, I want to take a bit of time to go through some basic constructions using set theory. We’ve seen, […]<\/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":[43,56],"tags":[],"class_list":["post-549","post","type-post","status-publish","format-standard","hentry","category-numbers","category-set-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-8R","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/549","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=549"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/549\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=549"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=549"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=549"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
\nthe ordinal and cardinal number stuff is about. Even doing that much is tricky – witness my gaffe about
\nordinals and cardinals and countability. (What I was thinking of is the difference between the ε series in the ordinals, and the ω series in the cardinals, not the ordinals and cardinals themselves.) But if we restrict ourselves to sets of finite numbers (note: sets of finite numbers, not<\/em> finite sets of numbers!), we’re pretty safe.<\/p>\n
\npretty important to define arithmetic on the numbers. If you thought that, you’d be absolutely
\nCorrect. So, that’s what I’m going to do next. First, I’m going to define addition and subtraction – multiplication can be defined in terms of addition. Division can be defined in terms of multiplication
\nand subtraction – but I’m going to hold off on defining division until we get to rational numbers.<\/p>\n
\nsets, we know about logical predicates, and we’ve constructed the natural numbers. But we haven’t said anything about functions. So before we can define addition, we need to define functions.<\/p>\n
\nordered pairs. For a relation, r, r = {(x,y) : R(x,y))}. In other words, a relation
\nis really a name for a predicate over the set of all ordered pairs that describes a relationship
\nbetween x and y – a two-parameter predicate. A function is a relation where, for any x, there is
\nno more<\/em> that one pair with any given value of x in its first position. If f is a function,
\nand (x,y)∈f, then we can also write y=f(x). This is called application syntax<\/em>.<\/p>\n
\nfrom the members of the set {1, 2, 3, 4} to itself. We could write one such function as f = {(1,2), (2,3), (3,4), (4,1)}. Then f(2) just means the second member of the pair in f that starts with 2: f(2)=3.<\/p>\n
\nvalues in an ordered pair, without<\/em> any notion of ordering. It turns out to be pretty easy: (x,y) = {x,{x,y}}. There’s a set with two values, and one of them is a subset of the other. So we can recognize the one that’s the first element, because it’s the value that’s an element of the other; and then we can look at the other set, and see what value is inside of it besides the first one.<\/p>\n
\nIn set form, 2 = {∅,{∅}}, and 1 = {∅}. So the ordered pair (2,1) would be the set
\n{2,{1,2}}. (Or expanded, {{∅,{∅}}, {{∅}, {∅,{∅}}}}). So if we were given
\nthe set {{1,2},2}, and we knew it was an ordered pair, then we could look at it, and say there are two
\nmembers, a and b. a = {1,2}; b = 2. b∈a, so b=2 is the first element of the pair. a = {1,2}, so
\nthe second element of our ordered pair is the member of a that is different from b, so the second element of the pair is 1. What if the pair is something like (1,1)? Then the set form is {1,{1}}, and since
\none element is a member of the other, and the other has only one element, then we know it’s an equal pair.<\/p>\n
\nfunctions for the operations. We don’t<\/em> need to say how to do them: we just need
\nto define their meaning. You’ll see what I mean by that in a minute. <\/p>\n
\nhow to increment it. We’ll define our functions using that.<\/p>\n
\na set of ordered pairs, whose first element is an ordered pair. So it’s a set of
\npairs of the form {((x,y),z) where:<\/p>\n\n
\nabout how to do it; we just define things in terms of logical relation. We know
\nthat every number has a successor. Because every number has a successor, every number
\nexcept 0 has a predecessor. We don’t need to say how to get it – we just know that
\nit exists, and for the purposes of defining what addition means, that’s good enough.
\nSubtraction is a better example of that. x-y is the set {((x,y),z) | ((z,y),x)∈Add} –
\nthat is, x-y=z if and only if z+y=x. That doesn’t tell us anything about how to subtract,
\nbut it does define what subtraction means.<\/p>\n<\/p>\n
\na set of ordered pairs, just like addition: Mult = {((x,y),z)} where:<\/p>\n\n