# How would you prove 7 is finite?

**URL:** <https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243>\
**Category:** Factual Questions\
**Created:** [May 31, 2009, 6:13am UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243 "2009-05-31T06:13:53Z")\
**Posts on this page:** 20\
**Page:** 2

<div class="post-metadata">

**Author:** ![DarrenS](https://avatars.discourse-cdn.com/v4/letter/d/977dab/32.png) [@DarrenS](https://boards.straightdope.com/u/DarrenS)\
**Post date:** [May 31, 2009, 7:48pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/21 "2009-05-31T19:48:20Z")

</div>

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.

> [@SaintCad](#):
>
> But his proof is somewhat circular in that how do you know 3 and 4 is finite. Also, under his logic, what is 1+1+1+1+… since one is finite.

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.

> [@Just\_Some\_Guy](#):
>
> Even if he meant “rational” when he said “infinite” it’s kind of in the definition. And then there’s that “proof”. I’m going to go out on a limb and guess that _Infinity and the Mind_ is no _Principia Mathematica_.

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.

> [@Little\_Nemo](#):
>
> I’m not sure I even understand the question. But wouldn’t counting to eight be proof that seven is not infinity and therefore must be a finite number?

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.)

> [@4.66](#):
>
> I like **SaintCad** s solution, but in this context, I’d simply define the property finite as _zero is finite and any direct successor to a finite number is finite_.
> 
> Now we can simply point out that _7 = s(s(s(s(s(s(s(0)))))))_ (in other words 7 is the successor of 6).
> 
> Now I may have used the successor function 7 times here, but since that’s not pertinent to the definition, there’s no circularity (if I hadn’t bothered to count the number of steps needed, that wouldn’t have invalidated the argument)

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?

> [@LSLGuy](#):
>
> IANA expert, but if that’s the author’s idea of a proof, he’s far to clueless to be writing about math.
> 
> His “proof” isn’t exactly circular, but it does require assuming 3 & 4 are finite. Since 7 was arbitrarily chosen and couldn’t be assumed, why can 3 or 4 be assumed? His approach is effectively circular, even if reductionist.

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.

> [@Alka\_Seltzer](#):
>
> I would take 7 marshmallows and eat them. If I did not explode then 7 must be a finite number.

Very apt, given your username!

> [@EdwardLost](#):
>
> Sets can be finite or infinite. Those terms don’t have meanings for individual numbers.

I disagree. In the [set theoretic](http://en.wikipedia.org/wiki/Natural_numbers#Constructions_based_on_set_theory) 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.

> [@Rucker](#):
>
> Can you prove, without circularity, that seven is a finite number?

His answer is as follows:

> [@Rucker](#):
>
> Yes, if you say that seven is three plus four – and if you agree that three and four are finite and that the sum of two finite numbers is finite. The kind of argument which is _not_ acceptable would be to say: “Seven is the sum of a finite number of ones: 1 + 1 + 1 + 1 + 1 + 1 + 1.” For here you are assuming that the given string of seven ones is finite, and this is just what needs to be proved. By the same token, counting up to seven involves seven steps, and could not be used in a proof of the finiteness of seven. It is abstractly possible to imagine beings that count up to infinite numbers without noticing anything wrong!

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.

---

<div class="post-metadata">

**Author:** ![Chronos](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/chronos/32/134_2.png) [@Chronos](https://boards.straightdope.com/u/Chronos)\
**Post date:** [May 31, 2009, 8:04pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/22 "2009-05-31T20:04:16Z")

</div>

Quoth **chrisk** :

> [@](#):
>
> With additional mechanisms for proving the finiteness of a given number x based on other finite numbers, we could address the first few from that list. I suppose this would do for a start:  
> Any number that can be derived using algebraic operations from finite numbers, (addition, subtraction, multiplication, division excluding division by zero, and roots of whatever degree,) is also finite.

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.

---

<div class="post-metadata">

**Author:** ![ultrafilter](https://avatars.discourse-cdn.com/v4/letter/u/3d9bf3/32.png) [@ultrafilter](https://boards.straightdope.com/u/ultrafilter)\
**Post date:** [May 31, 2009, 8:14pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/23 "2009-05-31T20:14:56Z")

</div>

> [@DarrenS](#):
>
> 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.

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.

> [@DarrenS](#):
>
> > [@4.66](#):
> >
> > I like **SaintCad** s solution, but in this context, I’d simply define the property finite as _zero is finite and any direct successor to a finite number is finite_.
> > 
> > Now we can simply point out that _7 = s(s(s(s(s(s(s(0)))))))_ (in other words 7 is the successor of 6).
> > 
> > Now I may have used the successor function 7 times here, but since that’s not pertinent to the definition, there’s no circularity (if I hadn’t bothered to count the number of steps needed, that wouldn’t have invalidated the argument)
> 
> 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?

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

---

<div class="post-metadata">

**Author:** ![Half\_Man\_Half\_Wit](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/half_man_half_wit/32/21766_2.png) [@Half\_Man\_Half\_Wit](https://boards.straightdope.com/u/Half_Man_Half_Wit)\
**Post date:** [May 31, 2009, 8:17pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/24 "2009-05-31T20:17:56Z")

</div>

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?

---

<div class="post-metadata">

**Author:** ![ultrafilter](https://avatars.discourse-cdn.com/v4/letter/u/3d9bf3/32.png) [@ultrafilter](https://boards.straightdope.com/u/ultrafilter)\
**Post date:** [May 31, 2009, 8:24pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/25 "2009-05-31T20:24:52Z")

</div>

> [@Half\_Man\_Half\_Wit](#):
>
> 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](http://en.wikipedia.org/wiki/Extended_real_number_line) or [here](http://en.wikipedia.org/wiki/Real_projective_line) for systems in which it is), so there’s no issue with taking this definition.

---

<div class="post-metadata">

**Author:** ![DarrenS](https://avatars.discourse-cdn.com/v4/letter/d/977dab/32.png) [@DarrenS](https://boards.straightdope.com/u/DarrenS)\
**Post date:** [May 31, 2009, 8:27pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/26 "2009-05-31T20:27:09Z")

</div>

> [@Hari\_Seldon](#):
>
> The given proof depends on induction. Let P(n) be the proposition that n is finite. Assuming, as you must (if you want a proof of this) that the successor of a finite number is finite, then it is clear that n finite implies its successor is, and if you also assume P(0), you conclude that P(n) is always finite.

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.

---

<div class="post-metadata">

**Author:** ![DarrenS](https://avatars.discourse-cdn.com/v4/letter/d/977dab/32.png) [@DarrenS](https://boards.straightdope.com/u/DarrenS)\
**Post date:** [May 31, 2009, 8:30pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/27 "2009-05-31T20:30:15Z")

</div>

> [@ultrafilter](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![EdwardLost](https://avatars.discourse-cdn.com/v4/letter/e/bbe5ce/32.png) [@EdwardLost](https://boards.straightdope.com/u/EdwardLost)\
**Post date:** [May 31, 2009, 8:39pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/28 "2009-05-31T20:39:27Z")

</div>

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!

---

<div class="post-metadata">

**Author:** ![ultrafilter](https://avatars.discourse-cdn.com/v4/letter/u/3d9bf3/32.png) [@ultrafilter](https://boards.straightdope.com/u/ultrafilter)\
**Post date:** [May 31, 2009, 8:42pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/29 "2009-05-31T20:42:27Z")

</div>

> [@DarrenS](#):
>
> 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.

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}}.

---

<div class="post-metadata">

**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\
**Post date:** [May 31, 2009, 9:12pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/30 "2009-05-31T21:12:59Z")

</div>

> [@DarrenS](#):
>
> 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?

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?”](http://www.ditext.com/carroll/tortoise.html), 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.

---

<div class="post-metadata">

**Author:** ![DarrenS](https://avatars.discourse-cdn.com/v4/letter/d/977dab/32.png) [@DarrenS](https://boards.straightdope.com/u/DarrenS)\
**Post date:** [May 31, 2009, 9:13pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/31 "2009-05-31T21:13:44Z")

</div>

> [@EdwardLost](#):
>
> 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!

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

---

<div class="post-metadata">

**Author:** ![Alka\_Seltzer](https://avatars.discourse-cdn.com/v4/letter/a/c89c15/32.png) [@Alka\_Seltzer](https://boards.straightdope.com/u/Alka_Seltzer)\
**Post date:** [May 31, 2009, 9:45pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/32 "2009-05-31T21:45:28Z")

</div>

Why theorise when you can perform an experiment?

> [@Alka\_Seltzer](#):
>
> I would take 7 marshmallows and eat them. If I did not explode then 7 must be a finite number.

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

---

<div class="post-metadata">

**Author:** ![Stealth\_Potato](https://avatars.discourse-cdn.com/v4/letter/s/d78d45/32.png) [@Stealth\_Potato](https://boards.straightdope.com/u/Stealth_Potato)\
**Post date:** [May 31, 2009, 9:55pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/33 "2009-05-31T21:55:43Z")

</div>

> [@EdwardLost](#):
>
> 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!

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.

---

<div class="post-metadata">

**Author:** ![Chronos](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/chronos/32/134_2.png) [@Chronos](https://boards.straightdope.com/u/Chronos)\
**Post date:** [May 31, 2009, 10:41pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/34 "2009-05-31T22:41:17Z")

</div>

Quoth **Indistinguishable** :

> [@](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![Saint\_Cad](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/saint_cad/32/18907_2.png) [@Saint\_Cad](https://boards.straightdope.com/u/Saint_Cad)\
**Post date:** [May 31, 2009, 11:21pm UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/35 "2009-05-31T23:21:13Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\
**Post date:** [June 1, 2009, 1:01am UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/36 "2009-06-01T01:01:06Z")

</div>

> [@DarrenS](#):
>
> (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.)

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,

> [@Indistinguishable](#):
>
> Probably the most famous illustration of this phenomenon…

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.

---

<div class="post-metadata">

**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\
**Post date:** [June 1, 2009, 1:11am UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/37 "2009-06-01T01:11:11Z")

</div>

> [@Chronos](#):
>
> 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.

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.

---

<div class="post-metadata">

**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\
**Post date:** [June 1, 2009, 2:05am UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/38 "2009-06-01T02:05:42Z")

</div>

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, …\>).

---

<div class="post-metadata">

**Author:** ![Chronos](https://sea3.discourse-cdn.com/straightdope/user_avatar/boards.straightdope.com/chronos/32/134_2.png) [@Chronos](https://boards.straightdope.com/u/Chronos)\
**Post date:** [June 1, 2009, 2:19am UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/39 "2009-06-01T02:19:31Z")

</div>

> [@](#):
>
> 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, …\> …} ?

---

<div class="post-metadata">

**Author:** ![Indistinguishable](https://avatars.discourse-cdn.com/v4/letter/i/90ced4/32.png) [@Indistinguishable](https://boards.straightdope.com/u/Indistinguishable)\
**Post date:** [June 1, 2009, 2:38am UTC](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243/40 "2009-06-01T02:38:12Z")

</div>

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.

[Previous page](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243.md?page=1)

[Next page](https://boards.straightdope.com/t/how-would-you-prove-7-is-finite/498243.md?page=3)