On Tue, Jul 05, 2005 at 04:03:11PM +0200, Bruno Marchal wrote: > > > >If D'P = BP & ~B~P & P, then D'P => P (ie necessitation). So it seems > >it is the conjunction of truth of P that gives rise to necessitation, > >no? > > > No. Necessitation is the inference rule according to which if the > machine proves (soon or later) the proposition p then the machine will > prove soon or later D'p. D'p -> p is the reflexion axiom for D' > (indeed true for the logic obtained by applying Theaetetus 1 and 3 on > G). > Er ... Russell, if I have been wrong or especially unclear on that > point somewhere in SANE or another paper I would be very pleased in > case you tell me precisely where. I am quite able to confuse terms > myself! >
You are right, my apologies. I read the necessitation rule backwards
in your thesis. You do in fact say P => []P. I'll take your word for
it that consistency destroys necessitation, but I don't have the
intuitive understanding of it yet. Never mind, it is enough for my
present purposes.
Cheers
--
*PS: A number of people ask me about the attachment to my email, which
is of type "application/pgp-signature". Don't worry, it is not a
virus. It is an electronic signature, that may be used to verify this
email came from me if you have PGP or GPG installed. Otherwise, you
may safely ignore this attachment.
----------------------------------------------------------------------------
A/Prof Russell Standish Phone 8308 3119 (mobile)
Mathematics 0425 253119 (")
UNSW SYDNEY 2052 [EMAIL PROTECTED]
Australia http://parallel.hpc.unsw.edu.au/rks
International prefix +612, Interstate prefix 02
----------------------------------------------------------------------------
pgp4kHcDcinhc.pgp
Description: PGP signature
