Re: [Hol-info] 0 / 0 = 0 ???

, hol-info 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 Mathe

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

Re: [Hol-info] 0 / 0 = 0 ???

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

Re: [Hol-info] 0 / 0 = 0 ???

Dear Professor Chun Tian: I am very interesting the problem. Could you kindly give your kind comments and suggestions on the draft: *viXra:1908.0100 * *submitted on 2019-08-06 20:03:01*, Fundamental of Mathematics; Division by Zero Calculus and a New Axiom ? It

Re: [Hol-info] 0 / 0 = 0 ???

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

Re: [Hol-info] 0 / 0 = 0 ???

Dear all, For what it's worth, a definition of division with 0/0 = 0 won't be possible constructively, because in constructive mathematics all functions of type real->real are continuous, and with this definition division is _not_ continuous. Also, in IEEE 754 floating point of course division

Re: [Hol-info] 0 / 0 = 0 ???

I sympathise with you here, as some mathematicians freak out at any mention of division by zero. It’s not always easy for them to grasp what we are doing with formal logic. You also need to bear in mind that mathematics texts are not proved in any formal system, and in most cases, foundational

Re: [Hol-info] 0 / 0 = 0 ???

Very nice paper. Thanks Umair and Freek for the correction and link. On Wed, 20 Feb 2019 21:08 Umair Siddique > http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.107.1101=rep1=pdf > > http://www.gilith.com/talks/tphols2001-subtypes.pdf > > > - Umair > > On Wed, Feb 20, 2019 at 4:02 PM

Re: [Hol-info] 0 / 0 = 0 ???

> So I think the key is to make sure that “undefined” thing really undefined, such that whenever it appears, the proof cannot proceed any more I think this is exactly what is impossible to do in HOL: it is a logic of total functions. On Wed, 20 Feb 2019 at 15:26, Chun Tian (binghe) wrote: >

Re: [Hol-info] 0 / 0 = 0 ???

Well, as the purpose of optionTheory is to augment any type with one more value, for (at least) extreals, it would be equivalent to have that “undefined” thing defined as part of the datatype definition: val extreal_def = Datatype `extreal = NegInf | PosInf | Normal real | Undefined`;

Re: [Hol-info] 0 / 0 = 0 ???

I'd say one of the stronger ways to get "undefined" is to add an element to your type representing undefinedness, e.g., make it (/) : real option -> real option -> real option, where NONE represents "undefined". But then you will have a lot of bookkeeping to deal with... I don't suggest this

Re: [Hol-info] 0 / 0 = 0 ???

Ha - I stand corrected. Thanks for that. From: Konrad Slind Date: Wednesday, 20 February 2019 at 17:22 To: "Norrish, Michael (Data61, Acton)" Cc: hol-info Subject: Re: [Hol-info] 0 / 0 = 0 ??? Just a minor note: ARB is declared as an uninterpreted constant of type 'a. It used to

Re: [Hol-info] 0 / 0 = 0 ???

Just a minor note: ARB is declared as an uninterpreted constant of type 'a. It used to be defined to be @x.T. Konrad. On Tue, Feb 19, 2019 at 11:49 PM wrote: > 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

Re: [Hol-info] 0 / 0 = 0 ???

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 =

Re: [Hol-info] 0 / 0 = 0 ???

Hi Chun, I run some experiments so to check if it is violating any fundamental rule. So far it went good. On Tue, Feb 19, 2019 at 5:31 PM Chun Tian (binghe) wrote: > Some further updates: > > With my last definition of `extreal_div`, I still have: > > |- !x. x / 0 = ARB > > and > > |- 0 /

Re: [Hol-info] 0 / 0 = 0 ???

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

Re: [Hol-info] 0 / 0 = 0 ???

Note that many/most interesting properties of division still pick up side-conditions involving the non-zero-ness of y. (The attachment is all HOL4's "simple" theorems about division from realTheory, which establishes the basic properties of the reals and their operations.) Michael On

Re: [Hol-info] 0 / 0 = 0 ???

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 =

Re: [Hol-info] 0 / 0 = 0 ???

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

Re: [Hol-info] 0 / 0 = 0 ???

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

Re: [Hol-info] 0 / 0 = 0 ???

You could write HD ([]:’a list) = @x:’a. T or, equivalently, HD [] = ARB. Michael From: "buday.gerg...@uni-eszterhazy.hu" Date: Friday, 15 February 2019 at 15:34 To: hol-info , "Norrish, Michael (Data61, Acton)" Subject: Re: [Hol-info] 0 / 0 = 0 ??? Is HD [] at al

Re: [Hol-info] 0 / 0 = 0 ???

.  (These functions all map into ranges where halfway reasonable defaults seem to exist.  It’s harder to imagine what HD [] should be. )   Michael   From: Thomas Sewell Date: Friday, 15 February 2019 at 04:15 To: "Chun Tian (binghe)" , hol-info Subject: Re: [Hol-info]

Re: [Hol-info] 0 / 0 = 0 ???

Sorry for my previous confusing email, this is something I didn't know about. It seems now TL and TL_T are the same. Jeremy On 02/15/2019 09:59 AM, michael.norr...@data61.csiro.au wrote: > the updated definition of TL. ___ hol-info mailing list

Re: [Hol-info] 0 / 0 = 0 ???

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=rep1=pdf On Thu, Feb 14, 2019 at 10:40 AM Chun Tian (binghe) wrote: > Hi, > > in HOL's realTheory, division is defined

[Hol-info] 0 / 0 = 0 ???

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