On 16 May 2000, Carl R. Witty wrote:
> "Jan Brosius" <[EMAIL PROTECTED]> writes:
>
> > > SORRY, this is quite TRUE , in fact [forall x. alpha(x)] <=> alpha(x)
> > >
> > > the above true equivalence seems to be easily considered as wrong . Why?
> > > Because alpha(x) is TRUE can be read as alpha(x) is TRUE for ANY x.
> > >
> > > (Is there something wrong with the education of a computer scientist?)
>
> Jan, could you tell us whether you think the following statements are
> true or false?
>
> Let prime(x) mean "x is a prime number".
>
> 1. [forall x. prime(x)] <=> prime(x)
> 2. forall x.([forall x. prime(x)] <=> prime(x))
[snipped]
So far I've avoided stepping into of an this increasingly rancorous
discussion but... could I just check that what I think both sides mean
when the write "=>" & (so "<=>") is what I think it is?
That is "=>" is a symbol within the set of formulae whose relations
are defined by the logic under consideration which
combines to formulae to produce another formula, which may be (a)
provable under the set of axioms of the theorem and hence (b) is said to
be a true statement in the system under the consideration (I'd prefer to
say it's a `result', `theorem', etc since there's a grave danger of
confusing true as in the value of certain boolean formulae in the system
and true as in `this statement is a correct result in the logic'). If so
then I certainly agree with Carl, but I half suspect that in the snippet
above Jan is using it in the sense of what I'd write as X -||- Y, ie
`an occurrence of a formula X in a proof can validly be replaced by
formula Y'. If this is so, then it's clearly non-sensical to write
forall x ([forall x.prime(x)] -||- prime x)
because forall is a symbol in the formulae whose relations are defined and
examined in the logic under consideration, and the implicit quantification
would instead be
[forall x.prime(x)] -||- [forall x.prime(x)]
ie, a tautology.
(I may well be wrong: third year undergrad logic was _way_ to long
ago.)
___cheers,_dave________________________________________________________
www.cs.bris.ac.uk/~tweed/pi.htm|I shoulda realised building the
email: [EMAIL PROTECTED] |memory allocation subsytem with
work tel: (0117) 954-5253 |--with-malicious-ai was a bad idea.
