Re: Implementable Set Theory and Consistency of ZFC

David C. Ullrich wrote:

On Wed, 31 Oct 2007 09:59:33 +0100, Han de Bruijn
<Han.deBruijn@xxxxxxxxxxxxxx> wrote:

Jesse F. Hughes wrote:

I will say it once more. I am typing this slowly, since I don't want
you to miss anything I say. If you have a proof in a theory
consisting of axioms (1)-(4), it is also a proof in the theory
consisting of axioms (1)-(4)+(X).

How do you "know" that? Has the Pope told you, by dogma, that it is so?

No. It's trvial to prove this, from the definition of "proof".

By definition, a proof of A from 1-4 is this: A finite sequence
of statements, such that each statement is either an instance
of 1-4 or a consequence of previous statements, and such that
the last statement is A.

Similarly for "a proof of A from 1-8". So a proof of A from
1-4 _is_ a proof of A from 1-8, because if each line is
either an instance of 1-4 or a consequence of previous
lines then each line _is_ either an instance of 1-8 or
a consequence of previous lines.

So, even if I don't make use of (5-8), a proof of A from (1-4) is a
proof from (1-8) ? So, even if I say "there exists a Foo", then such
a statement is a valid premise for proving that the integral of 1/t
from 1 to x is ln(x) ? Weird ..

Han de Bruijn

.

Relevant Pages