Monday, November 19, 2018

Do we have to know that seven is finite to know that three is finite?

Three is a finite number. How do we know this?

Here’s a proof that three is finite:

  1. 0 is finite. (Axiom)

  2. For all n, if n is finite, then n + 1 is finite. (Axiom)

  3. 3=0+1+1+1. (Axiom)

  4. So, 0+1 is finite. (By a and b)

  5. So, 0+1+1 is finite. (By b and d)

  6. So, 0+1+1+1 is finite. (By b and e)

  7. So, 3 is finite. (By c and f)

Let’s assume we can answer the difficult question of how we know axioms (a) and (b), and allow that (c) is just true by definition.

I want to raise a different issue. To know that three is finite by means of the above argument, it seems we have to know that the argument is a proof.

One might think this is easy: a proof is a sequence of statements such that each non-axiomatic statement logically follows from the preceding ones, and it’s clear that (d)-(g) each follow from the previous by well-established rules of logic.

One could ask about how we know these rules of logic to be correct—but I won’t do that here. Instead, I want to note that it is false that every sequence of statements such that each non-axiomatic statement logically follows from the preceding ones is a proof. This is the case only for finite sequences of statements. The following infinite sequence of statements is not a proof, even though every statement follows from preceding ones: “…, so I am Napoleon, so I am Napoleon, so I am Napoleon.”

Very well, so to know that (a)-(g) is a proof, I need to know that (a)-(g) are only finitely many statements. OK, let’s count: (a)-(g) are seven statements. So it seems we have to know that seven is finite (or something just as hard to know) in order to use the proof to know that three is finite.

This, of course, would be paradoxical. For to use a proof analogous to (a)-(g) to show that seven is finite, we would need a proof of eleven steps, and so we would need to know that eleven is finite to know that the proof is a proof.

Maybe we can just see that seven is finite? But then we gain nothing by (a)-(g), since the knowledge-by-proof will depend on just seeing that seven is finite, and it would be simpler and more reliable just to directly see that three is finite.

It might be better to say that we can just see that the proof exhibited above, namely (a)-(g), is finite.

It seems that knowledge-by-proof in general depends on recognition of the finite. Or else on causal finitism.

4 comments:

SMatthewStolte said...

Why not just say, “a proof is a sequence of statements such that each non-axiomatic statement logically follows from the preceding ones, provided that the number of steps in the sequence is equal to some natural number”? Then you wouldn’t have to worry about whether seven was finite, because you could tell that seven was a natural number.

Alexander R Pruss said...

Telling that it's a natural number is the same as telling that it's finite, just as difficult. An ordinal is finite iff it's a natural number.

Arnold said...

I suppose the solution must be that you can tell that the proof that three is finite without counting the steps. Say, because you went from the first step to the last step by always going to the next step. And if you need to prove that the proof is finite in order to know that it is finite, then we've just reverted to the old proof paradox: for any proof p, we need to prove that it's a proof with p', and we need to prove that that is a proof with p''...

Alexander R Pruss said...

Yeah, that's helpful. I guess it is related to the old proof paradox. There, presumably the solution is that you can just see that each step is valid. The finiteness issue adds the further problem: Even if you can see that each step is valid, how can you tell that the whole proof is valid? But it is still an instance of the same issue.

The old proof paradox requires us to be able to recognize instances of patterns. But finiteness isn't exactly a pattern. Yet, it does seem to be in the same spirit.

A similar issue comes up when checking if a proof step is an instance of an axiom schema, in that one needs to check that the formulas substituted into the schema are finite.