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 R.Standish.domain.name.hidden
Australia http://parallel.hpc.unsw.edu.au/rks
International prefix +612, Interstate prefix 02
----------------------------------------------------------------------------
- application/pgp-signature attachment: stored
Received on Tue Jul 05 2005 - 19:55:36 PDT