Re: Implementable Set Theory and Consistency of ZFC



On Wed, 24 Oct 2007 15:57:41 +0200, Han de Bruijn
<Han.deBruijn@xxxxxxxxxxxxxx> wrote:

David C. Ullrich wrote:

On Wed, 24 Oct 2007 09:50:42 +0200, Han de Bruijn
<Han.deBruijn@xxxxxxxxxxxxxx> wrote:

MoeBlee wrote:

On Oct 23, 4:23 am, Han de Bruijn <Han.deBru...@xxxxxxxxxxxxxx> wrote:

1. Extensionality 5. Specification X. Infinity
2. Empty set 6. Substitution
3. Pairing 7. Power Set
4. Union 8. Foundation
9. Choice

And, as I've said, in this "model", only (1-4) are necessary as axioms,
because (5-9) appear as theorems. And (X) is not part of the "model".

I just saw Virgil's post, which made me realize I overlooked that you
said 5-9 are theorems of 1-4!

You're wrong. None of 5-9 is derivable from all of 1-4.

What you might mean is that in a certain model of 1-4, we have that
5-9 are true in that model. But that does not ENTAIL that any of 5-9
are theorems of 1-4.

You are wrong. Read the article.

Just for fun I downloaded it and looked at it.
The supposed proof of (5) is this:

Think you mean (8) Foundation, throughout the following.

"Theorem. The minimal element in a set, when implemented
as a natural array, is always disjoint from the set.
Proof. This is a direct consequence of the above lemma:
the leftmost bit position of an integer >= 0 has a numeric
value which is always less than the numeric value of the
integer itself.
This completes the proof, of the assertion that the axiom
of Foundation is just a Theorem in our implementable set
theory."

All that stuff about bit positions is specific to your
"model". Sure enough, exactly as Jesse conjectured,
it's _not_ a proof that 5 follows from 1-4 as you
insist, it's just a proof that 5 is true in your
"model".

At most it's a proof that 5 is true of the hereditarily
finite sets. That's not what you've been insisting
it is, in particular it is simply _not_ a proof that
5 follows from 1-4.

Any (implementable) set is a hereditarily finite set, anyway.

Which of course is not surprising, since 5 does not
follow from 1-4.

Once you've entered my universe, you're plain wrong.
But I think much of the confusion rather stems from poor terminology.

http://en.wikipedia.org/wiki/Computable_function

Modified quote. Replacing "function" by "SET":

According to the Church-Turing thesis, computable SETs are exactly the
SETs that can be calculated using a mechanical calculation device given
unlimited amounts of time and storage space. Equivalently, this thesis
states that any SET which has an algorithm is computable. Consequently:
"Implementable Set Theory" has been renamed to "Computable Set Theory".

http://hdebruijn.soo.dto.tudelft.nl/jaar2007/set_theory.pdf

Does that make things better? Is it an improvement?

In fact the idea that you think this helps is sillier than
I realized at first. Because all the sets in your gizmo are
finite - computable sets are not necessarily finite.

Han de Bruijn


************************

David C. Ullrich
.



Relevant Pages

  • Re: Implementable Set Theory and Consistency of ZFC
    ... to me that it is a minimal model and, as you say, is true in that ... theorems HAVE to appear AS axioms. ... these axioms ... Choice is a theorem in the theory of finite sets. ...
    (sci.math)
  • Re: Implementable Set Theory and Consistency of ZFC
    ... And, as I've said, in this "model", only are necessary as axioms, ... because appear as theorems. ... computable SETs are exactly the ... SETs that can be calculated using a mechanical calculation device given ...
    (sci.math)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... you are using them in a standard way in CBL. ... assertion that the set of theorems is ... Any system where PR being the set of theorems satisfies the axioms. ... theorems or truths of any given system besides your say so. ...
    (sci.logic)
  • Re: primitive recursive: obsolete?
    ... we have to add more axioms. ... all true sentences of arithmetic in the language of PA. ... logic we define the set of sentences true in the standard model of PA ... theorems" or not has no bearing on the fact that what I said is ...
    (sci.logic)
  • Re: Godel proved maths inconsistent not incompleteness theorem
    ... It's the *axioms* ... If no more theorems to generate, ... Otherwise it's not an axiomatic system. ... The program was to be able to rewrite all mathematics starting using ...
    (sci.logic)