Re: Coming soon -- new proof checking software

[EMAIL PROTECTED] (Charlie-Boo) wrote in message news:<[EMAIL PROTECTED]>...
> "Dan Christensen" <[EMAIL PROTECTED]> wrote
> > Within a week or so, I will be releasing a free beta version download for my
> > new proof checking software, DC Proof 1.0.
> > 
> > In the mean time, here is a sampler from the User Guide:
> > 
> > http://members.allstream.net/~dchris/DCProofT.chm
> > 
> > It contains a tutorial that illustrates many of the main features of DC
> > Proof. Readers may be interested in both theoretical and a pedagogical
> > aspects of this application. Example 3, is a resolution of Russell's Paradox
> > without the usual prohibition on self-reference.
> > 
> > Enjoy.
> > 
> > Dan Christensen
> > Toronto, Canada
> 
> Your system appears to be a great aid to logicians writing proofs, and
> will also hopefully lend more insight into the exact nature of proofs.
>  I will be happy to obtain a copy.
>

Thank you.

 
> While a great bookkeeping aid, your system doesn't seem to do anything
> that isn't being done by hand already.

Agreed.


  Indeed, the user explicitly
> enters the proof itself.  This is a helpful tool, but I don't see how
> you have "resolved" the Russell Paradox.  You have only computerized
> the same proof that is written out by hand.  You correctly (IMHO)
> conclude that there is no Russell Set (the set of sets that don't
> contain themselves), which is the common conclusion one reaches from
> seeing the contradiction.
> 
> However, the question remains, what do we do about it?  How do we
> define sets to include the sets that mathematicians use, but exclude
> the Russell Set?  Are you simply saying don't allow it?  But what do
> we allow?  "Everything else"?
>

No. But if postulating the existence of a particular set leads to a
contradiction, then that set is said to not exist.

To play it safe, I don't actually postulate the existence of any set
in my theory of sets -- not even the empty set. That way, if I get a
contradiction from, say, a premise giving Peano's Axioms for the set
of natural numbers (previous posting), I would have to conclude that
the set of natural numbers, as defined by PA, cannot exist.


> ZF and various other axiomitizations of set theory attempt to define
> sets in a way that that meets these two needs (completeness without
> contradiction.)  Do you really have a solution to that problem?
>

I'm not sure. Maybe.

Dan