Re: [HM] Reassurances from proofs

Augusto Franco de Oliveira (francoli@dmat.uevora.pt)
Sat, 14 Nov 1998 22:17:23 +0000 (WET)

Just to remind collegues that the "proof that if ZF is consistent then ZFC
is consistent" is carried out in ZF, by the method of inner models (Godel,
1939).
AJ Franco Oliveira

On Thu, 12 Nov 1998, Jeremy Smith wrote:

> Hello,
>
> I agree with you in the sense that *I* find our proofs to be more
> reassuring than examples. But that's not the point. It seems to me that
> all of your arguments for the superiority of proofs could be applied
> mutatis mutandis to proof-by-example.
>
> You argue that ZF has 'stood the test of time', in the sense that people
> have tried to find inconsistencies and failed. You feel that this somehow
> makes it more likely that ZF is consistent. Suppose a person has an
> algorithm that has worked for all the cases anyone has ever tried, even
> when people have been specifically searching for failure. This strikes me
> as a perfectly analogous situation. In both cases, there are countably
> many (hence impossibly many) cases to check, and the people are gaining
> confidence in their thing based on a finite collection of cases.
>
> As for the *proof* that ZFC is consistent if ZF is consistent, I should
> remind you that this, too, could be false in the same way that a theorem
> *in* ZF could be false. Namely, whatever meta-system we're using could be
> inconsistent.
>
> Incidentally, one argument that someone might make is that a savage
> believer in unproved algorithms would, in general, be more likely to be
> reassured than a believer in proofs. It is easy to construct algorithms
> that work for billions of cases and then fail. For such an algorithm, our
> savage will be reassured of its correctness while people as superior as we
> would not be.
>
> This is in fact true, but it doesn't generalize. There are, I agree,
> cases where one reassured by examples would be tricked while one reassured
> by theorems would not. On the other hand, if ZF in inconsistent, there
> are also cases where a prover would be assured but an examplemeister
> wouldn't. For example, there may be an algorithm or a formula that is
> horrendously difficult to compute, and for which there exists a
> correctness proof. If the proof is in error (in either of the ways I've
> mentioned) then the prover would be in the position of the savage from the
> last paragraph, and vice versa.
>
> Hope you can make sense of the mess above.
>
> -Jeremy