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.


*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

Attachment: pgp4kHcDcinhc.pgp
Description: PGP signature

Reply via email to