sci.logic
[Top] [All Lists]

Re: Why Has None of Computer Science been Formalized?

Subject: Re: Why Has None of Computer Science been Formalized?
From: Bill Hale
Date: Tue, 03 Oct 2006 19:48:04 -0500
Newsgroups: sci.logic
In article <1159912824.883725.67590@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
 "Charlie-Boo" <shymathguy@xxxxxxxxx> wrote:

> Bill Hale wrote:
> > In article <1159899594.291222.133100@xxxxxxxxxxxxxxxxxxxxxxxxxxx>,
> >  "Charlie-Boo" <shymathguy@xxxxxxxxx> wrote:
> >
> > > > > > > http://www.arxiv.org/html/cs.lo/0003071
> > >
> > > > In the section "IV. An example from Number Theory", you give the
> > > > following definition:
> > > >
> > > >      4.  MUL(a,b,c) , MUL(a,b,c) ^ ~LT(c,a)               a * b > a
> > > >
> > > > This doesn't seem to be a definition of MUL(a,b,c). I find this
> > > > confusing and misleading.
> > > >
> > > > Bill Hale
> > >
> > > Thanks for the interest.  DEF 4 states that MUL(a,b,c) is equivalent to
> > > MUL(a,b,c) ^ ~LT(c,a), but is not meant to capture enough information
> > > to completely define MUL.
> >
> > But, you are not saying that the two are equivalent. You are saying that
> > the two are equivalent *by definition*.
> >
> > This is confusing. You are misusing the word "definition".
> 
> (I am actually calling them DEF, for what it's worth.)  That is
> debatable in this case, but think of the reasons that we might know
> that two wffs (relations) are equivalent. 

Two wffs might be equivalent because the second wff is defined to
be the first wff. Or, two wffs might be equivalent because the second
wff is proved to be equivalent to the first wff.

>The DEF in the paper show a
> number of scenarios, such as:
> 
> 1. P , ~~P

This would be a theorem or an axiom.
It would not be a definition.

> 2. P^Q , Q^P

This would be a theorem or an axiom.
It would not be a definition.

> 3. P(a) , (eA)P(A)^EQ(A,a)

This would not be a definition.

> 4. FAC(a,b) , (eA)MUL(A,a,b)

This should be a definition.

> 5. HALT(a,b) , YES(a,b)vNO(a,b)

I haven't read what you mean by this yet.

> What would you call each of these?  I think it is natural to say that
> these are true by definion of ^, EQ, FAC, MUL, HALT etc.

You are now giving another meaning for "true by definition", or at least
using it in a third meaning.

"2. P^Q , Q^P" is true by definition does not mean the same as
"2. P^Q , Q^P" is true by definition of "^".

Is this what you are saying:

     2. P^Q , Q^P since it is true by definition of ^

That is not a definition.

I am confused. You need to explain more.

I would say the following:

    "4. FAC(a,b) , (eA)MUL(A,a,b)" is not true by the definition of
    FAC and MUL. 

    "4. FAC(a,b) , (eA)MUL(A,a,b)" is true because it is the definition
    of FAC.

> What would you suggest as a better name?

Fact. Basic fact.

But, if it is not a definition, then you need to prove it or reference
where it is proved. It seems like you are saying that it doesn't need
a proof since it is a definition. This would require that CBL needs
more than just 8 or so axioms that you are claiming.

> I think that DEF (definition)
> is the best single general concept for these.

No. Definitions have certain requirements that you are not following.
You can't define Q^P to mean P^Q for example.

> After all, doesn't
> everything boil down to the definitions?

No. Definitions are not needed: they are just a convenience.

Bill Hale

<Prev in Thread] Current Thread [Next in Thread>
Privacy Policy