How would you prove 7 is finite?

Returning to my own party a bit late, here. Thanks for the considered responses. I’ll try to address some of them.

I had come up with my own proof (which the margin below will certainly be large enough to contain) but I didn’t want to bias others before posting. SaintCad’s proof is very close to what I came up with.

In his pseudo-proof, he is assuming that 3 and 4 are finite. Also, he only asserts the the sum of a finite number of finite numbers is finite, so 1+1+1… is allowed to be (and is) infinite.

As ultrafilter says, Prof Rucker is a respected mathematician, and while this is intended to be a popular book, the mathematics is (are?) sound. I’m sure he’s offering the 4 + 3 = 7 proof tongue-in-cheek, just to get the reader to question his own assumptions.

No, because you may have counted infinitely many steps to get there without realizing it. Be careful of statements like, “Well, I obviously didn’t count infinitely many steps!” – those are dangerous in proofs. Your assertion implicitly assumes that 8 is finite. If your system of axioms includes one that “8 is finite”, and you have another that says “anything less than a finite value is finite”, then you would have proved it according to your axioms. But we try to have a minimal set of axioms, and in that case you’d need one for each natural number (“9 is finite”, “10 is finite” etc.)

But how many s’s are there in that equation? How do you know it’s a finite number? I’m not being cute or obtuse here, of course we all “know” it’s a finite number, but how do we “know” that? How do you know you didn’t use the successor function an infinite amount of times without realizing it?

He gives no justification for why 3 and 4 are finite, but takes them as given. Again, I’m sure this is tongue-in-cheek and not considered to be a formal proof of anything.

Very apt, given your username!

I disagree. In the set theoretic construction of the natural numbers, each number is precisely associated with a single set, namely the set of all numbers less than the number. Then we can say that the number is finite if the associated set has finite cardinality, and vice versa.

For the record, I’ll post the original “puzzle” verbatim, along with Prof Rucker’s answer. I was quoting from memory before but now I found the book.

His answer is as follows:

To answer’s ultrafilter’s question, the book is very set-theoretic in focus, though he gives plenty of time to the Peano axioms too. He is gently guiding the reader towards infinite ordinals/cardinals (can never remember the difference).

Here’s my “proof”, which I already emailed to Rucker to see what he thinks. I’m very much an armchair mathematician so it’s quite likely there’s a flaw in this.

How to show that 7 is finite, by using the set theory definition of 7:

(this is the shaky part) A set is finite iff it cannot be put in 1-1 correspondence with a proper subset of itself. (Is that true? I know it’s a sufficient condition for a set to be infinite that it can be put in 1-1 correspondence with a proper subset.)

Constructing 7 using the set approach:

{} = 0
{{}} = 1
{ {{}}, {} } = 2
… etc.
(lots of curly braces) = 7

Eventually you have a set theoretic definition for 7, which could be a set with infinity cardinality – we have neither proved nor assumed that yet. Enumerate the proper subsets, and show that the set representing 7 cannot be put in 1-1 correspondence with any of those listed subsets, so the set representing 7, and ergo 7 itself, cannot be infinite and are therefore finite.

I find it interesting that people have two kinds of reaction to this type of problem: either, “WTF…of course 7 is finite! What a stupid question!” vs. “Hmm…yes, how could we prove that while introducing the fewest number of axioims?”

A lot of results in the world of math seem intuitively obvious, but either can be proved from a much smaller set of axioms or turn out to be wrong. This is especially true in the world of infinite sets…e.g. there are “obviously” more natural numbers than there are prime numbers, and “obviously” more natural numbers than there are perfect squares, right?

I highly recommend the book, by the way, for anyone interested in math. Someone recommended it to me on the Dope years ago, and I’ve read through it many times.

Quoth chrisk:

Doesn’t work. Consider, for instance, \Sigma_{n=0}^\infinity 1 (that’s 1+1+1+1+1+1+…). That’s something derived using algebraic operations from finite numbers, but it certainly doesn’t result in a finite number. You could get a fair amount of mileage by restricting your constructions to two finite numbers at a time, and building more finite numbers out of the ones you get that way. Personally, though, I’d prefer to just say that X is finite iff there exist finite numbers Y and Z such that Y < X < Z; Y and Z are both nonzero; and sgn(Y) = sgn(Z). That way, you can say that pi is finite, for instance, because 3 < pi < 4, and 3 and 4 are both finite.

This is the same proof that SaintCad offered above, and my previous criticism of it still stands–it’s valid for a particular construction of the natural numbers, but not for all of them. For any given construction, you can use a similar argument to show that 7 is finite, but you’d need an infinitely long combination of such arguments to prove that 7 is finite for any construction.

To do so, you need a proof that follows from the axioms of natural numbers, which are the Peano postulates. That’s where the argument given by Hari Seldon (which is a more explicit version of 4.66’s argument) comes in.

Even in mathematical set theory, some things are just obvious.

Hmm, nobody addressed my doodlings… Are they so horribly misguided that they’re not even worth talking about? Isn’t there some merit in taking those numbers to be finite that are limits of convergent sequences?

It’s not a bad idea, but you’d have to be very careful of introducing circularity, and there’s also a much simpler notion of finitude for real numbers: every real number is finite. Infinity is not a real number (see here or here for systems in which it is), so there’s no issue with taking this definition.

You mean P(n) is always true, rather than P(n) is always finite, right? Since P(n) is “the proposition that n is finite”?

Anyway, I think I see what you’re getting at.

Axioms:

A1: P(0) holds.
A2: if P(n), then P(n+1)

Working through this:

P(0) - axiom
P(1) - via A2
P(2) - via A2 and P(1)

therefore P(7).

I see how this gets around the circularity; although we have applied induction 7 times, the proof doesn’t rely upon 7 being finite. We may have accidentally applied induction an infinite amount of times, but that doesn’t change the conclusion, namely, P(7). Well played.

I see where Hari’s coming from, but doesn’t that proof only hold for the Peano construction of the natural numbers? The proof that SaintCad and I came up with only holds for the set-theoretic construction, but Hari’s proof only holds for the Peano construction…right?

Or is it that there is something canonical about the Peano construction, something that is more fundamental than the other possible constructions? I’m not asking this sarcastically…I honestly don’t know if the Peano construction enjoys a special, “more definitive” position than other constructions.

This is just screwing around with ill-defined terms.

X is a fleeble. All fleebles are the sum of X and some other fleeble. All fleebles are blurg. Proof that Y is blurg: Y is the sum of X and some other fleeble and is thus a fleeble and is thus blurg.

Wrong! Y is a floogle, not a fleeble!

There’s no Peano construction. The Peano postulates are a collection of properties that anything you want to call the natural numbers should have, and they’re only special in the sense that most people agree with that statement. The objects defined by 0 = {} and s’ = s + {s} (forgive my abuse of notation) are not the only possible models for the Peano postulates; for instance, consider the objects defined by 0 = {} and s’ = {s}, or 0 = {} and s’ = {0, {0, s}}.

This is a very salient point, I would say, and indeed, I assume without having read any Rucker, is what he was getting at.

The response to this point being: as with the response to any thoroughgoing foundational skepticism, you do know and you don’t know, in various senses. That is, if we’re going to be talking about formal proof at all, we need some a priori conception of what a formal proof is. Often, one of the properties one has in mind for what constitutes a formal proof is that it needs to have only finitely many steps, in some appropriate sense. But, whatever this constraint amounts to, it can’t be the case that every formal proof P needs to be accompanied by a further formal proof Q that the number of steps in P is finite… for then we would need to also adduce a formal proof R that the number of steps in Q is finite, and adduce another proof of the finitude of R, and so on, into unending regress. [Or, rather, one could make such stringent demands, but only if one were satisfied with an account of “formal proof” in which none actually exist]

So all any typical proof system talking about finiteness does (and could ever hope to do) here is to import into the object theory (i.e., the formal system you are studying) the notion of “finiteness” which already exists in the background metatheory (i.e., whatever (necessarily pre-formal) language was ultimately used to specify what counts as a valid formal proof). Whatever it is that you’ve taken as allowable proof lengths, that’s what the word “finite” is crystallized by the axioms to correspond to.

A similar thing happens with all sorts of concepts, though; not just “finiteness”. For example, I might take as a rule of my formal proof system that if you have a proof of A and you have a proof of B, then this counts as a proof of A & B.

Fine. And suppose I’ve also happened to prove A. Plus, I’ve happened to prove B. Now I want to prove A & B. What do I do?

Well, I need to establish that I have both a proof of A and a proof of B to be able to use the one relevant rule in my formal proof system. But this requires me to be able to move from “I have a proof of A” and “I have a proof of B” to “I have a proof of A and a proof of B”. So I need some pre-formal account of conjunction in my background metatheory in order to make use of any formalization of conjunction in the object theory.

Probably the most famous illustration of this phenomenon is in Lewis Carroll’s “What the Tortoise Said to Achilles?”, demonstrating how one cannot make us of a formalization of the rule of modus ponens (in an object theory) without first having some pre-formal accounting of modus ponens already in the metatheory.

A lot of math (and philosophy!) is about getting definitions nailed down. Which terms here do you think are ill-defined?

Why theorise when you can perform an experiment?

Despite the obvious dangers, I am prepared to try this out tomorrow.

I’m not sure what exactly you meant to show with your example, but there’s nothing particularly ill-defined here, as far as it goes. The clear problem with the “proof” is that you’re affirming the consequent by reversing the implication (A is a fleeble -> A is the sum of X and a fleeble). Nothing in your definitions precludes non-fleeble objects that are the sum of X and a fleeble.

Quoth Indistinguishable:

I presume you’ve read Hofstadter’s Gödel, Escher, Bach? If not, you should. He takes the tortoise far beyond the level of Carroll’s version.

Some didn’t like my proof since it only worked for natural numbers.

The point is that there needs to be definitions and axioms to develop proofs in mathematics. I actually do not like the proof that Rucker gives since I believes his proof while not circular certainly leaves “finite” undefined. I also do not like his proof since he all but discounts constructive proof which many mathematicians consider to be a superior type of proof over existance proofs.

Rucker’s proof boils down to
If P(a) is true and P(b) is true, than P(a+b) is true
P(3) is true and P(4) is true
but notice that since P(A) is undefined, there is know real justification for his statement. Therefore he is presenting this as an axiomic system

All of our proofs are superior to his because at some point we all define “finite”. My favorite proof would be to define n as finite if there exists a natural number a such that -a<n<a. I would then walk 8 steps to show 7 is finite.

He has a point in that it assumes 8 is a non-infinite number which is a perfectly valid a priori concern - but he neglects that once I prove 8 (or 7 in his example) is finite by construction i can use that knowledge a posterior.

This is certainly one formal notion of finiteness, called Dedekind-finiteness. As Hari Seldon hinted at, there are many different common formal conceptions of finiteness, which can come apart (i.e., turn out non-equivalent) in contexts without such strong principles as the axiom of choice and the law of excluded middle available. In such contexts, Dedekind-finiteness is (as you basically note) generally implied by any other kind of finiteness; however, it’s also very rarely the notion of finiteness one actually wants, inductively-based definitions generally being more relevant. So even in contexts where such principles are around as to prove the equivalence of Dedekind-finiteness and other conceptions, it may be best to consider another formalization as more direct.

For example, let us say that a property of sets is inductive if two things happen: it holds true of the empty set, and also, whenever it holds true of some set S, then it holds true of any set you can create by taking S and adding to it a single element not already in S.

Let us now say that a set is Peano-finite, or strongly Kuratowski-finite, just in case it satisfies every inductive property. This is very often the notion one wants; in particular, if one has a notion of natural numbers around which satisfies the Peano axioms, then we can say that a set has natural number size n just in case it can be put in bijection with those natural numbers below n, and it’ll turn out that a set is Peano-finite just in case it has some natural number size.

[There is another, slightly different standard definition for what it means to be Kuratowski-finite, which in “classical” contexts is equivalent to this, but in general is slightly weaker than this (hence my introduction of the word “strongly” above). But I shall not dwell on this right now.]

Anyway, that’s all by means of giving different formalizations of “finiteness”, but whichever formalization you go with, the points in my last post still apply.

Speaking of which,

Returning to this phenomenon specifically in the context of “finiteness”, I should have made one thing more clear: whatever the notion of “finite” in one’s metatheory, the notion imported by axioms to one’s object theory will be at least as inclusive, but it may be even more so. That is, whatever is considered finite in the metatheory corresponds to something finite in the object theory; however, there may also be things finite in the object theory which aren’t finite in the metatheory.

Perhaps an illustration is in order: let’s talk about Fréchet-world. What’s Fréchet-world, you ask? Fréchet-world is a particular foundational theory which axiomatizes the mathematical universe.

Ok. What is it? Well, the terms of this theory are just infinite sequences of mathematical objects. So, for example, there are terms <5, 5, 5, 5, 5 …>, <0, 1, 0, 1, 0, 1, …>, and <3, 1, 4, 1, 5, 9, …> which represent integers, a term like <sin(x), cos(x), x^2, …> which denotes a function from reals to reals, and so on.

What about operations on terms? Well, we do these component-wise; so <5, 5, 5, 5, …> + <0, 1, 0, 1, 0, 1, …> comes out to the term <5, 6, 5, 6, 5, 6, …> and so on.

And, finally, what dose Fréchet-world actually prove about these terms? For example, which integer terms are provably even? Which are provably odd? Which are neither? Well, in Fréchet-world, we can prove that a term has a property just in case all of its components from some point on have that property. So, for example <2, 2, 2, 2, …>, <0, 1, 2, 3, 4, 2, 4, 2, 4, 2, …>, and <9, 1, 1, 0, 2, 4, 6, 8, 10, …> are all provably even, while <0, 2, 4, 1, 3, 5, 7, 9, 11, …> is provably odd, and <0, 1, 0, 1, 0, 1, …> is neither provably even nor provably odd.

So we know what the terms are, how to combine them with any operation we like, and how to ask if the results satisfy any property we like. As long as this all interplays coherently, we have a bona fide foundational mathematical theory. And, indeed, you can easily verify for yourself that every particular true axiom and every valid formal proof rule applies just fine in Fréchet-world [e.g., we have modus ponens: if “A” is provable and “A implies B” is provable, then “B” is provable as well]. (Key to this working out is that formal proofs are finitary objects, so they never make use of more than finitely many premises)

Ok, so what? What’s interesting about Fréchet-world?

Well, for one thing, consider the term <{}, {0}, {0, 1}, {0, 1, 2}, {0, 1, 2, 3}, …>. In Fréchet-world, this is provably finite, even though it also provably contains 0 (which can be identified with <0, 0, 0, …>), contains 1, contains 2, and so on.

There is, in Fréchet-world, a natural number which it provably doesn’t contain, though; specifically, <0, 1, 2, 3, 4, 5, …>. But this is, again, provably larger than 0, provably larger than 1, provably larger than 2, and so on.

So, from the perspective of our Standard-world out of which we constructed Fréchet-world, what happens is that every Standard-world finite quantity is still considered finite in Fréchet-world; however, Fréchet-world also has some further entities within it which it considers finite but which are too large to be thought finite in Standard-world.

But what’s more, Fréchet-world thinks there is a proof that <{}, {0}, {0, 1}, {0, 1, 2}, {0, 1, 2, 3}, …> is finite. After all, if you have some uniform way (here in Standard-world) of proving that each of its components is finite, then you can string them together into a term which Fréchet-world thinks is a legitimate finite proof. From the perspective of Standard-world, it wouldn’t be a legitimate finite proof, but that’s to be expected, since Standard-world is stricter than Fréchet-world about what counts as finite.

And Standard-world is just a generic term for “Whatever world I happen to be working in at the moment”. Fréchet-world considers itself to be the “Standard world”, and cannot see the “actual” Standard-world. Indeed, the construction which took Standard-world to Fréchet-world can be internalized and carried out within Fréchet-world itself to yield something which Fréchet-world considers to be “Fréchet-world” (but which our initial Standard-world would have to call “Fréchet^2-world”). And so on and so forth.

Anyway, the point is, there’s no point asking “Am I working properly in Standard-world or illegitimately in Fréchet-world? When I prove that something is finite, is it a legitimate proof, or might I be making that mistake Fréchet-world makes of accidentally using a proof that’s only Fréchet-world finite and not Standard-finite?”. (Which is what foundational skepticism over how to ascertain the legitimating finitude of proof amounts to). Because “Standard-world” is only a relative term. Fréchet-world is, in every internal way, absolute indistinguishable from Standard-world; Fréchet-world thinks it is “Standard-world”, and that it’s Fréchet^2-world which is actually “Fréchet-world”, and so on. The things which distinguish Fréchet-world from Standard-world are not things which it is possible to see from within Fréchet-world; the distinction can only be seen from an external viewpoint whose existence, so far as Fréchet-world goes, can be postulated or not without changing anything.

Ah, yes, I have, though now rather a long time ago; it’s one of those books which I once enjoyed enough that I dutifully carry it to every new place I move, yet I haven’t actually cracked open in years. I really should, though, even if only to see how different or not the experience of reading it would be now.

Two clarifications about Fréchet-world to pre-emptively address common questions and points of confusion:

A) Although <0, 1, 0, 1, 0, 1> is neither provably even nor provably odd, it is provably (either even or odd).

B) There is no set in Fréchet-world which contains precisely those natural numbers which come from Standard-world. For example, if N is the Standard-world set of natural numbers, then the corresponding Fréchet-world set <N, N, N, N, …> does indeed contain every Standard natural number… but it also contains every nonstandard natural as well (e.g., it contains <0, 1, 2, 3, 4, …>).

Couldn’t you have the set {<0,0,0,0,0, …>,<1,1,1,1,1, …>,<2,2,2,2,2, …> …} ?

Well, a term in Fréchet-world is an infinite sequence of objects. But what you’ve provided is not an infinite-sequence of objects.

Specifically, you’ve provided a set of infinite sequences of natural numbers. However, a Fréchet-world X is an infinite sequence of Xes; thus, a Fréchet-world (set of natural numbers) would have to be an infinite sequence of sets of natural numbers.

So the problem here is that “infinite sequence of _” and “set of _” don’t quite commute.