df-met update

[Mario Carneiro]

Hi All,

I wrote a bit about this update on a previous thread, but now that it is complete I'll repeat it and add a few new developments since then. Sorry it took so long, I know there are some merges which were delayed because of my incomplete work which I'll catch up on now. Stefan's branch has been merged up to a6e567 'two new rings' (which had a few incomplete proofs - I hope you don't mind that I finished them for you!), and I will merge Drahflow's contribution as soon as I hear what name he would prefer for his work. (For my part, I would suggest using one's real name, since that seems to be the convention and also lends a bit more appearance of authority in academic circles, but the choice is his.)

The list below is expanded from the original with new items; the originals are numbered 1,2,3... and the new items are lettered a,b,c....

a. Added utility theorems rbaib and ralab2 (the ralab2 sequence is useful when the abstraction is more complicated than the quantified formula)

b. hbsbc1 and hbcsb1 now use a DV condition instead of a bound variable hypothesis for $d x A since this is more useful 99% of the time. The originals are at hbsbc1f etc.

c. df-mpt has been moved to just after df-opab, and all theorems that used df-opab or df-oprab for creating functions have been converted to use df-mpt / df-mpt2. This affected many old mathboxes with theorems written before df-mpt was created. As a result, there are now a number of new convenience theorems for df-mpt, such as fvmpt3i, fnmpti, ralrnmpt, elrnmpt1s. Users are encouraged to check out the new offerings.

d. Utility theorems op1std, op2ndd are often useful as a replacement to op1st etc.

e. As suggested by Stefan, a new syntax construction "tpos F" swaps the left and right arguments of a two-argument function. Because of its similarities to the converse operation and validity on proper classes, I thought it better to support as a syntax construction rather than a function "( tpos ` F )". See df-tpos for the available theorems. So far this construction has been used for oppG, oppR, and FL's dual category theorem (dualcat2).

f. rdgsucmpt2 may provide shorter derivation trees than rdgsucmptf; see if it is useful in your application.

1. df-er is now a two-parameter syntax construction, and includes the relation assumption. (I always found it odd that textbooks claim that an equivalence relation is reflexive, symmetric and transitive, but our iser only requires symmetric and transitive. Adding the domain fixes this.)

g. Yet another choice principle has been added: "X e. AC_ A" (df-acn) means that for all families of nonempty subsets of X indexed by A, there is a choice function for the family. This is read "X has choice sequences of length A", and it is a cardinal invariant in both X and A which passes from larger sets to smaller. Every set has finite choice sequences (finacn), and a well-orderable set has choice sequences of any length (numacn), while ax-cc is equivalent to "AC_ om = _V" (acncc). The purpose of this construction is to access "parameterized" versions of AC - each statement "X e. AC_ A" can be viewed as a weak version of choice - and some statements depend in nontrivial ways on both arguments, such as fodomacn. This also allows for unifying the proofs of iundom (which uses ax-ac) and iunctb (which uses ax-cc) into iundomg, which has explicit choice principles via df-acn.

h. ltne has lost its second unnecessary hypothesis "B e. RR", and ltneii has been augmented with gtneii which commutes the disequality (as discussed before on this list).

2. df-adde and df-nege were taken from FL's mathbox and built on extensively, under the new names df-xadd, df-xneg, df-xmul. These are operations for addition, multiplication, negation of extended reals, and most of the important algebraic theorems are there (x+-x=0, x+y=y+x, x+(y+z)=(x+y)+z, x <_ y -> x+z <_ y+z, x*(y+z)=x*y+x*z, x*y=y*x, etc.), with the usual caveats. In order to have unconditional closure and avoid a bunch of unnecessary hypotheses, I defined +oo + -oo = 0 * +oo = 0. For example, associativity of addition is true assuming all numbers are in ( RR* \ {-oo} ) (and there is a separate theorem for ( RR* \ {+oo} )).

i. df-fzo (half-open integer sequences), from Stefan's mathbox, has been imported. This can probably be used in many places but I haven't done much with it yet.

j. sqr2irr is an important proof, being mentioned in Freek Wiedijk's famous paper "The Seventeen Provers of the World". Nevertheless, the current proof shows its age with respect to the surrounding material, and I did my best to rewrite it into "modern" form for about half the length, while still maintaining the lack of any "advanced tricks" from the original proof - the most advanced lemma is nnesqi, which is now called nnesq in theorem form.

3. Struct and Slot definitions. Struct is mainly useful as a lemma for strfv; the statement "S Struct <. M , N >." means that S\{(/)} is a function on a subset of (M...N) - it functions as a "loop invariant" when recursing over a union of ordered pairs defining a structure (arranged in increasing order by slot), and allows for the structure proof in O(n) and slot extraction in O(log n) per slot, for a total of O(n log n) over all theorems for the structure, which I think is asymptotically optimal. Slot just gives a name to the "(x e. _V |-> (x`2))" construction used for slots like +g.

4. All the slots (including those in mathboxes) are now collected in the "Slot definitions" section, and in the future any new slots will be moved here immediately. This makes it easier for an author to make sure that they are not conflicting with someone else's slot. (Specifically: slots 4, 8 and 13 are now taken by Norm's df-starv and df-ipr, and FL's df-unif.) Aside from the definition, any slot that gets use will have ndxarg and ndxid specializations.

5. As promised, TopOpen has been split into two functions: TopSet is the slot, and (TopOpen`W) = ((TopSet`W) |`t (Base`W)) is the truncated topology so that it plays well with |`s. Generally, one will want to avoid TopSet in favor of TopOpen, and any derived structures should reference TopOpen.

6. Since the derivation order switch of Xm_ (df-prdm) and Xs_ (df-prds) made Xs_ almost useless as a special case of Xm_, and no theorems were ever built on it, Xs_ has been deleted. However I like the name Xs_ better, so Xm_ was renamed to Xs_ and similarly for the theorem labels *prdm* -> *prds*.

7. The extended real operations have been put into a new "canonical structure" RR*s (df-xrs) which also includes an extended metric in the metric slot and the order topology induced by <.

8. df-xps has been developed, meaning a bunch of utility theorems for the function `' ( { x } +c { y } ), which is a nice compact way of writing the function on 2o that sends (/) to x and 1o to y. Since df-xps is defined in terms of existing constructions (df-imas and df-prds) that have already been developed, this means that we immediately get theorems for the product of two groups, rings, modules, etc. The fact that the topology is df-tx is non-trivial, though.

9. In order to make TopGrp restriction-friendly, a new df-plusf function has been introduced, which is the "functionalization" of df-plusg, and TopGrp asserts that this function is continuous. To functionalize the ring multiplication you can use mulGrp and +f, but for scalar multiplication we will need a new definition.

k. Stefan's "Word" definition (adapted from FL's "Kleene") has been imported. There are many uses for strings in mathematics, and this is one section which I hope gets enough utility theorems to be painless to use. I put it after monoids because I plan to build FreeMnd and FreeGrp on top of it.

l. The symmetric group is now a topological group, under the product topology. I plan to make this a subgroup of the topological monoid of endofunctions on a set (in fact it is the unit group of the monoid, although our current "multiplicative" definition of unit group is designed for rings, not monoids).

m. As suggested/implemented by Stefan, df-od has been edited to take value 0 instead of +oo at "infinite order" elements. Although this goes against the usual terminology in group theory, it is more natural for the divisibility characterization of order (oddvds) and also matches the usual definition of characteristic of a ring as the group order of the identity. Some theorems such as mndodcong discuss the behavior of the order function on monoids, which is not as pleasant as in groups. In a monoid, the sequence of powers of an element will usually be an initial segment followed by a loop, such as 0,1,2,3,2,3,2,3,... and I wonder whether we should take the order of such an element to be the length of the loop, i.e. 2 in this case, rather than infinite (since 0 never appears again in the sequence).

n. As suggested by Gerard, the "Z2Ring" (ZZ to ring) ring homomorphism has been renamed to "ZRHom" (ZZ ring homomorphism) which is hopefully less confusing. This is the function that maps n e. NN to 1r+1r+...+1r (n times), with the obvious extension to ZZ. Stefan's df-chr has also been imported to describe the behavior of this function in connection with the ring characteristic (a straight port of analogous results for group order).

10. Metric spaces now have an explicit base set "D e. ( Met ` X )" instead of the dom dom thing, similar to the Fil change. Furthermore, the addition of extended real addition and the proof of the product metric have necessitated the development of extended metrics. Since almost all theorems from metrics generalize to extended metrics with little change, most of the metric theorems now refer to *Met instead of Met. Similarly, df-ball and df-mopn (renamed from df-opn, since 'opn' is usually used to refer to open sets in a topology and using them for the metric topology as well is confusing) now allow extended metrics. The radius of a ball is allows to be any extended real, which in particular means that -. (/) e. ran ( ball ` D ) is no longer true. This does not affect the generated topologies, though, so I think it is harmless.

11. Although Top has not been converted to use a base set the same way as Met, I am doing a "soft introduction" by introducing df-topon and using it in most of the later topology theorems, in particular for filters and continuity. Derived topological spaces (like Haus) have not been changed to add a base set; you will have to write ( J e. Haus /\ J e. ( TopOn ` X ) ) if you want to use a specific base set. But the old method of just using $e |- X = U. J is not deprecated, and both approaches are in use. Also the Cn and CnP predicates have had some unutilized reverse closure properties; a lot of hypotheses were eliminated by taking advantage of these.

o. The order topology is now supported, including in particular the topology of the extended reals. It accepts a TosetRel or more general relation (note that weak inequality is used), and produces a topology generated by the closed rays (-oo, a], [a,+oo), (+oo,-oo) as a closed subbasis. Not too much work has been done on non-TosetRel relations, but note that this definition makes sense for lattices, where the definition produces the so-called "interval topology".

12. Separation axioms have been developed - I imported df-t0, df-reg, df-nrm from JGH's mathbox and added CNrm, PNrm for completely normal and perfectly normal, with enough theorems to fill out the chart https://en.wikipedia.org/wiki/Separation_axioms#Relationships_between_the_axioms . I also added the Kolmogorov quotient so that even the "non-T0" versions are accessible; the only separation axioms missing at this point are Urysohn, completely Hausdorff, and Tychonoff (which require continuous functions into RR and so are not appropriate to go in the section with df-haus).

13. The ultrafilter lemma is now a definition, localized by base set (X e. UFL iff every filter on X extends to an ultrafilter). I made a new proof of the Alexander subbase theorem using UFL instead of Zorn's lemma (the original alexsub is kept as *ALT), and finally used it to prove Tychonoff's theorem, with an explicit choice hypothesis (you have to assume U. (Xt_`F) e. (UFL i^i dom card) ), so that I could add the other half of dfac21i without using choice.

14. JGH's filter cluster theorems have been imported (they were already well-developed enough as it is and it is easier to maintain them from main).

p. Topological monoids and topological groups have been developed. I separated the definitions of TopMnd and TopGrp to allow for easy access of paratopological groups and other similar notions. Interesting theorems include: the group sum operation is continuous into a function space (tmdgsum), for any neighborhood nA e. U there is a neighborhood A e. V such that any sum of n elements in V is in U (tmdgsum2), any group with the discrete or indiscrete topology is a TopGrp (distgp, indistgp), an open subgroup is closed (opnsubg), the closure of a (normal) subgroup is a (normal) subgroup (clssubg, clsnsg), the connected component of the identity is a normal subgroup (tgpconcomp), a TopGrp is T0/T1/Hausdorff iff {0} is closed (tgphaus, tgpt1, tgpt0).

q. The topological group sum operation has been developed. The most basic theorems require that G is a (CMnd i^i TopSp) and F : A --> (Base`G) for some (possibly infinite) index set A, in which case (G tsums F) is the set of convergent points of the group sum. Any finite group sum converges to its usual value (tsmsid), and in fact it converges to the closure of {(G gsum F)} in this case (tsmsgsum). In topological groups this is also true generally - a convergent sum always converges to a coset of (cls`{0}) (tgptsmscls). Topological sums distribute nicely over submonoids (tsmssubm), trivial restrictions (tsmsres), bijections (tsmsf1o), continuous monoid homomorphisms (tsmsmhm), group addition (tsmsadd), and partitions (tsmssplit). Unfortunately the equivalent of gsumxp is only true under certain conditions, but we can say that in a topological group, if sum_k F(j,k) ~~> H(j) for each j, and (sum F) ~~> a, then (sum H) ~~> a as well (tsmsxp).

r. A number of new results relate the topology and metric of RR* to that of RR and CC. The complex numbers are a MetSp and a TopSp, and (TopOpen`CCfld) is a topology on CC. This is now used in preference to the old ( MetOpen ` ( abs o. - ) ) as an idiom for "the topology of CC". A neighborhood of +oo contains (a,+oo] for some a e. RR (pnfnei), the restriction of the RR* topology to RR yields the usual topology (xrtgioo), the topology is homeomorphic to II (xrhmph), ~~>r limits correspond to continuity at +oo (xrlimcnp), sums on [0,+oo] always converge uniquely (xrge0tsms). RR* has an extended metric (xrsxmet) which extends the usual metric on RR (xrsdsre) and generates a finer topology than the usual one on RR* (xrsmopn). You would think that this topology is not very useful, but it turns out to be the natural one for dealing with extended metrics as continuous functions (xmetdcn2).

s. df-fne and df-locfin in Jeff Hankins' mathbox underwent some simple proof-shortening/modification, and neibastop1/2/3 was considerably shortened (I wasn't planning on it, but I had to do some simple modifications and the original was nearly unreadable), as well as the topology lattice theorems (topmeet, topjoin, fnemeet1, etc.).

t. The Bnd and TotBnd predicates have also been changed to (Bnd`X) and (TotBnd`X), and the section was developed some more, with new material on boundedness of a product metric and a new derivation of total boundedness of balls in Rn via total boundedness in the supremum metric. df-rrn was also changed to use a finite index set instead of a (1...N) index set.

Believe it or not, these are just the highlights of this big update, and because I don't want to bore you I have just touched on the more mathematically interesting bits. For the full story there is no better source than the diff of commit a54a88c over b52eacd, and of course I can talk in greater detail on any of the points above. Unfortunately, as is usual with this sort of bleeding-edge work you won't see the material up on the site until the next "official release", but you can always download the latest off of github (https://github.com/metamath/set.mm/commit/a54a88c) and generate your own HTML.

Mario Carneiro

[David A. Wheeler]

Overall it looks nice.

However, +oo + -oo = 0 seems arbitrary, can't that be avoided?

--- David A.Wheeler

[Mario Carneiro]

To be sure, it is arbitrary. Well, not that arbitrary: the only choice that makes xaddcom and xnegdi true unconditionally is +oo + -oo = -oo + +oo = 0. But this situation bears a strong resemblance to the 1/0 = ? problem, which was recently discussed on FOM. I'll quote from (a quote from) John Harrison:

> To: q...@mcs.anl.gov
> Subject: Re: Undefined terms
> In-reply-to: Your message of "Thu, 18 May 1995 12:39:59 MDT." <1995051818...@antares.mcs.anl.gov>
> Date: Fri, 19 May 1995 10:54:02 +0100
> From: John Harrison <John.Harrison@cl.cam.ac.uk>
> Message-ID: <"swan.cl.cam.:266770:950519095422"@cl.cam.ac.uk>


This is a very important topic. I can think of at least four main approaches to
the problem of undefined terms.

[1] Resolutely give each partial function a convenient value on points
    outside its domain. For example, set:

      |- inverse(0) = 0

    This has the advantage that you can state many theorems more elegantly:

     |- inverse(inverse(x)) = x
     |- 0 < x <=> 0 < inverse(x)
     |- inverse(-x) = -inverse(x)
     |- inverse(x * y) = inverse(x) * inverse(y)

    But it also gives you strange "accidental" theorems like

     |- inverse(0) = 0

    itself.

[2] Give each partial function some arbitrary value outside its domain. This
    gives fewer convenient theorems, but also fewer accidental ones.
    Nevertheless you still get some, e.g. assuming we define

     |- x / y = x * inverse(y)

    then we have

     |- 0 / 0 = 0 * something = 0

[3] Encode the domain of the partial function in its type and make its
    application to arguments outside that domain a type error. This works well
    in situations where definedness is implicit, like differential equations
    where

      |- d f(x) / dx = H[f,x]

    includes (I think) an implicit assertion that f is differentiable iff
    H[f,x] is defined. On the other hand in complicated situations in
    analysis, one could imagine the types becoming staggeringly complicated,
    and this approach disallows routine manipulations like:

     |- inverse(-x) = -inverse(x)
     |- inverse(x * y) = inverse(x) * inverse(y)

    without incurring additional typechecking obligations (which might be
    nontrivial if x is complicated).

[4] Have a true logic of partial terms. This is the most flexible, since one
    can define multiple notions of equality; e.g. "both sides are defined and
    equal" or "if one side is defined so is the other and they are equal".
    The downside is that the logic becomes more complicated. I don't know how
    troublesome this is in practice. Anyway, I think there's a strong argument
    that this is how mathematicians normally think informally.

As far as I know, HOL takes approaches [1] and [2] according to the whim of the
user, Nuprl and PVS normally take approach [3], while IMPS takes approach [4].
Old LCF has (used to have?) something analogous to approach [4], and Lambda did
too, though I think it was abandoned in the face of user pressure for a simpler
logic. I'm not sure about other systems. For generic provers like Isabelle, I
suppose you have a free choice.

There's a good discussion of these issues in Farmer's paper "A Partial
Functions Version of Church's Simple Theory of Types" (JSL vol. 55, 1990; pp.
1269-1291). There's also an interesting-looking paper by Feferman on this topic
which I've just received a copy of (it's at home now so I can't give a
reference).

John.

Now we have discussed what is essentially the difference between 1 and 3 here. Since we are based on ZFC, it is impossible to take option 3 in all aspects, for example we know ( A + B ) is unconditionally a set with no assumptions on A,B and no axioms to this effect. In the +oo + -oo question, the main alternative in the spirit of df-div is to make +e a function with a non-rectangular domain, specifically ( ( RR* X. RR* ) \ { <. +oo , -oo >. , <. -oo , +oo >. } ). Let me dissuade you from this course of action. The number one most important theorem I am interested in having without extra restrictions is xaddcl, which would be turned in to the hideous

|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A =/= +oo \/ B =/= -oo ) /\ ( A =/= -oo \/ B =/= +oo ) ) -> ( A +e B ) e. RR* )

if this were to be done. My goal with the new xadd* theorems is to make the new theorems as close as possible to the addition theorems, with even the names and hypothesis order borrowed directly from the originals. For this to work I want +e to inherit *as many theorems as possible* from the RR context, straight into the square domain ( RR* X. RR* ), which entails giving those points the nicest possible values. As far as I see it, there are already a number of concessions which need to be made to keep the theorems true in RR*, and doing this would only make it worse.

But then again, I am personally in favor of 1/0 = 0 as well, so perhaps someone else can cast a vote on the matter?

Mario

[Norman Megill]

On 9/28/15 3:03 PM, Mario Carneiro wrote:
> To be sure, it is arbitrary. Well, not that arbitrary: the only choice
> that makes xaddcom and xnegdi true unconditionally is +oo + -oo = -oo +
> +oo = 0. But this situation bears a strong resemblance to the 1/0 = ?
> problem, which was recently discussed on FOM. I'll quote from (a quote
> from) John Harrison:
>

> > To: q...@mcs.anl.gov <mailto:q...@mcs.anl.gov>

> > Subject: Re: Undefined terms
> > In-reply-to: Your message of "Thu, 18 May 1995 12:39:59 MDT."
> <1995051818...@antares.mcs.anl.gov

> <mailto:1995051818...@antares.mcs.anl.gov>>

> > Date: Fri, 19 May 1995 10:54:02 +0100

> > From: John Harrison <John.H...@cl.cam.ac.uk
> <mailto:John.H...@cl.cam.ac.uk>>

> > Message-ID: <"swan.cl.cam.:266770:950519095422"@cl.cam.ac.uk

> <http://cl.cam.ac.uk>>

This can be shortened slightly:

|- ( ( A e. RR* /\ B e. RR* /\ { A , B } =/= { -oo , +oo } )

-> ( A +e B ) e. RR* )

or more obscurely

|- ( <. A , B >. e. dom +e -> ( A +e B ) e. RR* )

>
> if this were to be done. My goal with the new xadd* theorems is to make
> the new theorems as close as possible to the addition theorems, with
> even the names and hypothesis order borrowed directly from the
> originals. For this to work I want +e to inherit *as many theorems as
> possible* from the RR context, straight into the square domain ( RR* X.
> RR* ), which entails giving those points the nicest possible values. As
> far as I see it, there are already a number of concessions which need to
> be made to keep the theorems true in RR*, and doing this would only make
> it worse.

My personal feeling is that +oo + -oo = 0 is distasteful, although I
won't reject it out of hand (I don't anticipate using it myself).

Most analysis books define only ordering relations with +-oo, which of
course are highly useful when dealing with sup, limsup, and intervals.
I've occasionally seen operations with +-oo defined, I think with
+oo + -oo left undefined, although I don't recall their application.
What do you plan to use these operations for? If you know of a book
that defines +oo - -oo = 0 I would be more comfortable with it.

One question is whether +oo + -oo = 0 makes a significant difference
in the big picture. While it may simplify trivial theorems, many of the
more advanced ones may require hypotheses avoiding this condition anyway
for the theorems to hold.

>
> But then again, I am personally in favor of 1/0 = 0 as well, so perhaps
> someone else can cast a vote on the matter?

Personally I find 1/0 = 0 a distasteful hack. It goes against standard
math texts and what people are taught in school ("never divide by 0").
It is arbitrary and possibly misleading to someone learning math.

In HOL Lite it allows shorter statements of some theorems by not having
to specify =/=0 conditions. Maybe it makes the proof engine more
efficient, not sure. But I would guess that for the bulk of theorems
beyond trivial ones we would still have to specify =/=0 for the theorem
to hold, and I'm not convinced that the savings are that significant in
the big picture. In any case I think =/=0 provides useful information
to the casual reader since that's how it would appear (explicitly or
implicitly) in standard texts.

You and I have had discussions in the past about using definitional
artifacts, particularly out-of-domain df-fv. I am ok with it in early
set theory since people are "expected" to learn the df-fv details as an
integral part of the development, and it makes a lot of proofs shorter.
But people reading more advanced material at a relatively high level may
want to assume a "generic" set theory underneath. Having to drill down
to the details of nonstandard out-of-domain behavior can be an
unnecessary distraction.

In general, whether we should exploit a definitional artifact to achieve
a shorter theorem statement is a subjective matter, but I like to keep
the reader in mind, in the context of the material at hand.

BTW I have no problem exploiting proper class artifacts everywhere to
eliminate sethood hypotheses, since class variables ordinarily represent
sets outside of early set theory. The fact that some theorems also hold
when the variables are proper classes shouldn't cause confusion.

From the same thread as above
http://mizar.org/qed/mail-archive/volume-3/0031.html
while Mizar leaves 1/0 undefined, I was surprised that it still has
strange divide-by-0 behavior:

One can justify that 0 * (0/0) = 0 by reference to the theorem REAL_1:23:
x*y=0 iff (x=0 or y=0)
i.e. Mizar accepts
0 * (0/0) = 0 by REAL_1:23;
as a correct inference.

Apparently x*y is a number if only one of the arguments is a number. This
is a little weird and certainly nonstandard. I think set.mm's mul0or is
closer to normal arithmetic.

Norm

[Mario Carneiro]

On Mon, Sep 28, 2015 at 11:59 PM, Norman Megill <n...@alum.mit.edu> wrote:

This can be shortened slightly:

|- ( ( A e. RR* /\ B e. RR* /\ { A , B } =/= { -oo , +oo } )
       -> ( A +e B ) e. RR* )

or more obscurely

|- ( <. A , B >. e. dom +e -> ( A +e B ) e. RR* )

The problem isn't so much the length of the theorem statement itself as the extra steps needed to discharge the assumptions. set.mm is not currently very well set up to handle =/= +-oo proofs, so it takes more time than I'd like. In this case I would probably take the second option if it comes to that, analogous to atandm.

 

Most analysis books define only ordering relations with +-oo, which of
course are highly useful when dealing with sup, limsup, and intervals.
I've occasionally seen operations with +-oo defined, I think with
+oo + -oo left undefined, although I don't recall their application.
What do you plan to use these operations for?  If you know of a book
that defines +oo - -oo = 0 I would be more comfortable with it.

I think the main reason most sources leave this undefined is that + has a unique continuous extension to RR* everywhere *except* +oo + -oo, and we like our functions to be continuous. I find it useful to have a *value* even when *continuity* is not guaranteed - the most famous example of this in the literature is 0^0 = 1 (speaking here of complex exponentiation ^c ). Many fight against this because the function does not have a limit here, but there is a clear gain by having a particular value. The question of 0^x = ? required half an hour of playing with Mathematica before I realized that a^x -> 0 as a -> 0 iff Re[a] > 0, so that setting it to zero will not make it continuous there, but then I realized that it will never come up in a "real" application, so it is best just to set it to something simple. Put another way: there is way too much stuff going on in the ^c function that most people won't care about, so it is easiest to use if the hypotheses are also as simple as possible. I think that adding these side hypotheses makes it more confusing, not less.

As for where the extended real operations are used, I think the new material somewhat speaks for itself - much of it was not possible without a +e function. Specifically: the +e , *e functions are inserted into a new "canonical structure" RR*s, upon which infinite sums are possible using tsums. These will probably see use soon in measure theory, and they are already in use in extended metric theorems, where the triangle inequality is ( ( x D y ) +e ( y D z ) ) <_ ( x D z ). I believe +oo - +oo is even used in a technical condition in xblss2, as well as many of the extended real theorems themselves, such as xsubge0. Of course, in many cases +oo + -oo will not come up (and whenever we restrict to [0,+oo] we know it won't), but having to avoid it entirely causes many more problems than it solves.

 

One question is whether +oo + -oo = 0 makes a significant difference
in the big picture.  While it may simplify trivial theorems, many of the
more advanced ones may require hypotheses avoiding this condition anyway
for the theorems to hold.

Consider integrating a function which is undefined on a set of measure zero. This is, believe it or not, a really common thing (think meromorphic function), and it is much more troublesome to carry all those undefined points around than simply integrate over them since the value "obviously" doesn't matter. I have yet to come up with a satisfactory approach to this under the partial functions approach, but with stuff like 1/0 = 0 (or even option 2: 1/0 e. RR) this is trivial.

From the same thread as above
http://mizar.org/qed/mail-archive/volume-3/0031.html
while Mizar leaves 1/0 undefined, I was surprised that it still has
strange divide-by-0 behavior:

  One can justify that 0 * (0/0) = 0 by reference to the theorem REAL_1:23:
  x*y=0 iff (x=0 or y=0)
  i.e. Mizar accepts
  0 * (0/0) = 0 by REAL_1:23;
  as a correct inference.

Apparently x*y is a number if only one of the arguments is a number.  This
is a little weird and certainly nonstandard.  I think set.mm's mul0or is
closer to normal arithmetic.

I think in their case it is a number by typing considerations. The equivalent of this for us is:

( (1/0) u. (1/0) ) = (1/0)

even if nothing whatsoever is known about (1/0): this is true simply *by the form of the expression*, since any valid class expression denotes a class and thus satisfies any identity of classes.

Mario

[David A. Wheeler]

> But then again, I am personally in favor of 1/0 = 0 as well...

I think that is a terrible approach. If 1/0 =0, then a reasonable corollary is that 0*0=1. There is a reason division by 0 is considered undefined, after all.

I appreciate that hacks like this make it easier to create proofs. But the world already has a much simpler way to create informal proofs... namely, informal proofs as shown in math textbooks.

To me, one of the compelling advantages of metamath is that it can show the exact preconditions, and that only legal steps are allowed. Allowing 1/0 =0 means that the proofs involving division do not really mean what most readers will think they mean. I think the same is true for +oo + -oo = 0 (though not as strongly).

I realize that there is a strict formalist camp that says that symbols mean whenever we want them to mean. But I think relatively few people are interested in a system where division does not mean the normal meaning of division. If there is a symbol for division, then it should not allow division by zero, because direct division by zero is not allowed in normal mathematics. Similarly, it should be very careful with infinities... lots of things don't work the same way with Infinity.

I think it is fine to do this sort of thing temporarily, as a simplified model of mathematics just to get things going. But I think that should not be done permanently.


--- David A.Wheeler

[Mario Carneiro]

On Tue, Sep 29, 2015 at 7:48 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

> But then again, I am personally in favor of 1/0 = 0 as well...

I think that is a terrible approach. If 1/0 =0, then a reasonable corollary is that 0*0=1. There is a reason division by 0 is considered undefined, after all.

That is most certainly *not* a reasonable corollary. The fundamental property of division is y =/= 0 -> y*(x/y) = x, not y*(x/y) = x with no guards. Obviously we are not considering any theorems that lead to contradiction - but in no way does this affect the question of what value to assign x/0. Not all theorems are true for the entire range of the operation. The theorem x,y e. NN0 -> (x - y) e. NN0 is not true without the additional guard y <_ x. The theorem sqr(x*y) = sqr(x)*sqr(y) is not true for all complex x,y, even though both sides are well-formed and valid complex expressions (and the guards are rather complicated in this case). Just because an equation is true in a subset of the domain *does not* mean it is true for the whole domain. Complex analysis considers some conditions in which we can make just such a claim, but not all our functions are analytic, and limiting the domain to the areas where they are analytic causes bigger problems when needed boundary points are missing.

Keep in mind that this decision also interacts with the (/) e. CC problem to make it so that any undefined values propagate forward, and so these problems do not go away as you go to more advanced work, they just get worse.

 

I appreciate that hacks like this make it easier to create proofs. But the world already has a much simpler way to create informal proofs... namely, informal proofs as shown in math textbooks.

Informal mathematics solves this issue by ignoring it. That's obviously not an option for us.

 

To me, one of the compelling advantages of metamath is that it can show the exact preconditions, and that only legal steps are allowed. Allowing 1/0 =0 means that the proofs involving division do not really mean what most readers will think they mean. I think the same is true for +oo + -oo = 0 (though not as strongly).

I disagree. Consider the following experiment, which I have half a mind to enact: define "totalized division" as

/t = ( x e. CC , y e. CC |-> if ( y = 0 , 0 , ( x / y ) ) )

Then /t is clearly a total function, and it is the same thing as / away from zero. The important fact is that this definition satisfies a "conservativity" property - if you make a proof using /t to produce a theorem which does not need the value of /t at zero, you can substitute it away to get a statement about / which is also valid, without even having to revisit the original proof. For example, if there is a proof of

( ( A e. CC /\ B e. CC /\ A =/= 0 ) -> ( A /t ( A /t B ) ) = B )

then using the fact B =/= 0 -> ( A /t B ) = ( A / B ), I can prove

( ( ( A e. CC /\ A =/= 0 ) /\ ( B e. CC /\ B =/= 0 ) ) -> ( A / ( A / B ) ) = B )

with only a few steps. Since /t is just a definition, it is conservative, so this shows the validity of the latter theorem even if /t did not exist.

The point is that /t is an *extension* of regular division, so everything that is true about / is also true about /t, in particular all the field axioms. You won't be able to derive a contradiction by knowing the value of /t at zero because making such an assignment is consistent.

I realize that there is a strict formalist camp that says that symbols mean whenever we want them to mean. But I think relatively few people are interested in a system where division does not mean the normal meaning of division. If there is a symbol for division, then it should not allow division by zero, because direct division by zero is not allowed in normal mathematics. Similarly, it should be very careful with infinities... lots of things don't work the same way with Infinity.

 

Finally, since Norm has expressed an interest in literature to back me up, I will point to some work on 'meadows', unearthed during the recent FOM discussion, which are basically fields with a totalized division operator setting x/0=0. Inverse is an atomic operation here, axiomatized by (x^-1)^-1 = x*x*(x^-1) = x (from which necessarily 0^-1 = 0).

Mario

---------- Forwarded message ----------
From: John Tucker <j.v.t...@swansea.ac.uk>
Date: Thu, Sep 24, 2015 at 12:24 PM
Subject: [FOM] On 0^{-1}=0
To: f...@cs.nyu.edu

I’d like to follow up various posts on 0^{-1}=0.

If you want to avoid the partial nature of division for some reason then there are many options. In this post I’ll speak of one that has been mentioned already: meadows.

1. In computer science the algebraic theory of data types provides a beautiful general theory of data based on many-sorted algebras and axioms that are, or are close to, equations.  The theory started as formal theory of specification. Here is one basic problem:  suppose data and its operations and tests are modelled as a many sorted algebra A with signature S, then find equations E, possibly expanding S using extra operators S’, such that a S-reduct of the initial algebra I(S’, E) is isomorphic to A.

2. The theory’s beauty is diminished somewhat if operations are partial, as was observed in the 1970s when attempts to axiomatise the stack met the operation of popping the empty stack. If only the pop operation could be total. See for example:

Bergstra and Tucker, The data type variety of stack algebras 

Annals of Pure and Applied Logic 73 (1995) 11-36

http://www.sciencedirect.com/science/article/pii/0168007294000385

3. Given the theoretical importance of the rational numbers in computation — being the data type of finite representations of reals and physical measurements relative to a system of units — the problem of finding an equational specification of the rational numbers is interesting and challenging.  A successful attack on the problem was made in:

Bergstra and Tucker, The rational numbers as an abstract data type

Journal ACM 54 (19) Article 7 25 pages

DOI = 10.1145/1219092.1219095 

In order to make an equational specification of the rationals,  the question of totalising division was addressed and idea of a ‘generalisation’ of the concept of field to a meadow arose.

4. Meadows are a class of structures, with total operations of +, x , - and ^{-1}, that is equationally definable. The equations imply that 0^{-1}=0. Later, in the study

Bergstra, Hirshfeld and Tucker, Meadows and the equational specification of division

Theoretical Computer Science 410 (2009) 1261-1271

http://www.sciencedirect.com/science/article/pii/S0304397508008967

There were a number of theorems that demonstrated the concept had an interesting theory and quite some potential for further developments. For example, 

Theorem: Up to isomorphism, non-trivial meadows are precisely the subalgefbras of products of zero-totalised fields.

Theorem: The equational theory of meadows and the equational theory of fields with zero-totalised division are identical.

5. Subsequently, Jan Bergstra and his colleagues at Amsterdam have developed a good deal of the algebraic theory of meadows and some applications. A convenient source of references is his page on the CS Bibliography:

http://dblp.uni-trier.de/pers/hd/b/Bergstra:Jan_A=.html

A particularly interesting application is:

Meadow based fraction theory

http://arxiv.org/abs/1508.01334

There is much to say on the topic, most of which can be found in these papers. Total division makes sense algebraically and logically.

6. Given their algebraic theory is solid, are there precedents in the vast literature of abstract algebra? Meadows are close to the well-known von Neumann regular rings, expanded with a pseudo-inverse. However, the idea of 0^{-1}=0 is used in the idea of desirable pseudo fields: 

Komori, Free algebras over all fields and pseudofileds, 

Reports of the  Faculty of Science, Shizuoka University 10 (1975), 9-15

http://ir.lib.shizuoka.ac.jp/bitstream/10297/8858/1/10-0009.pdf

Ono, Equational theories and universal theories of fields

Journal of the Mathematical Society of Japan 356 (1983) 289-306

https://projecteuclid.org/download/pdf_1/euclid.jmsj/1230396550

7. As to other methods, there is the notion of wheel proposed by my colleague Anton Setzer in:

Setzer,Wheels, 1997. 

http://www.cs.swan.ac.uk/~csetzer/articles/wheel.pdf

The topic was developed in:

J Carlstrom, Wheels - on division by zero

Mathematical Structures in Computer Science 14 (2004) 143-184

http://journals.cambridge.org/action/displayFulltext?type=1&fid=198510&jid=MSC&volumeId=14&issueId=01&aid=198509

where wheels are equationally defined.

Formalisations like 0^{-1}=0 can reveal the power of taking syntax seriously. This is something that computer science has long understood and institutionalised in its culture, theory and practice, but mathematics remains reluctant to acknowledge outside logic.

John 

_______________________________________________
FOM mailing list
F...@cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

[David A. Wheeler]

On Tue, 29 Sep 2015 21:04:20 -0400, Mario Carneiro <di....@gmail.com> wrote:
> That is most certainly *not* a reasonable corollary. The fundamental
> property of division is y =/= 0 -> y*(x/y) = x, not y*(x/y) = x with no

> guards. Obviously we are not considering any theorems that lead to contradiction...

Yes.

> but in no way does this affect the question of what value to assign x/0...

I think that set.mm should include models of mathematical operations that
have definitions consistent with how they are normally used by mathematicians.
With rare exceptions, x/0 is considered "undefined", and NOT 0 or any other value in CC.

> Keep in mind that this decision also interacts with the (/) e. CC problem
> to make it so that any undefined values propagate forward, and so these
> problems do not go away as you go to more advanced work, they just get worse.

Agreed.

For the record, I think it should be *provable* that ( 1 / 0 ) e/ CC ... something
I suspect we will *not* agree on :-). Again, because 1/0 is traditionally considered
"undefined", which is not a value in CC, and I think "/" should model the traditional
mathematical operation.

> Informal mathematics solves this issue by ignoring it. That's obviously not
> an option for us.

Yes, I agree completely. I think this is the fundamental challenge of formal systems;
"little details" that often get ignored in papers must be directly addressed somehow.
But I think this is also the potential glory of metamath; you can ensure it's all accounted for.

> I disagree. Consider the following experiment, which I have half a mind to
> enact: define "totalized division" as
>
> /t = ( x e. CC , y e. CC |-> if ( y = 0 , 0 , ( x / y ) ) )
>
> Then /t is clearly a total function, and it is the same thing as / away
> from zero.

I'm fine with defining *other* functions if they're convenient.
I just would like to see division, as traditionally defined, modeled.

--- David A. Wheeler

[Mario Carneiro]

On Tue, Sep 29, 2015 at 10:32 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

> I disagree. Consider the following experiment, which I have half a mind to
> enact: define "totalized division" as
>
> /t = ( x e. CC , y e. CC |-> if ( y = 0 , 0 , ( x / y ) ) )
>
> Then /t is clearly a total function, and it is the same thing as / away
> from zero.

I'm fine with defining *other* functions if they're convenient.
I just would like to see division, as traditionally defined, modeled.

 

The main reason I don't do this is because it leads to the following "slippery slope" argument. At what stage do you find it unacceptable?

1. Define /t in terms of /, as above.

2. Add convenience theorems for /t, deriving all the common properties.

3. Since every theorem of / is a theorem of /t, possibly with fewer hypotheses (but never with more), notice that /t is more pleasant to work with than / and hence make /t the "preferred" syntax.

4. Since /t now gets used much more than /, rename /t to have center focus as /, and rename / to /p.

5. At this point, /p will only be used in deriving properties of /, which could just as well be argued directly with /, so modify the definition of / to refer directly to the iota expression instead of defining it through the intermediate function /p.

6. Now /p is not used at all; it can be either deleted or moved to a mathbox with a similar status as df-gt.

I bought into the arguments before when talking about + as an axiomatic object rather than an actual function, but here we are talking about / *which is already a definition*, and generally we are allowed to choose our definitions, especially in order to make them more general if there is no corresponding loss. I usually take the approach when drafting definitions that a definition should have the widest possible domain such that it still makes sense to state, so that it can supersede any narrower definitions that might otherwise be considered in different domains. I realize this might be an over-trivialized example, but what if we wanted to support meadows as well? In a meadow 1/0 = 0, while in a ring 1/0 might equal 0, or it might equal something else or it could be undefined - the axioms don't say anything about this case. The only way to support *both* environments is by taking 1/0 = 0.

Mario

[Norman Megill]

On 9/29/15 10:32 PM, David A. Wheeler wrote:
> On Tue, 29 Sep 2015 21:04:20 -0400, Mario Carneiro
<di....@gmail.com> wrote:

> For the record, I think it should be *provable* that ( 1 / 0 ) e/ CC
... something
> I suspect we will *not* agree on :-). Again, because 1/0 is
traditionally considered
> "undefined", which is not a value in CC, and I think "/" should model
the traditional
> mathematical operation.

"Undefined" doesn't necessarily mean "not in CC". "Not in CC" would
actually be partially defining it. "Undefined" means we don't know or
care because we never use it. That will make our theorems and proofs as
general as possible.

>> Informal mathematics solves this issue by ignoring it. That's
obviously not
>> an option for us.

I think ignoring it is an option. That is what we pretty much do now.

On 9/30/15 12:18 AM, Mario Carneiro wrote:
>
>
> On Tue, Sep 29, 2015 at 10:32 PM, David A. Wheeler
> <dwhe...@dwheeler.com <mailto:dwhe...@dwheeler.com>> wrote:
>
> > I disagree. Consider the following experiment, which I have half a mind to
> > enact: define "totalized division" as
> >
> > /t = ( x e. CC , y e. CC |-> if ( y = 0 , 0 , ( x / y ) ) )
> >
> > Then /t is clearly a total function, and it is the same thing as / away
> > from zero.
>
> I'm fine with defining *other* functions if they're convenient.
> I just would like to see division, as traditionally defined, modeled.
>
> The main reason I don't do this is because it leads to the following
> "slippery slope" argument. At what stage do you find it unacceptable?
>
> 1. Define /t in terms of /, as above.
> 2. Add convenience theorems for /t, deriving all the common properties.
> 3. Since every theorem of / is a theorem of /t, possibly with fewer
> hypotheses (but never with more), notice that /t is more pleasant to
> work with than / and hence make /t the "preferred" syntax.

I am not convinced that /t would make a significant difference in the
big picture. The drawback is that it goes against virtually all
literature, which I think would turn off many mathematicians and confuse
beginners.

"Many in the theorem proving community would be likewise disgusted with a
definition of division that admitted equations like 1/0=0, or
likewise..." -
http://www.cs.nyu.edu/pipermail/fom/2015-September/019148.html

If /t ends up offering a significant advantage for some specialized
application, we can define it for local use there. But I think
replacing / with /t in the main development would turn off a lot of
people. It doesn't keep the reader in mind and it deviates from the
goal of documenting and communicating mathematics as it is done in the
literature.

> 4. Since /t now gets used much more than /, rename /t to have center
> focus as /, and rename / to /p.
> 5. At this point, /p will only be used in deriving properties of /,
> which could just as well be argued directly with /, so modify the
> definition of / to refer directly to the iota expression instead of
> defining it through the intermediate function /p.
> 6. Now /p is not used at all; it can be either deleted or moved to a
> mathbox with a similar status as df-gt.

If we do this we will end up with theorems and proofs intimately tied to
the 1/0 value, which will become incompatible with other proof languages
that adopt a different value or keep it undefined. Wouldn't you agree
that we should keep our theorems and proofs as generally applicable as
possible or practical, even if it occasionally means an extra inconvenience?

>
> I bought into the arguments before when talking about + as an axiomatic
> object rather than an actual function, but here we are talking about /
> *which is already a definition*, and generally we are allowed to choose
> our definitions, especially in order to make them more general if there
> is no corresponding loss.

The point of pretending + is an axiomatic object is to show arithmetic
as it is normally taught, as well as making it as general as possible in
some sense.

The fact that / is a definition doesn't mean that we should suddenly
switch philosophies. Most of our early theorems for it treat it no
differently from an axiomatic object i.e. they don't make any
assumptions about it being a set-theoretical operation object. In
principle this also makes it more compatible with a proof language that
defines only the compound operation value x/y without treating / as a
standalone object.

> I usually take the approach when drafting
> definitions that a definition should have the widest possible domain
> such that it still makes sense to state, so that it can supersede any
> narrower definitions that might otherwise be considered in different
> domains. I realize this might be an over-trivialized example, but what
> if we wanted to support meadows as well? In a meadow 1/0 = 0, while in a
> ring 1/0 might equal 0, or it might equal something else or it could be
> undefined - the axioms don't say anything about this case. The only way
> to support *both* environments is by taking 1/0 = 0.

I had never heard of meadows before. It appears they arose around 2008
to make type theory treatment of fields more elegant (correct me if I am
wrong). In any case they are a specialization of the theory of fields.
Our practice has been to start with general structures then specialize
them as needed. I don't think we'd want to start off defining CC as a
meadow with a bunch of theorems that hold for meadows but not fields in
general.

Norm

[Mario Carneiro]

On Wed, Sep 30, 2015 at 8:48 PM, Norman Megill <n...@alum.mit.edu> wrote:

>> Informal mathematics solves this issue by ignoring it. That's obviously not
>> an option for us.

I think ignoring it is an option. That is what we pretty much do now.

To be clear: Our discussion has strayed a bit from +oo + -oo, since 1/0 is a more common instance of a similar problem, but what I hope to practically get out of this discussion is to leave both / and +e alone for now (so 1/0 is undefined and +oo + -oo = 0). I have no current plans to implement /t, but it makes a good thought experiment.

 

If /t ends up offering a significant advantage for some specialized application, we can define it for local use there.  But I think replacing / with /t in the main development would turn off a lot of people.  It doesn't keep the reader in mind and it deviates from the goal of documenting and communicating mathematics as it is done in the literature.

One more question along these lines: suppose I were to define /t and use it in another definition, that uses division and has inconvenient zeroes, for example df-tan or df-gam? This is one of the main motivations I have had in the past to consider redefining / , because in derived functions the domains can get messy (and it is not necessarily the case that almost all the theorems need to be stated in the restricted domain anyway).

 

4. Since /t now gets used much more than /, rename /t to have center
focus as /, and rename / to /p.
5. At this point, /p will only be used in deriving properties of /,
which could just as well be argued directly with /, so modify the
definition of / to refer directly to the iota expression instead of
defining it through the intermediate function /p.
6. Now /p is not used at all; it can be either deleted or moved to a
mathbox with a similar status as df-gt.

If we do this we will end up with theorems and proofs intimately tied to the 1/0 value, which will become incompatible with other proof languages that adopt a different value or keep it undefined.  Wouldn't you agree that we should keep our theorems and proofs as generally applicable as possible or practical, even if it occasionally means an extra inconvenience?

The point that I was trying to make by stressing that / is a definition is that this is not the case. If the entire programme is enacted, then in just a few steps (comparable to a dedth application) we can transform any theorem about /t into one about /, possibly with extra guards just to ensure that / is not applied to any zero denominators, and this will be a perfectly correct theorem, compatible with other proof languages. To be sure if you check the "definitions used" list you will find df-divt in there, because it is probably used in the derivation somewhere (even possibly taking advantage of 1 /t 0 = 0), but this is no more suspect than the usage of df-top in say sincn, which a priori has nothing to do with topology. The whole point of conservativity of definitions is that we don't need to worry about which definitions are used in a proof, because they are all in principle eliminable.

 

I bought into the arguments before when talking about + as an axiomatic
object rather than an actual function, but here we are talking about /
*which is already a definition*, and generally we are allowed to choose
our definitions, especially in order to make them more general if there
is no corresponding loss.

The point of pretending + is an axiomatic object is to show arithmetic as it is normally taught, as well as making it as general as possible in some sense.

The fact that / is a definition doesn't mean that we should suddenly switch philosophies.  Most of our early theorems for it treat it no differently from an axiomatic object i.e. they don't make any assumptions about it being a set-theoretical operation object.  In principle this also makes it more compatible with a proof language that defines only the compound operation value x/y without treating / as a standalone object.

This is one reason why I keep / the way it is, since I understand your philosophy of keeping the introductory complex number material as simple as possible.

 

I usually take the approach when drafting
definitions that a definition should have the widest possible domain
such that it still makes sense to state, so that it can supersede any
narrower definitions that might otherwise be considered in different
domains. I realize this might be an over-trivialized example, but what
if we wanted to support meadows as well? In a meadow 1/0 = 0, while in a
ring 1/0 might equal 0, or it might equal something else or it could be
undefined - the axioms don't say anything about this case. The only way
to support *both* environments is by taking 1/0 = 0.

I had never heard of meadows before.  It appears they arose around 2008 to make type theory treatment of fields more elegant (correct me if I am wrong).  In any case they are a specialization of the theory of fields.  Our practice has been to start with general structures then specialize them as needed.  I don't think we'd want to start off defining CC as a meadow with a bunch of theorems that hold for meadows but not fields in general

I realize that talking about meadows is sort of a straw man argument, because they are basically built around the assumption that 1/0 = 0 is a good thing. (Nevertheless, Jan Bergstra has written some good arguments in those links to back this philosophy up.) At the very least it answers positively the question of whether 1/0 = 0 has been investigated in research mathematics. This is also a fairly rare phenomenon in that it appears that the process of doing formal math has informed the informal math community and developed a new field of research in pure abstract algebra. The reasons which made 1/0 = 0 attractive in type theory apply just as well to us, though. Computerized type theory is basically the result of trying to make closure proofs automatically derivable. For this it is convenient to make sure that closure theorems are as simple as possible, and side conditions get in the way of this derivation.

However, Metamath is not HOL Light, and we have different goals. I appreciate that being pedagogically useful and being efficient for authors do not always align, but since I usually find myself on the side of the authors I hope you can understand my motivations.

Mario

[fl]

  > It doesn't keep the reader in mind and it deviates from the
> goal of documenting and communicating mathematics as it is done in the
> literature.

Speaking of communication, there was a feature in metamath that I liked: the fact

that for every theorem and definition a precise reference to an accessible treatise

in the "literature" was given. It had often given me the desire of reading the original.

 

I don't know why but it is no longer the case. Despite in my opinion the negligent

contributors in no case are the inventors of the material they "borrow".

 

I regret this (among other things).

 

--

FL 

[Mario Carneiro]

This is a serious problem that I recognize should be addressed. My usual strategy for filling out the library is to browse Wikipedia, lecture notes, and sometimes textbooks (usually online) looking for *theorem statements*. I cannot stress enough that this is my main bottleneck in production: I need to know what I should be proving in the first place. For example when I drafted quotient spaces I just read the wiki page for "properties" and just wrote them all down as theorem statements. Except in extreme cases, it is usually not necessary to also supply a *proof* - I generally make these up as I go along, because most of the time it is quite clear how to move forward.

TL;DR for casual readers: if you want to help me populate the database with your favorite theory, it would be very helpful if you sent me a list of simple, obvious theorems that you think are essential for efficient manipulation of the involved concepts. Proofs are not necessary - I can usually make them up or look them up as necessary. For example, using the recently added theory of topological groups:

 

* addition is continuous

* negation is continuous

* subtraction is continuous

* negation is homeomorphism

* topological group iff subtraction is continuous

* group multiple function is continuous
* group sum function is continuous
* a neighborhood V of 0 has a symmetric subneighborhood U = -U with U + U C_ V

* opposite of a top group is a top group

* a discrete or indiscrete group is a top group

* symmetric group is a top group with the product topology

* left group action is a homeomorphism

* subgroup of a top group is a top group

* closure of a (normal) subgroup is a (normal) subgroup

* an open subgroup is closed

* a closed subgroup of finite index is open

* a subgroup with nonempty interior is open

* connected component containing 0 is a normal subgroup

* a top group is Hausdorff iff {0} is closed

It doesn't take any special skills to come up with a list like this, and I usually don't think of them on my own unless they show up in a textbook as an example/theorem/exercise or if they are directly necessary for some other proof.

But coming back to FL's concern, I think you can see why this approach to producing theorems more often than not makes unreferenced theorems. It is no lie to say that I "came up with the proof myself", in the same sense that a student discovers a solution to a homework problem on their own, but clearly it would be better if there was more complete attribution to existing literature. The database is ripe for a "reference finding" project along the following lines:

1. Open any citable textbook which covers material similar to what is in set.mm. I'd give slight preference to books we are already referencing.

2. Read the chapter in the book and compare with the relevant set.mm section. Whenever a statement in the book matches or nearly matches a statement in set.mm, add the appropriate citation to the set.mm theorem.

3. Since I'm trying to make each set.mm section roughly the union of all "chapter 1" theorems for the topic over all relevant textbooks, you should have a high hit ratio (almost all the textbook theorems should be covered), meaning that you will make lots of progress in step 2. If there are theorems in the book which are not in set.mm, let me know!

However, I don't think that I should head such a project. I know where my strengths lie, and that is why I focus mainly on producing theorems instead. The downside is that if we go too long with me just churning out theorems with this sort of "clerical work" by the wayside, the database ends up in a lopsided state. I know that there are a number of Metamath users/readers who don't feel confident writing theorems themselves, and I want you all to know that there are many other ways you can improve the state of the database doing important work which may not be directly mathematical.

Mario

[fl]

> For example, using the recently added theory of topological groups:

By the way, I know that I have not been fortunate enough to have my own proofs make official

even for a short time. But I would appreciate that an acnowledment is made to my defunct work

even it is not your "policy".

 

There are even references that you can copy.

 

--

FL

[Mario Carneiro]

I'm not sure what you mean; I imported your entire section, with attribution and the Bourbaki references intact. For example:

      tgpinv.5 $e |- I = ( invg ` G ) $.
      $( In a topological group, the inverse function is continuous.
         (Contributed by FL, 21-Jun-2010.  Revised 21-Jun-2014.) $)
      tgpinv $p |- ( G e. TopGrp -> I e. ( J Cn J ) ) $=
        ( ctgp wcel cgrp ctmd ccn co istgp simp3bi ) AFGAHGAIGBCCJKGABCDELM $.
        $( [27-Jun-2014] $) $( [21-Jun-2010] $)

Granted there aren't too many of them, but that's mainly because you only proved a handful of theorems on topological groups; as of now http://us2.metamath.org:88/mpegif/mmtheorems203.html#df-topgrp still shows the old state of the database before my update (the update is not yet on the web) where I count 6 theorems on topological groups, all of which appear with attribution to you in the imported version.

Mario

[Norman Megill]

On 9/30/15 9:44 PM, Mario Carneiro wrote:
>
>
> On Wed, Sep 30, 2015 at 8:48 PM, Norman Megill <n...@alum.mit.edu
> <mailto:n...@alum.mit.edu>> wrote:
>
> >> Informal mathematics solves this issue by ignoring it. That's obviously not
> >> an option for us.
>
> I think ignoring it is an option. That is what we pretty much do now.
>
>
> To be clear: Our discussion has strayed a bit from +oo + -oo, since 1/0
> is a more common instance of a similar problem, but what I hope to
> practically get out of this discussion is to leave both / and +e alone
> for now (so 1/0 is undefined and +oo + -oo = 0). I have no current plans
> to implement /t, but it makes a good thought experiment.

I checked Wolfram Alpha, and they define 1/0 = complex infinity. Also
both 0/0 and oo - oo are "undefined".

Assuming +oo + -oo = 0, what did I overlook in the following? Does
addition become non-associative?

1 + +oo = +oo = 2 + +oo
(1 + +oo) + -oo = (2 + +oo) + -oo
1 + (+oo + -oo) = 2 + (+oo + -oo)
1 + 0 = 2 + 0
1 = 2

Norm

[Mario Carneiro]

On Thu, Oct 1, 2015 at 8:41 AM, Norman Megill <n...@alum.mit.edu> wrote:

On 9/30/15 9:44 PM, Mario Carneiro wrote:

On Wed, Sep 30, 2015 at 8:48 PM, Norman Megill <n...@alum.mit.edu
<mailto:n...@alum.mit.edu>> wrote:

    >> Informal mathematics solves this issue by ignoring it. That's obviously not
    >> an option for us.

    I think ignoring it is an option. That is what we pretty much do now.


To be clear: Our discussion has strayed a bit from +oo + -oo, since 1/0
is a more common instance of a similar problem, but what I hope to
practically get out of this discussion is to leave both / and +e alone
for now (so 1/0 is undefined and +oo + -oo = 0). I have no current plans
to implement /t, but it makes a good thought experiment.

I checked Wolfram Alpha, and they define 1/0 = complex infinity.  Also both 0/0 and oo - oo are "undefined".

The choice 1/0 = complex infinity makes sense on the one-point compactification of CC, a.k.a the Riemann sphere. I may start moving into this direction once projective geometry gets off the ground. Mathematica also defines DirectedInfinity which acts more like our +oo, -oo, but also includes an infinity in each imaginary direction (each unimodular complex number), also similar to the projective geometry conception (although in this case it is P^2(RR) instead of P^1(CC) so that you get an infinity in each direction).

Assuming +oo + -oo = 0, what did I overlook in the following?  Does addition become non-associative?

1 + +oo = +oo = 2 + +oo
(1 + +oo) + -oo = (2 + +oo) + -oo
1 + (+oo + -oo) = 2 + (+oo + -oo)
1 + 0 = 2 + 0
1 = 2

Correct. Associativity of addition is the only main theorem which fails for +oo + -oo: there is no consistent assignment of +oo + -oo which makes associativity work. See xaddass:

  $( Associativity of extended real addition.  The correct condition here is
     "it is not the case that both ` +oo ` and ` -oo ` appear as one of
     ` A , B , C ` , i.e. ` -. { +oo , -oo } C_ { A , B , C } ` ", but this
     condition is difficult to work with, so we break the theorem into two
     parts: this one, where ` -oo ` is not present in ` A , B , C ` , and
     ~ xaddass2 , where ` +oo ` is not present.
       (Contributed by Mario Carneiro, 20-Aug-2015.) $)
  xaddass $p |- ( ( ( A e. RR* /\ A =/= -oo ) /\ ( B e. RR* /\ B =/= -oo ) /\
  ( C e. RR* /\ C =/= -oo ) ) -> ( ( A +e B ) +e C ) = ( A +e ( B +e C ) ) ) $=

I'm not going to repeat the whole argument, but let me just remind you that just by defining +oo + -oo in no way am I making a promise that all theorems will work on this extended domain. Associativity is one of these cases.

Mario

[fl]

Le jeudi 1 octobre 2015 14:32:36 UTC+2, Mario Carneiro a écrit :

On Thu, Oct 1, 2015 at 8:14 AM, fl <freder...@laposte.net> wrote:

> For example, using the recently added theory of topological groups:

By the way, I know that I have not been fortunate enough to have my own proofs make official

even for a short time. But I would appreciate that an acnowledment is made to my defunct work

even it is not your "policy".

 

There are even references that you can copy.

I'm not sure what you mean; I imported your entire section, with attribution and the Bourbaki references intact. For example:

 

 

Thank you I knew that in your heart you were a good boy.

 

 

The definition of word should have the same destiny if you were good enough. 

 

--

FL

[Mario Carneiro]

On Thu, Oct 1, 2015 at 9:06 AM, fl <freder...@laposte.net> wrote:

The definition of word should have the same destiny if you were good enough. 

The problem with attribution for Word is that it was worked on somewhat independently by you (the Kleene definition) and Stefan (with Word), but on incompatible definitions (Word is 0-based, Kleene is 1-based). Insofar as you have a "morally" equivalent definition and the earlier claim, your name is attached to df-word and df-concat as contributor, with Stefan marked as revising the definition. Your name is also on some of the more advanced theorems whose proofs were adapted for the new setup, such as closure of concatenation ccatcl (called clscnc in your mathbox).

Since the definitions are different, though, it's not clear if I should delete Kleene (moving over any remaining contrib comments to the equivalent Word theorems) and retrofit the remainder of the theorems in your mathbox (the grammar stuff) to use 'Word'-based definitions. You have objected to this in the past, which is why I haven't attempted anything, but I'm not a fan of having multiple definitions for the "same" thing.

If you want to know why I imported Stefan's definition instead of yours, the simple answer is that his section has some 5 to 10 times as many theorems as yours, and he managed to develop the section to the point that it could be used for a proof in a different section (in his case, some group sum theorems and the sign of a permutation), so evidently his definition "works" at a practical level. Not to say that your definition doesn't / can't be made to work, but it is important to work out enough utility theorems to get a familiarity with the definition and address the drawbacks adequately. Too many of your definitions are not developed beyond 2-5 definitional theorems, so that you can't be sure whether the definition captures everything you want. isplibg looks impressive, but since you never proved anything other than the definition it's not clear what any of it means or how it relates to anything else, which means it is hard for me to find a way to use it and import it for any work in a different section.

 

Mario

[fl]

 

The problem with attribution for Word is that it was worked on somewhat independently by you (the Kleene definition) and Stefan (with Word), but on incompatible definitions (Word is 0-based, Kleene is 1-based).

 

 

The problem with attribution is not that you can't replace a definition or a theorem by another one. We are not so

vain. The problem is simply to recall that a contributor or another has made a contribution about the subject. A simple

matter of politeness. Obviously that you choose to make official another definition most often on a vanity

or opportunism or random basis doesn't matter. And even if you try to disguise the real motives by introducing

a small difference to the definition to give an apparence of rationality to your choice;

 

--

FL

[fl]

 

The problem with

 

 

Another word. If you want to lose contributors, make official a definition that is perfectly incompatible

with their work. The success is guaranteed.

 

--

FL

[Jens-Wolfhard Schicke-Uffmann]

Hi,

given my so-far minimalist contribution, my opinion shouldn't carry too
much weight here, but

On Thu, Oct 01, 2015 at 08:07:13AM -0700, fl wrote:
> If you want to lose contributors, make official a definition that
> is perfectly incompatible with their work.

the most important quality of the set.mm project for me is internal
consistency. I'd rather not read multiple definition of similar things
without some connecting theorems between them. Because then, how would I
(who didn't invent the various ways to define the same idea formally)
know which one to use and what the up- and downsides are?

Hence I am pretty grateful for some force (whoever it might be), who
makes a (ideally well informed) decision which variation is the main
one. (And puts some comments in set.mm which alternatives exist and
what the differences are.)


Regards,
Drahflow

[fl]

given my so-far minimalist contribution, my opinion shouldn't carry too

much weight here, but [...]

 

You should try to write without parentheses. It makes the main idea clearer

and you will look more self confident: it's important in a neoliberalism

world order.

 

 --

FL

[Cris Perdue]

Another vote on the value of 1/0 -- I vote that the value be outside the domain of the function, so not a real number for division of real numbers.

My main motivations for this are that traditionally 1/0 is "undefined", whatever exactly that may mean (certainly not 1/0 = 0); and that requiring the value to be outside the input domain guarantees that equations such as 1/0 = x or ex = 0 or sqrt x = -1 have no solution in ℝ in the usual sense that ∀x ∈ ℝ 1/0 ≠ x and so on.

In Metamath, would you make 1/0 for a domain D be Undef ` D? That would allow division to be defined with restricted definite description.

My personal taste preference would be to write 1/0 = ⊥, as in https://en.wikipedia.org/wiki/Scott_domain and so-called denotational semantics. (Fully worked out, I would consider this a form of what Harrison calls a true logic of partial terms.) But unfortunately this does not seem achievable without introducing urelements and/or making other relatively unconventional changes. Any thoughts on this?

-Cris

On Mon, Sep 28, 2015 at 12:03 PM, Mario Carneiro <di....@gmail.com> wrote:

To be sure, it is arbitrary. Well, not that arbitrary: the only choice that makes xaddcom and xnegdi true unconditionally is +oo + -oo = -oo + +oo = 0. But this situation bears a strong resemblance to the 1/0 = ? problem, which was recently discussed on FOM. I'll quote from (a quote from) John Harrison:

> To: q...@mcs.anl.gov

> Subject: Re: Undefined terms
> In-reply-to: Your message of "Thu, 18 May 1995 12:39:59 MDT." <1995051818...@antares.mcs.anl.gov>

> Date: Fri, 19 May 1995 10:54:02 +0100

> From: John Harrison <John.Harrison@cl.cam.ac.uk>

> Message-ID: <"swan.cl.cam.:266770:950519095422"@cl.cam.ac.uk>

|- ( ( ( A e. RR* /\ B e. RR* ) /\ ( A =/= +oo \/ B =/= -oo ) /\ ( A =/= -oo \/ B =/= +oo ) ) -> ( A +e B ) e. RR* )

if this were to be done. My goal with the new xadd* theorems is to make the new theorems as close as possible to the addition theorems, with even the names and hypothesis order borrowed directly from the originals. For this to work I want +e to inherit *as many theorems as possible* from the RR context, straight into the square domain ( RR* X. RR* ), which entails giving those points the nicest possible values. As far as I see it, there are already a number of concessions which need to be made to keep the theorems true in RR*, and doing this would only make it worse.

But then again, I am personally in favor of 1/0 = 0 as well, so perhaps someone else can cast a vote on the matter?

Mario

On Mon, Sep 28, 2015 at 7:59 AM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

Overall it looks nice.

However, +oo + -oo = 0 seems arbitrary, can't that be avoided?

--- David A.Wheeler

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at http://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Mario Carneiro]

On Mon, Oct 5, 2015 at 4:30 PM, Cris Perdue <cr...@perdues.com> wrote:

Another vote on the value of 1/0 -- I vote that the value be outside the domain of the function, so not a real number for division of real numbers.

My main motivations for this are that traditionally 1/0 is "undefined", whatever exactly that may mean (certainly not 1/0 = 0); and that requiring the value to be outside the input domain guarantees that equations such as 1/0 = x or ex = 0 or sqrt x = -1 have no solution in ℝ in the usual sense that ∀x ∈ ℝ 1/0 ≠ x and so on.

In Metamath, would you make 1/0 for a domain D be Undef ` D? That would allow division to be defined with restricted definite description.

I have always found (Undef`A) a bit distasteful, and I would like to remove it from df-riota (as soon as all the dependent theorems are pushed to alternate methods, which will not be for a while). The thing is that (Undef`A) does *not* represent an "undefined" value - it represents a value that is defined and different from every element of A. The common mathematical notation for this uses +oo or something - and in fact the definitions df-pnf, df-mnf would be a good use of the Undef function (they aren't defined that way due to some technicalities in the derivation of reex).

I think we have the correct approach in letting undefined values be equal to a certain canonical representative of undefinedness, namely (/). This maximizes the chance of "accidental equalities" of out-of-domain values, which allows for a lot of reverse closure theorems and shorter hypotheses. "Accidental disequalities" (which is what Undef gives you) are much less useful (in a nutshell because equality is transitive but disequality is not). Much better to only have disequalities when they are meaningful, i.e. +oo e/ RR is necessary for x e. RR -> x < +oo to work.

 

My personal taste preference would be to write 1/0 = ⊥, as in https://en.wikipedia.org/wiki/Scott_domain and so-called denotational semantics. (Fully worked out, I would consider this a form of what Harrison calls a true logic of partial terms.) But unfortunately this does not seem achievable without introducing urelements and/or making other relatively unconventional changes. Any thoughts on this?

It is interesting that you mention this, because just yesterday I thought about a few of our missing "categorical constructions" and this is one of them. For context, we currently have products via df-xps, infinite products via df-prds, quotients and forward images via df-imas and df-divs, and finitely supported products (indexed direct sums) via df-dsmm, but we still lack disjoint unions, and in particular the "add one" special case of this.

A disjoint union does not have natural group, ring, etc operations, but it is an important construction in topology and one can also define an extended metric naturally on a disjoint union. (There is a natural total order on a disjoint union of total orders, but only if the base set is ordered. I'd probably just stick with the natural partial order, where distinct components are not in relation with each other.) The one-point addition also has a number of uses, and in this case there is also a natural monoid extension setting x + O = O = O + x (where O is the new point), while topology has the Aledandroff one-point compactification and the order has the option of making O either the maximum or the minimum, as in your link. I'm actually inclined to call the point oo (infinity) and make it the top element of the order.

The construction which lead me on this line of thought was https://en.wikipedia.org/wiki/Valuation_%28algebra%29 , which discusses a certain function from a field K to the one-point extension of an ordered abelian group G. It would be simpler to define the function only on nonzero elements of the field and skip the extension business, but I haven't found any sources which do it this way, so I'm faced with the (not so rare) choice of taking the easy path or following mathematical intuition and the literature, and both choices have their drawbacks.

 

Later: On review, I think I may have missed the point of Cris's comment. Ah, well.

Mario

[fl]

 
> I have always found (Undef`A) a bit distasteful

May I recall the trick that has been found by functional language oriented computer scientists; you return a set with

the values inside. If the function is not defined, it returns the empty set. If the function returns something it returns

a singleton. It maybe a singleton with the empty set inside obviously. It also works with relations. In that case

you return a set with several elements. As you can see the trick is generic.

 

It works remarkably well with the definition of a limit and you can express easily the case where the limit doesn't exist.
 

 --

FL

[Cris Perdue]

Yes, Frederic caught the direction of my thoughts. His trick is exactly what occurred to me, though I do not see how to carry out the concept in a satisfactory way without a bit of, shall I say, "remodeling" of standard set theory itself.

If one were willing to exclude the empty set from all domains (integers, real numbers, etc.), it could then serve to indicate application of a function to an object outside its domain, and I would not see a need for restricted definite description or the Metamath Undef, and that would be very good in my eyes.

Unfortunately this has not been the habit in set theory.  The traditional ordinal and cardinal numbers in particular include the null set as their zero.

Alternatively --

If the "bottom" object is not to be the same as the null set, I find myself led to a theory in which it is not a set at all. For me, Michael Potter's approach in "Set Theory and Its Philosophy" (2004) for example seems quite reasonable. In it, "bottom" (⊥) would be an urelement -- thus not itself a set. Not that this is shocking in itself. Historically, I doubt there was any mathematician anywhere before 1900 who thought all mathematical entities were sets. (Maybe even 1950?)

Urelements avoid the unpleasantness of "junk theorems" that occur due to everything being a set and having properties as a set that are not intended for their mathematical domain -- and of course are true to mathematical thinking up to the 20th century.

But urelements not part of conventional set theory.  In my 1964 edition of Mendelson's "Introduction to Mathematical Logic" he mentions urelements but simply mentions that he will not use them in his development of set theory because it does not require them. Suppes "Axiomatic Set Theory" (1960) also mentions urelements respectfully without including them.

Shoenfield in "Mathematical Logic" (1967) in fact does include urelements in his set theory, building up his universe of sets in a sequence of stages, where sets in the first stage contain only urelements, and each following stage contains all sets of objects in all previous stages. Potter does rather similarly, in fact. But still standard ZF, ZFC, etc. do not have them, as we know.

-Cris

--

[Mario Carneiro]

It is exactly this sort of thinking which leads to type theory! Type theory is designed to "avoid the unpleasantness of 'junk theorems' that occur due to everything being a set". Of course set theory is designed to avoid the unpleasantness that occurs when *not* everything is a set - it goes both ways. If you have ever seen &0 appear in a HOL light theorem, you will know the price that they had to pay by emphasizing a multitude of well-chosen types and injections between them rather than an all inclusive universe with many natural subsets. I find that it is often easier to do type theory in set theory than type theory in type theory, because of simple things like ( x e. NN -> x e. RR ). (I think the best foundation is set theory pretending to be type theory, like Mizar, or set.mm once closure proofs are automated and hidden by intelligent proof assistants.)

There is of course a natural type-theoretic construction for adding a "null" value, which is to say a type A+ := A' u. { O } given a type A (producing a constructors "some : A --> A+" and "none : A+"). It's usually called "option" or "maybe", and it is equivalent to the plus-one construction I was talking about earlier or the (Undef`A) construction given a set A. The important part is not to try to push this up to the "top level", where we have A being the universe of all sets, because that is where we run into axiomatic strengthenings for no good reason. There are some really big sets in ZFC; you should be satisfied with performing your construction on a "sufficiently large" set A rather than on the whole universe (because that way no "remodeling" is necessary).

The drawback of doing it this way is that you have to relativize; you can't just write "Undef e/ _V", you have to have "(Undef`A) e/ A". But perhaps that's not such a drawback after all. We here have a precedent for a similar issue: the constant ~H (chil, ax-hilex) which appears in the Hilbert space explorer. This is not a defined notion; Norm wanted a "big set" ~H so he posited one. All the theorems involving ~H are theorems which apply to any Hilbert space, but you won't be able to prove this in Metamath - if you want to reuse any of them on some other Hilbert space constructed in ZFC, you are out of luck. This was later fixed by defining CHil, which is just the relativization of ~H. Even just in one theory, you often find yourself reusing bits of the theory in itself (for example, a Grp is a Mnd, and a Ring is a Grp whose multiplication is a Mnd) and if you do "global" arguments you don't have this opportunity of reuse.

Mario

[Cris Perdue]

By the way, I would be delighted to try to respond to what Mario wrote, but his understanding of math goes far beyond my own, and there is probably no point in this case.

-Cris

[Norman Megill]

On 10/5/15 7:08 PM, Mario Carneiro wrote:
> I have always found (Undef`A) a bit distasteful, and I would like to
> remove it from df-riota (as soon as all the dependent theorems are
> pushed to alternate methods, which will not be for a while).

I agree, it was a somewhat failed experiment, and df-riota should be
changed. My motivation was posets, where books frequently talk about
lub and joins "existing", with theorems beginning "if the lub exists,
then..." See for example lubprop where U`S e. B is meant to express
"the lub of S exists". There are other ways to express this that will
have to be used when we change df-riota, but in any case we need the
"lub exists" condition less frequently than I expected and it's not a
big deal.

On 10/6/15 7:08 AM, fl wrote:
> May I recall the trick that has been found by functional language
> oriented computer scientists; you return a set with
> the values inside. If the function is not defined, it returns the empty
> set. If the function returns something it returns
> a singleton. It maybe a singleton with the empty set inside obviously.

I have been aware of this method and its advantages, which are nice. A
primary issue is that it doesn't conform to conventional usage, and I've
tried to follow the literature wherever possible, for better or worse
(sometimes for the worse), to make it as easy as possible for the reader
to correlate set.mm theorems with a textbook they are studying.

We already have this method available by using the image of a singleton
in place of function value. So for any situation where it offers an
advantage we can use that.

Adopting it everywhere at this point would be a huge retrofitting
project, and I'm not sure it would actually buy all that much. The
nitpicks about Undef arise only infrequently since it is hardly used at
all. In particular, with x/y we simply avoid referencing out-of-domain
values, which I think is the best and most general approach.

We can solve the problem of Undef being base-set dependent by defining
the out-of-domain value of df-fv, as well as the value of df-iota when
uniqueness fails, to be the universal class _V. In some abstract sense
I find this an elegant solution, since the value will then literally not
exist. However, in a practical sense it would be a lot more tedious and
annoying to prove things since we would lose the shortcuts provided by
fvex and related existence theorems. The empty set as the out-of-domain
value is a compromise to make proofs more practical.

Norm

[Cris Perdue]

I will respond to Mario's posting contrasting type theory and set theory, as I do have some background in this.

He mentions HOL Light and "&0", a notation for the 0 of the real numbers. HOL Light is based on Church-style type theory, and I will only be referring here to that style, not on other varieties such as Homotopy Type Theory, which I can't help with.

Type theory does not actually require that real numbers must be treated separately from the integers or natural numbers, leading for example to notation such as "&0" to distinguish which zero is intended. The one exposition of type theory frequently referred to is Peter Andrews' "Introduction to Mathematical Logic and Type Theory" (https://books.google.com/books?id=UaPuCAAAQBAJ), in which the type theory does not provide for definition of new types even though it does include a construction of countably many cardinal numbers. In this book there is no actual type for the reals or the integers, etc.. In this respect it is like set theory.

But yes, I agree it is characteristic of type-theoretic thinking to have numbers and other entities that are not necessarily sets. 

It seems to me that it might be helpful for some purposes to use the kinds of description used in abstract algebra -- that a structure "is a group" or "forms a ring" rather than "being the integers".  Suppose "Nat" were a predicate with three arguments: a set, a "zero" element and a "successor" function. Treating "ℕ", "0", and "succ" as variables, statements about the natural numbers would amount to:

∀(ℕ, 0, succ) ∈ Nat: ∀n ∈ ℕ: n ≥ 0

where of course we normally just write

∀n ∈ ℕ: n ≥ 0

Are there objections to this way of thinking about things like numbers?

-Cris

[Mario Carneiro]

On Tue, Oct 6, 2015 at 8:24 PM, Cris Perdue <cr...@perdues.com> wrote:

It seems to me that it might be helpful for some purposes to use the kinds of description used in abstract algebra -- that a structure "is a group" or "forms a ring" rather than "being the integers".  Suppose "Nat" were a predicate with three arguments: a set, a "zero" element and a "successor" function. Treating "ℕ", "0", and "succ" as variables, statements about the natural numbers would amount to:

∀(ℕ, 0, succ) ∈ Nat: ∀n ∈ ℕ: n ≥ 0

where of course we normally just write

∀n ∈ ℕ: n ≥ 0

Are there objections to this way of thinking about things like numbers?

Indeed it is very useful to generalize statements like these two arbitrary structures, and that's been exactly my goal with all these new structures like TopGrp, LMod, and (teaser) NrmVec. But one can reasonably ask, as you have, why NN and RR are not so defined. After all that talk of relativization, why do we choose one specific construction for RR?

The big difference here is that NN and RR are uniquely defined up to isomorphism. Mathematicians like to pretend that isomorphic structures are equal, so they have no qualms about writing A. x e. RR x < ( x + 1 ) when they really want to quantify over all real number systems. For us, we can't actually let all real number systems be equal to one another as that would be a contradiction (note, though, that it is possible and practical to do this in HoTT), but we can do the next best thing: replace "R is a real number system" with "R is isomorphic to RR" where RR is a specific construction of a real number system.

This has actually been done in an abstract algebra setting with Stefan's theorem lmisfree, which asserts that a module has a basis iff it is isomorphic to a specific construction of something that we call a free module - by using this approach we don't need to define "free" categorically but can instead refer to the construction as a definition of "free module". (A construction of free monoids and free groups is coming soon, and there you will see the same thing.)

I don't think this is always possible; for example we can't pick one construction of a free ultrafilter on NN because there aren't any. But in many interesting cases it is possible, and when it is, we get the "best of both worlds" in that we have the convenience of absolute statements (we don't need extra quantification over real number systems) while still having the generality of a relative statement (because the isomorphisms can be used to transfer theorems from the construction to other isomorphic structures). This doesn't work with ~H because Hilbert spaces are not unique up to isomorphism.

Mario

[Cris Perdue]

Continued ...

A tangible outcome of all of this would be, in a typical first-order logic at least, that one could add constant symbols to the language for ℕ, 0, and succ, with exactly the properties desired (like satisfying Peano's axioms) and be assured of maintaining consistency. This seems like a good combination.

[fl]

I agree, it was a somewhat failed experiment,

 

I don't understand why you are so self-critical.

 

Adopting it everywhere at this point would be a huge retrofitting
project, and I'm not sure it would actually buy all that much.  

 

 

Only use it when there is a partial function or when the "function" is a relation

as in the case of a limit (which is also "partial" by the way).

 

 

The
nitpicks about Undef arise only infrequently since it is hardly used at
all.  In particular, with x/y we simply avoid referencing out-of-domain
values, which I think is the best and most general approach.

 

 

The fact that computer experts prefer testing returned values lets me think

it won't be so simple. I suppose it is a matter of complexity of the conditions.

 

When you see how complex can be the conditions of existence of a limit!

 

--

FL

[fl]

We already have this method available by using the image of a singleton
in place of function value. So for any situation where it offers an
advantage we can use that.

 

 

I hadn't understood but you are right when the function is partial or when we have a relation

don't use ( F ` A) use ( F " { A } ). And then test if you get the empty set or a singleton. It is

simple, easy, generic, perfect.

 

--

FL 

[Mario Carneiro]

Note also that if you are testing that it is not empty that is the same as A e. dom F, which is the preferred method I have used for partial functions like _D (when we want to treat the thing as a function), or using relations instead as in ~~> (which is really the same sort of thing, but writing ( ~~> ` F ) looks more peculiar). It is not always clear whether to use sets or relations in some cases, though, for instance with tsums: the current definition is as a set, so A e. ( G tsums F ) means that the sum of F converges to A, but it could also have been defined as F ( tsums ` G ) A instead, which would make it more like the limit relation.

Method 1                  | Method 2                            | Meaning

A e. ( G tsums F )        | F ( tsums ` G ) A                   | F converges to A

( G tsums F ) =/= (/)     | F e. dom ( tsums ` G )              | F converges
( G tsums F ) ~<_ 1o      | Fun ( ( tsums ` G ) |` { F } )      | F converges to at most one point
( G tsums F ) ~~ 1o       | ( ( tsums ` G ) |` { F } ) Fn { F } | F converges uniquely
A. f ( G tsums f ) ~<_ 1o | Fun ( tsums ` G )                   | sums are unique
A. f ( G tsums f ) C_ C   | ran ( tsums ` G ) C_ C              | Every convergent sum is in C
( G tsums F ) C_ C        | ( ( tsums ` G ) " { F } ) C_ C      | Every convergent sum is in C
U. ( G tsums F )          | ( ( tsums ` G ) ` F )               | The unique sum of F

As you can see from this comparison chart, there are advantages and disadvantages to each method; some concepts are easier to describe with method 1 and others are easier with method 2. Note also that method 2 singles out one of its arguments (F) as being "the independent variable" with the others as parameters, while method 1 treats all the auxiliary parameters the same - there is no special syntax for talking about varying F.

Mario

[fl]

 

As you can see from this comparison chart, there are advantages and disadvantages to each method; some concepts are easier to describe with method 1 and others are easier with method 2.

 

 

 

Sure but transforming a partial relation into a total function using conditions in my opinion hide the true nature of things. And I think one might have

simpler theorems if you remove the conditions.

 

In the case of limits for instance, I think it is unfortunate they are always presented as total functions with appended conditions.

 

There is also the case of partial functions that are definied by a formula where partial functions are called. In that case propagating the empty set may

simplify the formula.

 

--

FL