My comment is about how this is done in HOL, where the existing axiomatization is sufficient to give the behaviour as I have explained it.
Michael From: Saburou Saitoh <saburou.sai...@gmail.com> Date: Saturday, 10 August 2019 at 10:28 To: "Norrish, Michael (Data61, Acton)" <michael.norr...@data61.csiro.au> Cc: "Chun Tian (binghe)" <binghe.l...@gmail.com>, hol-info <hol-info@lists.sourceforge.net> Subject: Re: [Hol-info] 0 / 0 = 0 ??? Dear Michael For x/0, the essential problem is on its definition. I think the division by zero is trivial and clear all. However, we will need a new axiom. So, I would like to ask for your kind help for the axiom problem; Foundation of Mathematics. Please look the draft: viXra:1908.0100<http://vixra.org/abs/1908.0100> submitted on 2019-08-06 20:03:01, Fundamental of Mathematics; Division by Zero Calculus and a New Axiom With best regards, Sincerely yours, Saburou Saitoh 2019.8.10.9:25 2019年8月10日(土) 9:07 Norrish, Michael (Data61, Acton) <michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au>>: It’s still defined inasmuch as it is perfectly legitimate to write x/0 and use that term to define other things in turn. For example, I can define foo = x/0 + 1 and then quite successfully prove that x/0 < foo. I would avoid the use of the word undefined in this context; rather x/0 has an unspecified value. All functions are total so all applications of functions to all possible arguments have values. Michael > On 9 Aug 2019, at 21:46, Chun Tian (binghe) > <binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>> wrote: > > A follow-up of this old topic: > > Finally I found the following definitions of `extreal_inv` and `extreal_div` > based on new_specification(): > > local > val lemma = Q.prove ( > `?i. (i NegInf = Normal 0) /\ > (i PosInf = Normal 0) /\ > (!r. r <> 0 ==> (i (Normal r) = Normal (inv r)))`, > (* proof *) > Q.EXISTS_TAC `\x. if (x = PosInf) \/ (x = NegInf) then Normal 0 > else if x = Normal 0 then ARB > else Normal (inv (real x))` \\ > RW_TAC std_ss [extreal_not_infty, real_normal]); > in > (* |- extreal_inv NegInf = Normal 0 /\ > extreal_inv PosInf = Normal 0 /\ > !r. r <> 0 ==> extreal_inv (Normal r) = Normal (inv r) > *) > val extreal_inv_def = new_specification > ("extreal_inv_def", ["extreal_inv"], lemma); > end; > > local > val lemma = Q.prove ( > `?d. (!r. d (Normal r) PosInf = Normal 0) /\ > (!r. d (Normal r) NegInf = Normal 0) /\ > (!x r. r <> 0 ==> (d x (Normal r) = extreal_mul x (extreal_inv > (Normal r))))`, > (* proof *) > Q.EXISTS_TAC `\x y. > if ((y = PosInf) \/ (y = NegInf)) /\ (?r. x = Normal r) then Normal 0 > else if y = Normal 0 then ARB > else extreal_mul x (extreal_inv y)` \\ > RW_TAC std_ss [extreal_not_infty, real_normal]); > in > (* |- (!r. extreal_div (Normal r) PosInf = Normal 0) /\ > (!r. extreal_div (Normal r) NegInf = Normal 0) /\ > !x r. r <> 0 ==> extreal_div x (Normal r) = x * extreal_inv (Normal r) > *) > val extreal_div_def = new_specification > ("extreal_div_def", ["extreal_div"], lemma); > end; > > In this way, things like `extreal_inv 0` and `extreal_div x 0` are *really* > undefined. > > --Chun > > Il 20/02/19 06:48, > michael.norr...@data61.csiro.au<mailto:michael.norr...@data61.csiro.au> ha > scritto: >> Your right hand side is no better than ARB really. You say that your aim is >> to avoid x/0 = y, with y a literal extreal. But if you believe ARB is a >> literal extreal, then I will define >> >> val pni_def = Define`pni = @x. (x = PosInf) \/ (x = NegInf)`; >> >> and then I can certainly prove that x/0 = pni. If ARB is a literal extreal, >> surely pni is too. >> >> (Recall that ARB's definition is `ARB = @x. T`.) >> >> Michael >> >> >> On 20/2/19, 09:31, "Chun Tian (binghe)" >> <binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>> wrote: >> >> Some further updates: >> >> With my last definition of `extreal_div`, I still have: >> >> |- !x. x / 0 = ARB >> >> and >> >> |- 0 / 0 = ARB >> >> trivially holds (by definition). This is still not satisfied to me. >> >> Now I tried the following new definition which looks more reasonable: >> >> val extreal_div_def = Define >> `extreal_div x y = if y = Normal 0 then >> (@x. (x = PosInf) \/ (x = NegInf)) >> else extreal_mul x (extreal_inv y)`; >> >> literally, it says anything (well, let's ignore zero) divides zero is >> equal to either +Inf or -Inf. But actually the choice of +Inf/-Inf is >> irrelevant, as the sole purpose is to prevent any theorem like ``|- x / >> 0 = y`` being proved, in which y is a literal extreal. For example, if I >> try to prove ``!x. x / 0 = ARB``: >> >> (* with the new definition, ``x / 0 = ARB`` (or any other extreal) can't >> be proved, e.g. >> val test_div = prove ( >> `!x. extreal_div x (Normal 0) = ARB`, >> RW_TAC std_ss [extreal_div_def] >>>> Suff `(\f. f = ARB) (@x. (x = PosInf) ∨ (x = NegInf))` >>> - RW_TAC std_ss [] >>>> MATCH_MP_TAC SELECT_ELIM_THM >>>> RW_TAC std_ss [] (* 3 gubgoals *) >> NegInf = ARB >> >> PosInf = ARB >> >> ∃x. (x = PosInf) ∨ (x = NegInf)); >> *) >> >> at the end I got 3 subgoals like above. I *believe*, no matter what >> value I put instead of ARB, at least one of the subgoals must be false. >> Thus the theorem should be unprovable. (am I right?) >> >> Can I adopt this new definition of `extreal_div` in the future? Any >> objection or suggestion? >> >> --Chun >> >> Il 15/02/19 23:37, Chun Tian (binghe) ha scritto: >>> I'm going to use the following definition for `extreal_div`: >>> >>> (* old definition of `extreal_div`, which allows `0 / 0 = 0` >>> val extreal_div_def = Define >>> `extreal_div x y = extreal_mul x (extreal_inv y)`; >>> >>> new definition of `extreal_div`, excluding the case `0 / 0`: *) >>> val extreal_div_def = Define >>> `extreal_div x y = if (y = Normal 0) then ARB >>> else extreal_mul x (extreal_inv y)`; >>> >>> previously ``|- !x. inv x = 1 / x`` holds, now I have to add `x <> 0` as >>> antecedent, which makes perfectly senses. >>> >>> P.S. the division of extended reals in HOL4 are not used until the >>> statement and proof of Radon-Nikodým theorem, then the conditional >>> probability. >>> >>> --Chun >>> >>> Il 15/02/19 17:39, Mark Adams ha scritto: >>>> I think there is definitely an advantage in keeping ``x/y`` undefined >>>> (even granted that it will always be possible to prove ``?y. x/0 = y``), >>>> namely that it means that your proofs are much more likely to directly >>>> translate to other formalisms of real numbers where '/' is not total. >>>> >>>> Of course there is also a disadvantage, in that it makes proof harder. >>>> But then, arguably, being forced to justify that we are staying within >>>> the "normal" domain of the function is probably a good thing (in a >>>> similar way as being forced to conform to a type system is a good >>>> thing). I understand that, historically, it is this disadvantage of >>>> harder proofs that was the reason for making ``0/0=0`` in HOL. It's >>>> much easier for automated routines if they don't have to consider side >>>> conditions. >>>> >>>> Mark. >>>> >>>>> On 15/02/2019 08:56, Chun Tian (binghe) wrote: >>>>> Thanks to all kindly answers. >>>>> >>>>> Even I wanted ``0 / 0 = 0`` to be excluded from at least >>>>> "extreal_div_def" (in extrealTheory), I found no way to do that. All I >>>>> can do for now is to prevent ``0 / 0`` in all my proofs - whenever it's >>>>> going to happen, I do case analysis instead. >>>>> >>>>> --Chun >>>>> >>>>> Il 14/02/19 18:12, Konrad Slind ha scritto: >>>>>> It's a deliberate choice. See the discussion in Section 1.2 of >>>>>> >>>>>> http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=775DBF504F7EE4EE28CC5169488F4190?doi=10.1.1.56.4692&rep=rep1&type=pdf >>>>>> >>>>>> >>>>>> >>>>>> >>>>>> On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) >>>>>> <binghe.l...@gmail.com<mailto:binghe.l...@gmail.com> >>>>>> <mailto:binghe.l...@gmail.com<mailto:binghe.l...@gmail.com>>> wrote: >>>>>> >>>>>> Hi, >>>>>> >>>>>> in HOL's realTheory, division is defined by multiplication: >>>>>> >>>>>> [real_div] Definition >>>>>> >>>>>> ⊢ ∀x y. x / y = x * y⁻¹ >>>>>> >>>>>> and zero multiplies any other real number equals to zero, which is >>>>>> definitely true: >>>>>> >>>>>> [REAL_MUL_LZERO] Theorem >>>>>> >>>>>> ⊢ ∀x. 0 * x = 0 >>>>>> >>>>>> However, above two theorems together gives ``0 / 0 = 0``, as shown >>>>>> below: >>>>>> >>>>>>> REWRITE_RULE [REAL_MUL_LZERO] (Q.SPECL [`0`, `0`] real_div); >>>>>> val it = ⊢ 0 / 0 = 0: thm >>>>>> >>>>>> How do I understand this result? Is there anything "wrong"? >>>>>> >>>>>> (The same problems happens also in extrealTheory, since the >>>>>> definition >>>>>> of `*` finally reduces to `*` of real numbers) >>>>>> >>>>>> Regards, >>>>>> >>>>>> Chun Tian >>>>>> >>>>>> _______________________________________________ >>>>>> hol-info mailing list >>>>>> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> >>>>>> <mailto:hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net>> >>>>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>>>>> >>>>> >>>>> >>>>> _______________________________________________ >>>>> hol-info mailing list >>>>> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> >>>>> https://lists.sourceforge.net/lists/listinfo/hol-info >>> >> >> >> >> >> _______________________________________________ >> hol-info mailing list >> hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> >> https://lists.sourceforge.net/lists/listinfo/hol-info >> > _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net<mailto:hol-info@lists.sourceforge.net> https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
