{"id":540,"date":"2007-11-04T15:30:51","date_gmt":"2007-11-04T15:30:51","guid":{"rendered":"http:\/\/scientopia.org\/blogs\/goodmath\/2007\/11\/04\/mathematical-constructions-and-the-abstraction-barrier\/"},"modified":"2007-11-04T15:30:51","modified_gmt":"2007-11-04T15:30:51","slug":"mathematical-constructions-and-the-abstraction-barrier","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2007\/11\/04\/mathematical-constructions-and-the-abstraction-barrier\/","title":{"rendered":"Mathematical Constructions and the Abstraction Barrier"},"content":{"rendered":"

There was an interesting discussion about mathematical constructions in the comment thread on my post about the professor who doesn’t like infinity<\/a>, and I thought it was worth turning it into a post of its own.<\/p>\n

In the history of this blog, I’ve often talked about the idea of “building mathematics”. I’ve shown several constructions – most often using something based on Peano arithmetic<\/a> – but I’ve never really gone into great detail about what it means, and how it works.<\/p>\n

I’ve also often said that the underlying theory of most modern math is built using set theory. But what does that really mean? That’s the important question, and the subject of this post.<\/p>\n

<\/p>\n

Math is based on formal reasoning. A formal reasoning system consists of two parts: a logic<\/a> – that is, a mechanical, symbolic inference system; and a model – a set of objects that our inference system can reason about. The objects are described by a basic set of axioms<\/em><\/a> that form the basis of
\nwhat we know about the objects. Everything else – everything<\/em> else, will be done by defining things in terms of those basic objects, and inferring things from the definitions – and the meanings that they get from the axioms of the basic objects that underly the definitions.<\/p>\n

In modern math, we typically work by using first order predicate logic as our inference system, with sets (defined by the Zermelo-Fraenkel axioms<\/a>) as their basic objects.<\/p>\n

Often, when you ask someone who dislikes the axiomatic approach to math how to do math without axioms, they’ll say “with definitions”. That answer is a copout. Definitions can be one of two things: they can be axioms, under a different name. Or they can be true definition, which rely on the underlying formal
\nreasoning system – including its axioms.<\/p>\n

The difference, in my jargon here, between a “true definition” and an “axiom” is that a definition defines objects in terms of something else; an axiom is foundational. While that distinction might seem
\nto be splitting hairs, it’s actually quite important. An axiom system has the responsibility of establishing the validity of everything built upon it. If an axiom scheme contains any kind of
\ninconsistency or error, then everything that you do in the formal system – every theorem, every proof,
\nis invalid. True definitions, on the other hand, rely on an axiom scheme for their validity. A definition doesn’t have the strong requirement of validity that the axiom scheme does: you define things in terms of the consistent underlying basis, and so long as you build your construction in terms of the things provided by the axioms and the logic, your definitions will necessarily be consistent.<\/p>\n

One of the subtle points of this – and one of the things that is commonly misunderstood – is how you
\nbuild things in an axiomatic formal system like FOPL+ZF Set theory. When you’re building something in a
\nformal system, you need to make a distinction between the thing that you’re building, and the things that
\nyou’re building it with. You define the set of objects, properties, and operations that you’re interested
\nin studying in terms of<\/em> the underlying system. You can show the validity of your construct by
\nproving the correctness of its essential properties in terms of the underlying construction. But you always keep that clear line distinguishing between the construction and the elements.<\/p>\n

So – let’s look at an example. We generally build the natural numbers from Z-F sets. We say
\nthat 0=∅, 1={0}={∅}, 2={0,1}={{∅},∅}, and so on. Using the usual Peano
\narithmetic construction, we can say that for any integer, it has a unique successor. We show that
\nin set theory by showing how, given a number in set theoretic representation, we can construct its
\nsuccessor: given a number n, s(n) = n ∪ {n}. By doing that, we’ve defined<\/em> the successor operation in terms of set theory. And we can prove the property that each number has a unique successor, by using the ZF-axioms to show that for any set N which is a set-theoretic representation of a natural number, that there is exactly one set N’ such that N’=S(N).<\/p>\n

It’s important to note that it’s not the case that we can arbitrarily use set theoretic operations on
\nour set theoretic numbers, and have the result be meaningful. We can define a set difference operator –
\nbut set difference of numbers M and N won’t necessarily be a valid number. When we’re working in terms of
\nthe construction of natural numbers using sets, we can only use the operations that we defined in the
\nconstruction<\/em>. The set theory is providing us with a tool for proving the validity of our
\nconstruction.<\/p>\n

My favorite metaphor for this is (obviously, given my interests) computer languages. When you write a program in a computer language, you’re writing in terms of abstractions that are very<\/em> different
\nfrom the natural abstractions of the real machine on which the program is executed. For example, a few months back, I wrote a bunch of articles about programming in Haskell<\/a>. In Haskell, you work in terms of functions, without any idea of mutable state. The computer hardware has no concept of a function. But you can write a compiler that implements Haskell functions in terms of the primitive, mutable-state-based
\nmachine language. All of Haskell becomes executable by that translation. But if you were to take a Haskell program, look at the primitive representation of a function, and perform some change to it that makes perfect sense in terms of the machine language, you could end up with something that breaks Haskell – that makes the program crash.<\/p>\n

That’s exactly the same idea as building things in math. You define them (implement them) in terms of
\na low level formal system (machine language), and then build theorems (programs) in terms of the high-level constructions that you’ve built. But if you break the abstraction, you can get into trouble.<\/p>\n","protected":false},"excerpt":{"rendered":"

There was an interesting discussion about mathematical constructions in the comment thread on my post about the professor who doesn’t like infinity, and I thought it was worth turning it into a post of its own. In the history of this blog, I’ve often talked about the idea of “building mathematics”. I’ve shown several constructions […]<\/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-540","post","type-post","status-publish","format-standard","hentry","category-logic"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-8I","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/540","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=540"}],"version-history":[{"count":0,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/540\/revisions"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=540"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=540"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=540"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}