[Prev][Next][Index][Thread]
Re: specification logic, intuitionistic logic
Kurt: I have quite a different attitude to the "questionable" axioms.
At this point, it is only their utility that is in question, not their
validity. So if in fact these axioms are not all that useful and the
intuitionistic nature of the theory arises "naturally" from the kind
of model being used, this doesn't suggest to me that such axioms should
be discarded, but rather that we don't yet have axioms that sufficiently
exploit the possibilities of an intuitionistic programming logic.
I would expect that specification logic will evolve into a theory that
is more rather than less intuitionistic. In particular, I hope that
the idea underlying Reynolds' Non-interference Composition axiom
can be used in axioms that will replace the invalid higher-order
instances of Noninterference-Decomposition and Variable-Declaration
axioms.
About full abstraction: you are correct that x:=x+1; x:=x-1 and
skip are not equivalent; but this is not a failure of full abstraction.
There ARE contexts that allow this distinction to be detected;
they happen to be logical rather than operational contexts. I
don't see that this has anything fundamentally to do with classical
versus intuitionistic logic.
Regards, Bob.