On Wed, Apr 10, 2013 at 3:04 AM, Freek Wiedijk <[email protected]> wrote:
> Hi Mike,
>
> >Taking definedness to the level Freek is discussing would,
> >I think, not let you prove that
> >
> > x DIV 0 = x DIV 0
>
> Exactly. I think that what I want is much closer to PVS and
> B than to IMPS. I also don't want any change to the logic.
> I _hate_ partial logics. I want to be able to use all the
> tools that are available for the (standard) total logics!
>
> As I say, I _hate_ partial logics. You get multiple variants
> of equality. With one you can prove `1/0 = 1/0`, with one
> you can _dis_prove `1/0 = 1/0`, and maybe you even have
> other ones too? So I want a world in which writing
> `1/0 = 1/0` is _illegal_ (something akin to a type error).
>
> _And_ want that `!x. 1/x = 1/x` is illegal too (because x
> can take the value 0), but I _also_ want that
> `!x. ~(x = 0) ==> 1/x = 1/x` is fine (even although x
> _still_ can take the value 0). That's how things work in B.
> And this seems unlike IMPS to me.
>
At some phases of the moon this sounds attractive to me too. But my mother
used to say, "Be careful what you wish for, you just might get it." I don't
know B at all, nor how it may arrange to give the proposed results, but if
`!x. 1/x = 1/x` is illegal and `!x. ~(x = 0) ==> 1/x = 1/x` is fine, is it
possible to use the classical propositional calculus definition of the
conditional? (And to define the value of `!x. A` in terms of the value of
`A` at each possible input.) That looks to me like a fundamental change in
the HOL logic.
For me the idea that: "`A = A` for all boolean terms A" is one of the
beauties of classic HOL logic, part of its conceptual elegance. If
determining the value of a term A is a thought experiment, HOL logic says
this is a repeatable experiment. What a wonderful principle!
Perhaps you might achieve a satisfying result by adding equality-like
relations such as (for the real numbers) `reallyEqual`, meaning "the
arguments have determinate real values that are equal" or (for the natural
numbers) `naturallyEqual`, etc.. (Sorry, I don't know the answers to any of
this.)
>
> What I just want is to have some story + infrastructure
> that allows me to -- at the very very end -- prove that
> the result that I have established is "meaningful", in the
> sense that it doesn't depend on/refer to what functions do
> outside their domain. But that apart from that _everything_
> is as it was before.
>
It does sound especially appealing put this way.
Regards,
Cris
>
> Freek
>
------------------------------------------------------------------------------
Precog is a next-generation analytics platform capable of advanced
analytics on semi-structured data. The platform includes APIs for building
apps and a phenomenal toolset for data science. Developers can use
our toolset for easy data analysis & visualization. Get a free account!
http://www2.precog.com/precogplatform/slashdotnewsletter
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
