The Russell class and the function "Undef"

[Benoit]

Hi all,

It looks like the theorem

|- { x e. A | x e/ x } \notin A

is not in set.mm (but I'm not good at searching...). I think it is important, especially since the only non-logical axiom needed is extensionality (it is of course a trivial consequence of regularity). As a byproduct, this could be used to advantageously replace the current definition of Undef from

df-undef $a |- Undef = ( s e. _V |-> ~P U. s )

to

df-undef $a |- Undef = ( s e. _V |-> { x e. s | x e/ x } )

thus dispensing with the axiom of powerset, and needing only extensionality, which is a big gain. This would allow to introduce iota and riota much sooner in set.mm, in the section on extensionality, where I think they belong.

I think the "Russell class" appears often enough to deserve a definition

df-russ $a |- Russell = { x | x e/ x }

so that the proposals I made above would read

|- A \cap Russell \notin A
df-undef $a |- Undef = ( s e. _V |-> ( s \cap Russell ) )

(Note that the theorem |- Russell \notin V is a special case already in set.mm, labelled ru.)

What do you think

--
Benoit

[Mario Carneiro]

It is true that this theorem is not in set.mm, and I think it is a good standalone theorem, possibly as a replacement for ru (i.e. reproving ru as a corollary). I also once proposed it as a replacement for df-undef, but there isn't any real reason to use it (the rank of the set is a bit lower? It's a longer formula), and it doesn't really matter for most applications of df-undef how it is defined. It is worthwhile also to point out that the ~P U. A e/ A proof generalizes to ~P ... ~P U. A e/ A, while the Russell class doesn't (although you can do it with repeated applications of the Russell construction on a union of everything you want to avoid, with a little work). This is used, for example, to define the elements +oo and -oo so that they are distinct from each other and not in CC.

I don't see a good argument for the Russell class as a definition though. It doesn't actually appear anywhere - ru itself is sort of an endpoint theorem, it never gets used AFAIK. Even df-undef is rarely used, and you only need a few key theorems in this area before you have more set-avoiding than you could ever need. If anything was to get a definition, I would suggest something like disjenex, which gives a bit more parametric control over what to avoid and how many elements you want. (I originally formulated that theorem and its corollaries for doing field extensions, so that you can do a construction over another structure, and then re-situate it as a superset of the old structure, which would allow things like the real numbers construction in which NN0 = om.)

I would like to introduce df-riota earlier, but I would prefer to do it by removing the dependence on df-undef entirely. I've argued before on this list about replacing the definition of df-riota to return (/) instead of Undef when it is not unique. It's an out of domain thing anyway, and the empty set is much more likely to make "coincidentally true" theorems, while Undef is almost adversarially avoiding such things.

Mario

--
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+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Benoit]

On Saturday, September 9, 2017 at 10:51:59 PM UTC+2, Mario Carneiro wrote:

It is true that this theorem is not in set.mm, and I think it is a good standalone theorem, possibly as a replacement for ru (i.e. reproving ru as a corollary). I also once proposed it as a replacement for df-undef, but there isn't any real reason to use it (the rank of the set is a bit lower? It's a longer formula), and it doesn't really matter for most applications of df-undef how it is defined.

The reason I see is that the property we want for Undef, namely Undef(x) \notin x, can thus be proved with only extensionality, instead of extensionality + powerset. This is a huge gain: extensionality is the base axiom of any set theory, while powerset is a very powerful axiom (compare Kripke-Platek). Of course, this does not matter for the applications, and anyway we are later working in ZF. But this allows to move riota in the section about extensionality.

 

It is worthwhile also to point out that the ~P U. A e/ A proof generalizes to ~P ... ~P U. A e/ A, while the Russell class doesn't (although you can do it with repeated applications of the Russell construction on a union of everything you want to avoid, with a little work). This is used, for example, to define the elements +oo and -oo so that they are distinct from each other and not in CC.

I don't see a good argument for the Russell class as a definition though. It doesn't actually appear anywhere - ru itself is sort of an endpoint theorem, it never gets used AFAIK.

The reason I saw was historical importance, but this may not be a sufficient reason.

 

Even df-undef is rarely used, and you only need a few key theorems in this area before you have more set-avoiding than you could ever need. If anything was to get a definition, I would suggest something like disjenex, which gives a bit more parametric control over what to avoid and how many elements you want. (I originally formulated that theorem and its corollaries for doing field extensions, so that you can do a construction over another structure, and then re-situate it as a superset of the old structure, which would allow things like the real numbers construction in which NN0 = om.)

I would like to introduce df-riota earlier, but I would prefer to do it by removing the dependence on df-undef entirely. I've argued before on this list about replacing the definition of df-riota to return (/) instead of Undef when it is not unique. It's an out of domain thing anyway, and the empty set is much more likely to make "coincidentally true" theorems, while Undef is almost adversarially avoiding such things.

I'm not sure (/) is a good idea. And the fact that it makes more theorems coincidentally, or accidentally, true is a drawback, to me. I'll look for your earlier posts.

 

[Mario Carneiro]

On Sat, Sep 9, 2017 at 5:20 PM, Benoit <benoit...@gmail.com> wrote:

I would like to introduce df-riota earlier, but I would prefer to do it by removing the dependence on df-undef entirely. I've argued before on this list about replacing the definition of df-riota to return (/) instead of Undef when it is not unique. It's an out of domain thing anyway, and the empty set is much more likely to make "coincidentally true" theorems, while Undef is almost adversarially avoiding such things.

I'm not sure (/) is a good idea. And the fact that it makes more theorems coincidentally, or accidentally, true is a drawback, to me. I'll look for your earlier posts.

Now this is a hard thing to explain. It is well known that ZFC has lots of "junk" theorems, that is, theorems where the inputs are not well typed, and so say something meaningless, but are nevertheless provable because you were forced to make some concrete choices for the definitions of things, like function value out of domain. After you've used ZFC for a while, you recognize that these things exist, but don't actually get in your way or matter much at all. At least, *most* of the time they don't matter. They start to matter when you realize that one application of junk theorems is making theorems have fewer hypotheses. For a system like ours where all preconditions are explicit, this is a big gain.

Even type theory, which was invented *specifically for avoiding junk theorems*, fought this demon and lost in some places, specifically division by zero. Most of the type theory systems I know, like Isabelle, Coq, and Lean, made the deliberate choice to totalize the division function so that x / 0 = 0, because it's just more convenient. Ironically, Metamath is one of the few systems that bucks this trend, and properly states that division is undefined at zero. For example, 1/(1/x) = x is true for x =/= 0, but is "coincidentally" true for x = 0 if you define 1/0 = 0, which saves you having to prove that x =/= 0 when applying this theorem. Now you can argue that the real mathematical content of the theorem needs x =/= 0, but if you can save a tiny bit of effort by skipping this subgoal which is almost certainly provable in whatever context you've applied the theorem, but needs work anyway, then it makes the whole system just that little bit easier to work with.

In junk land, it is better if everything evaluates to a single object when it is junk, because this makes equalities more likely provable when terms are undefined (and equalities are of course extremely common things to want to prove). For example, associativity is provable without assumptions (addasspi). One place where adding assumptions makes things disproportionately complicated is substitution hypotheses. Many theorems like grpass take hypotheses like "|- .+ = ( +g ` G )", intended for direct substitution if you have it and proof by eqid if you don't, but if you have a proof of "( ph -> myplus = ( +g ` G ) )" which has hypotheses, then you have to use eqid and then post substitute into the theorem, which is a lot more work. This puts a pressure on being able to prove such theorems with no hypotheses if possible. grpidval is a place where I deliberately avoided df-riota and used df-iota instead for precisely this reason - you can't prove grpidval without the assumption that the G exists otherwise. Check out 0g0 and its uses for more examples of "junk theorems" in action. (Incidentally, using the Russell definition, ( Undef ` (/) ) = (/) rather than the current { (/) }, so some of these theorems might still be recoverable.)

Now you can try to be a purist and argue that none of this matters for real mathematics, and it is better to just stay in the fragment where everything is well typed, but in my view this is just needlessly hobbling yourself unless you have a mechanism to ensure that you really are being "pure" - "mostly pure" is not pure at all. Type theory does this, and frankly I don't think it actually helped, but ZFC trying to be type theory should not extend beyond a "gentleman's agreement" level of enforcement.

Mario

[David A. Wheeler]

On September 9, 2017 6:43:23 PM EDT, Mario Carneiro <di....@gmail.com> wrote:
>Now this is a hard thing to explain. It is well known that ZFC has lots
>of
>"junk" theorems, that is, theorems where the inputs are not well typed,
>and
>so say something meaningless, but are nevertheless provable because you
>were forced to make some concrete choices for the definitions of

>things...

I think that the metamath scoping statements sometimes make it possible to state things without accidentally using the concrete choices that were made.

...

>division
>by zero. Most of the type theory systems I know, like Isabelle, Coq,
>and
>Lean, made the deliberate choice to totalize the division function so
>that
>x / 0 = 0, because it's just more convenient. Ironically, Metamath is
>one
>of the few systems that bucks this trend, and properly states that
>division
>is undefined at zero.

This is something I really like about set.mm. if you're going to be persnickity, which is fundamental to formal mathematics, simultaneously ignoring a case that every grade-schooler knows is absurd. I understand why they do it, but I still prefer the clarity that is done here.


--- David A.Wheeler

[Benoit]

Mario, your comments are exactly to the point. We working mathematicians don't like junk theorems ;) and mathematical thinking is fundamentally typed. That's why I want to avoid junk / accidentally true theorems. And the phrase "x \in \R implies 1/(1/x) = x" bothers me (I would have removed points to my students for that!). As you say, as we add layers of abstraction, we rapidly encounter fewer junk theorems, but still. I'm afraid I would have liked to enforce something beyond a gentleman's agreement, to use your words!

Anyway, there was an interesting discussion a few years ago on this topic (the first three answers are interesting):
https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems

[Mario Carneiro]

On Sat, Sep 9, 2017 at 8:33 PM, Benoit <benoit...@gmail.com> wrote:

Mario, your comments are exactly to the point. We working mathematicians don't like junk theorems ;) and mathematical thinking is fundamentally typed. That's why I want to avoid junk / accidentally true theorems.

Note that the second statement doesn't follow from the first, depending on what you mean by "avoid". If you mean "avoid stating", I'm 100% on board. If you mean "make my definitions so that as many junk theorems as possible turn out false" I will be annoyed. The idea is that on a given day you will have one of two mentalities on junk theorems: "I don't care if they are true or false, they don't matter", or "it would be nice if it was true, because then I could eliminate this inessential assumption". You never want a junk theorem to be false, so it's best to set things up so that as many turn out true as you can manage, for those people on those days that *do* care about them.

 

And the phrase "x \in \R implies 1/(1/x) = x" bothers me (I would have removed points to my students for that!). As you say, as we add layers of abstraction, we rapidly encounter fewer junk theorems, but still. I'm afraid I would have liked to enforce something beyond a gentleman's agreement, to use your words!

Also, don't forget that if you are in "absolutely no junk" mode, there is nothing stopping you from using the theorem x e. RR -> 1/(1/x) = x only when you have the assumption x =/= 0 floating around. Hell, you can trivially prove the more "comfortable" version of the theorem by weakening if you don't want to see the junk. But there is no way to truly excise it from the language, so to some degree you just have to live with the fact that sometimes you have to worry about this stuff. The math overflow question mentions a programming analogy, which I think is spot-on. If you are writing a library for C, you will occasionally do "weird" things like bit shift a float for specialized purposes. Most users don't need to break that abstraction, but it *is* useful to have the ability to do so, and of course you have to break an abstraction while you're building it (hmm, that's a mixed metaphor).

Mario

[Norman Megill]

On Saturday, September 9, 2017 at 8:33:05 PM UTC-4, Benoit wrote:

Mario, your comments are exactly to the point. We working mathematicians don't like junk theorems ;) and mathematical thinking is fundamentally typed. That's why I want to avoid junk / accidentally true theorems. And the phrase "x \in \R implies 1/(1/x) = x" bothers me (I would have removed points to my students for that!). As you say, as we add layers of abstraction, we rapidly encounter fewer junk theorems, but still. I'm afraid I would have liked to enforce something beyond a gentleman's agreement, to use your words!

Anyway, there was an interesting discussion a few years ago on this topic (the first three answers are interesting):
https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems

That's an interesting read.  In set.mm, we more or less do this:

1.  For ordinal numbers, we treat them as if they _are_ their definitions, leading to examples like 1o e. 2o, and we exploit such "junk" theorems freely.  Books about ordinals tend to do this also, e.g. Enderton's Elements of Set Theory.  Indeed, it seems that von Neumann ordinals were invented so that such "junk" theorems can be used as shortcuts.  Although we call the finite ordinals om the "natural numbers" in keeping with literature terminology, it is clear that these aren't the natural numbers NN0 used in ordinary math (they can't be mixed with real numbers in expressions, for example).

2. For complex numbers, we isolate their construction from their properties by restricting our use to their axioms and disallowing direct use of their construction.  As long as we are careful with definitions, there are very few "junk" theorems.  For example, we could protect df-div from casual usage of the out-of-domain case by restricting usage to divval only.  In a couple of cases in the past, I rejected omitting an "A e. CC" antecedent that became redundant due to "junk" behavior".

3. For structures such as groups, rings, etc., I think their definitions keep them relatively pure.  For example, there is nothing in the definition of a group that lets us say anything at all about what a group element contains as a set.  There may be some relatively minor out-of-domain behavior that could be exploited in principle but I think it's very rare that we do so, if we do it at all (barring things like fvex, which I think is a very mild "junk" exploitation).  To some extent the structure definition itself typically discourages exploitation of things like ndmfv because we normally do not exclude (/) from the carrier set of a structure.

So I would say we've done a pretty good job at exploiting junk where it's appropriate (ordinals) and avoiding it essentially completely for structures, with complex numbers somewhere in between.

 

On Sunday, September 10, 2017 at 12:43:25 AM UTC+2, Mario Carneiro wrote:

On Sat, Sep 9, 2017 at 5:20 PM, Benoit <benoit...@gmail.com> wrote:

I would like to introduce df-riota earlier, but I would prefer to do it by removing the dependence on df-undef entirely. I've argued before on this list about replacing the definition of df-riota to return (/) instead of Undef when it is not unique. It's an out of domain thing anyway, and the empty set is much more likely to make "coincidentally true" theorems, while Undef is almost adversarially avoiding such things.

I agreed with Mario on this point (wherever those earlier posts were) and would also think it would be good to remove Undef.  For one thing, it isn't consistent with the pattern in df-ral, df-rex, df-rmo, etc. that simply abbreviates the non-restricted version.  It also has complexity that makes it harder to understand - you have to go back to df-undef, and understand the theorems that prevent Undef from belonging to the carrier set.  We don't use Undef in any other definitions (except implicitly in df-pnf and df-mnf, where it is unavoidable)

Most importantly, though, this out-of-domain behavior simply isn't used in practice, just like we don't normally use the out-of-domain behavior of other functions beyond "junk" tricks in early set theory.  When I created df-riota, my thought was that it would provide significant savings by letting use use "riota ... e. A" instead of "E! x e. A..." as an antecedent.  In fact I believe this is used in only 2 theorems about posets.  After I did those, I abandoned doing it this way because it was confusing to read:  you had to know the definition of riota intimately in order to understand the theorem, whereas "E! x e. A... ->" makes the theorem immediately readable to anyone who understand the concept of "the unique element in A such that..."  In the end, it didn't come anywhere near making proofs significantly shorter and may have made them longer.  I consider it a failed experiment.

I have also considered removing Undef entirely simply because it isn't used much, it doesn't really pay off, and it encourages the use of "junk" behavior.  I think that all uses would essentially disappear if we take it out of df-riota.

Norm

[Benoit]

On Sunday, September 10, 2017 at 3:57:06 PM UTC+2, Norman Megill wrote:

That's an interesting read.  In set.mm, we more or less do this:

1.  For ordinal numbers, we treat them as if they _are_ their definitions, leading to examples like 1o e. 2o, and we exploit such "junk" theorems freely.  Books about ordinals tend to do this also, e.g. Enderton's Elements of Set Theory.  Indeed, it seems that von Neumann ordinals were invented so that such "junk" theorems can be used as shortcuts.  Although we call the finite ordinals om the "natural numbers" in keeping with literature terminology, it is clear that these aren't the natural numbers NN0 used in ordinary math (they can't be mixed with real numbers in expressions, for example).

Yes, that's a nice example. Actually, I think the definition 0o = (/) and the use of 0o when we think of the ordinal (in the section on Ordinal arithmetic) would make the statements look nicer.

2. For complex numbers, we isolate their construction from their properties by restricting our use to their axioms and disallowing direct use of their construction.  As long as we are careful with definitions, there are very few "junk" theorems.  For example, we could protect df-div from casual usage of the out-of-domain case by restricting usage to divval only.  In a couple of cases in the past, I rejected omitting an "A e. CC" antecedent that became redundant due to "junk" behavior".

By "protecting", you mean adding a "new usage is discouraged", is that correct? In the analogy with programming in the mathoverflow answer, this would be a kind of encapsulation, like the "private" keyword in java, if I'm not mistaken. I don't have enough experience with metamath to know if that would be good or not, but the idea is appealing.

[David A. Wheeler]

On September 10, 2017 12:53:34 PM EDT, Benoit <benoit...@gmail.com> wrote:
>By "protecting", you mean adding a "new usage is discouraged", is that
>correct? In the analogy with programming in the mathoverflow answer,
>this
>would be a kind of encapsulation, like the "private" keyword in java,
>if
>I'm not mistaken.

I don't know if that is what he had in mind, but that is certainly what I have in mind. Being able to say that new usage is discouraged is useful. It means that you can devise arbitrary encapsulations of properties, allowing reuse of the properties, while simultaneously hiding the details of the construction. It also means that if you really do need to access something else, you are warned but you can still do it.

I don't recall the terminology being used often in this forum, but I like to think of these hidden constructions as a "witness". That is, the witness shows an example of how one might construct something, and the "new usage is discouraged" marking prevents arbitrary theorems from depending on the unnecessary details.

Of course, that means that if you really do want to break the encapsulation you can easily do so. But at least it cannot be accidental, and it is something that is immediately flagged for others to review.


--- David A.Wheeler

[Raph Levien]

I have pretty strong feelings about the way this should be handled, and have tried to prototype it in Ghilbert, but getting it right is not easy. I feel there should be a module structure, with clearly defined interfaces at the modules. The "axioms for complex numbers" (http://us.metamath.org/mpegif/mmcomplex.html#axioms) are a pretty good look at what such an interface would look like.

Then, theorems proved using the interface would be _portable_ to not just one, but potentially multiple constructions, as long as they can satisfy the interface.

In the case of the ordinals, A ⊆ succ(A) etc could be part of an interface designed to make such theorems convenient. Of course, the construction would need to have a strong enough set theory to be able to provide this interface - certainly not trivial for axiomatic systems other than ZFC, but probably doable.

I'm still very much wrestling with the question of how to handle types in such interfaces. I think the most general approach would be to have a predicate that says that the value is "in domain," which corresponds loosely to a typing judgment, and which concrete interpretation in a ZFC world would be element in the set. I'll use the type notation ":" but with some uneasiness.

For functions of type ℂ → ℂ (such as, say, unary negation), there would be inference rules of the form from φ → A : ℂ deduce φ → -A : ℂ. However, for division, it would look more like:

φ → A : ℂ

φ → B : ℂ

φ → B ≠ 0 → (A / B) : ℂ

This can be satisfied in all reasonable constructions of divison - those in which the result is the empty set, those in which it's 0, those in which it's guaranteed to be some complex number but not specified which one (the most common behavior in HOL, for which this is the behavior of epsilon choice with an everywhere-false predicate), those in which there's a designated "bottom" value of a domain, etc.

A proof which is written in terms of this interface would be portable across all such constructions. Thus I think the technique has strong potential to get rid of "junk theorems".

To me, proving the negation of A / 0 : ℂ is a junk theorem of a different sort, because it can't be satisfied in logics that prefer functions to be totally typed, notably HOL.

Again, these are my feelings of how such things should be, I don't at the moment have a concrete proposal of how to get there.

Raph

[Thierry Arnoux]

In this sense, should we consider as "junk theorems" - and therefore tag
them as "new usage is discouraged" - those which use the fact that the
value of a function is (/) outside of its domain?

I'm thinking about ~ fvprc , ~ fvrn0, ~ ndmfv, ~ fv01, ~ nfunsn, etc.
Those theorems are actually used a lot throughout set.mm. What shall I
think about those theorems which are derived from them?

[Mario Carneiro]

On Mon, Sep 11, 2017 at 11:54 AM, Thierry Arnoux <thierry...@gmx.net> wrote:

In this sense, should we consider as "junk theorems" - and therefore tag them as "new usage is discouraged" - those which use the fact that the value of a function is (/) outside of its domain?

I think - I'm not sure how practicable this is, but it sounds like a reasonable idea. Even if there are a lot of theorems using these newly discouraged theorems, it is only a one-time change to the discouraged file, as long as the list of theorems doesn't continue to grow (this is the practicability assumption).

I'm thinking about ~ fvprc , ~ fvrn0, ~ ndmfv, ~ fv01, ~ nfunsn, etc. Those theorems are actually used a lot throughout set.mm. What shall I think about those theorems which are derived from them?

One way to think of this is that "new usage is discouraged" really means "new usage is controlled". The usage of a discouraged theorem does not "poison" that theorem in its derivatives - this is not the purpose of the discouraged marker. It only creates an interface barrier, and adds an extra level of review to the admission of proofs that circumvent that barrier. If a theorem uses ndmfv, it is up to the author or the maintainers to determine if the theorem should also be discouraged, but it does not necessarily follow. For example, I would not discourage f0cli or cardon even though it uses ndmfv.

Mario

 

On 11/09/2017 02:53, David A. Wheeler wrote:

On September 10, 2017 12:53:34 PM EDT, Benoit <benoit...@gmail.com> wrote:

By "protecting", you mean adding a "new usage is discouraged", is that
correct? In the analogy with programming in the mathoverflow answer,
this
would be a kind of encapsulation, like the "private" keyword in java,
if
I'm not mistaken.

I don't know if that is what he had in mind, but that is certainly what I have in mind. Being able to say that new usage is discouraged is useful.  It means that you can devise arbitrary encapsulations of properties, allowing reuse of the properties, while simultaneously hiding the details of the construction. It also means that if you really do need to access something else, you are warned but you can still do it.

I don't recall the terminology being used often in this forum, but I like to think of these hidden constructions as a "witness".  That is, the witness shows an example of how one might construct something, and the "new usage is discouraged" marking prevents arbitrary theorems from depending on the unnecessary details.

Of course, that means that if you really do want to break the encapsulation you can easily do so. But at least it cannot be accidental, and it is something that is immediately flagged for others to review.


--- David A.Wheeler

[Stefan O'Rear]

On Mon, Sep 11, 2017 at 12:45 PM, Mario Carneiro <di....@gmail.com> wrote:
>
>
> On Mon, Sep 11, 2017 at 11:54 AM, Thierry Arnoux <thierry...@gmx.net>
> wrote:
>>
>> In this sense, should we consider as "junk theorems" - and therefore tag
>> them as "new usage is discouraged" - those which use the fact that the value
>> of a function is (/) outside of its domain?
>
>
> I think - I'm not sure how practicable this is, but it sounds like a
> reasonable idea. Even if there are a lot of theorems using these newly
> discouraged theorems, it is only a one-time change to the discouraged file,
> as long as the list of theorems doesn't continue to grow (this is the
> practicability assumption).

If you make this rule, I will ignore it.

-s

[Cris Perdue]

On Mon, Sep 11, 2017 at 7:41 AM, Raph Levien <raph....@gmail.com> wrote:

I have pretty strong feelings about the way this should be handled, and have tried to prototype it in Ghilbert, but getting it right is not easy. I feel there should be a module structure, with clearly defined interfaces at the modules. The "axioms for complex numbers" (http://us.metamath.org/mpegif/mmcomplex.html#axioms) are a pretty good look at what such an interface would look like.

Then, theorems proved using the interface would be _portable_ to not just one, but potentially multiple constructions, as long as they can satisfy the interface.

I am very much of this view also, numbers being truly independent of any particular construction from sets.

 

In the case of the ordinals, A ⊆ succ(A) etc could be part of an interface designed to make such theorems convenient. Of course, the construction would need to have a strong enough set theory to be able to provide this interface - certainly not trivial for axiomatic systems other than ZFC, but probably doable.

I'm still very much wrestling with the question of how to handle types in such interfaces. I think the most general approach would be to have a predicate that says that the value is "in domain," which corresponds loosely to a typing judgment, and which concrete interpretation in a ZFC world would be element in the set. I'll use the type notation ":" but with some uneasiness.

As a thought experiment, have you considered using a predicate notation for this predicate? The question may seem a bit arch, but I wonder if you feel any conceptual issues with use of a predicate. 

 

For functions of type ℂ → ℂ (such as, say, unary negation), there would be inference rules of the form from φ → A : ℂ deduce φ → -A : ℂ. However, for division, it would look more like:

φ → A : ℂ

φ → B : ℂ

φ → B ≠ 0 → (A / B) : ℂ

This can be satisfied in all reasonable constructions of divison - those in which the result is the empty set, those in which it's 0, those in which it's guaranteed to be some complex number but not specified which one (the most common behavior in HOL, for which this is the behavior of epsilon choice with an everywhere-false predicate), those in which there's a designated "bottom" value of a domain, etc.

A proof which is written in terms of this interface would be portable across all such constructions. Thus I think the technique has strong potential to get rid of "junk theorems".

The thing I see missing from these "axioms" for division is that they do not rule out the possibility that A / 0 is a complex number. I find this to be important in showing properly that certain problems (e.g. equations) do not have solutions.

 

To me, proving the negation of A / 0 : ℂ is a junk theorem of a different sort, because it can't be satisfied in logics that prefer functions to be totally typed, notably HOL.

I would much prefer a description other than "junk theorem" for the kind of issue this raises. I think you are saying that the type systems of HOL provers inherently limit the type of A / 0 to be ℂ. I have seen some defense of A / 0 = 0, but it is certainly counter to tradition and seems to me to be "making a virtue of necessity".

As you are probably aware, a claim to fame of IMPS is that within the HOL approach it provides support for "undefinedness". For what it's worth, it turns out that a very IMPS-like system can be built on the same logical foundations, but with a bottom element in place of predicates for defined/undefined. This has advantages such as simplifying the definition of equality of partial functions (all "undefined" values are equal to each other), among others.

I am interested in discussing options here further, though I'm not sure it is entirely on-topic for this list.

[Raph Levien]

You mean something like ℂ(x) rather than x: ℂ or x ∈ ℂ? I'm open to it. I've also considered something like a check-mark, especially when the type is clear from context. (and now I'm referring to "type" without defining it more precisely, oh dear).

You're right, I take back calling things like the assertion that ¬ (x/0 : ℂ) is a "junk theorem." A more precise way of saying what I meant is that it's an overly strong assertion in many contexts, and it should be possible to express the fact that proofs don't depend on it, so they can be more easily ported.

Having a domain with an explicit bottom value seems like it would be useful in a lot of contexts. I've seen a presentation by Kahan on the inclusion of infinity in floating point, where having it in a continued fraction causes no difficulty at all, and avoids having to special-case it. So my personal feeling is that this should also be a (well-supported) choice, but by no means a requirement.

Happy to have this discussion on another thread, but I personally feel it's relevant to the "Undef" issue originally brought up. It's a subtle point and people have very different responses to it; it seems worthwhile bringing up things like IMPS so we can consider the pros and cons.

Raph

Raph

[Norman Megill]

On Monday, September 11, 2017 at 4:00:10 PM UTC-4, Stefan O'Rear wrote:

On Mon, Sep 11, 2017 at 12:45 PM, Mario Carneiro  wrote:
>
>
> On Mon, Sep 11, 2017 at 11:54 AM, Thierry Arnoux 

> wrote:
>>
>> In this sense, should we consider as "junk theorems" - and therefore tag
>> them as "new usage is discouraged" - those which use the fact that the value
>> of a function is (/) outside of its domain?
>
>
> I think - I'm not sure how practicable this is, but it sounds like a
> reasonable idea. Even if there are a lot of theorems using these newly
> discouraged theorems, it is only a one-time change to the discouraged file,
> as long as the list of theorems doesn't continue to grow (this is the
> practicability assumption).

If you make this rule, I will ignore it.

I agree.  I think we should just acknowledge that some things in set.mm are not "pure" in some sense and move on, rather than impose draconian restrictions that will slow us down and increase the size of proofs.

I haven't done an analysis, but I would guess the most commonly used junk theorem is fvex and its consequences (ovex etc.).  Imagine if we had to avoid those!

The next most common usage of junk theorems is probably the elimination of sethood hypotheses (A e. _V).  I think this is a good thing when it can be done because it makes proofs shorter and removes an unnecessary distraction that most mathematicians don't care about, and I always encourage it.

After that, a common use is to eliminate other hypotheses.  Looking at the last application of ndmfv, it is used to let dihvalrel say

( ( K e. HL /\ W e. H ) -> Rel ( I ` X ) )

instead of

( ( K e. HL /\ W e. H /\ X e. dom I ) ->  Rel ( I ` X ) ) )

which may offer significant proof size savings in future uses of this theorem, since we don't have to prove X e. dom I.   This is more controversial than removal of a sethood hypothesis, but I usually tolerate it when it makes proofs shorter, and I don't see that it seriously detracts from understanding the theorem.  Shorter and easier proofs are a strong motivation.

The only place I would not like to see such hypothesis elimination is in the early complex number development, which has a different audience, and we want to keep things as "pure" as possible.  As I mentioned, I once rejected a proposal to eliminate "A e. CC" (actually "A e. RR" now that I think of it, in an early theorem about ordering that used out-of-domain behavior of relations I think).  But in advanced proofs I don't think I would reject this.

The theorem 1div0, 1/0=(/), is a borderline case that I would ordinarily reject, but it serves to satisfy curiosity (especially in light of 1/0=0 assumed by some proof languages).  I will add "(New usage is discouraged.)" to this theorem.

A theorem I would definitely reject is "1/0 e/ CC", which would need the construction-dependent 0ncn.  At least one real number construction (Levy) does use (/) as the number 0.

Aside from the special case 1div0, I think the right approach for division is to be agnostic about division by 0, which can be accomplished by using divval as the starting point and avoiding direct reference to the definition.  I think the bulk of theorems about division honor this.  I will add "(New usage is discouraged.)" to df-div to prevent accidental abuse.

To summarize:   we don't discourage all usage of junk theorems, but we temper it with some common sense.  Using junk theorems to eliminate sethood hypotheses is always OK.  Using them to eliminate other hypotheses is usually OK, especially if shorter and easier proofs result.  Exploiting construction-dependent facts about complex numbers is never OK.  Proving something normally considered nonsensical like 1/0 = (/) is hardly ever OK, except when explicitly intended as a curiosity (as the comment of 1div0 makes very clear).

I addressed our current practice above and don't expect that it will change much.  A potentially difficult problem is portability to other proof languages, that may expect "complex numbers" to be a pure, self-contained module.  However, beyond trivial theorems, we need to import essentially all of set theory into complex numbers anyway.  In principle, all of our "impure" usage can be cleaned up (although we have to agree on what is "pure" - is fvex allowed?), but it would be a thankless task and result in a set.mm burdened with theorems having many more hypotheses as well as much longer proofs in many cases.  Personally I think that would make it uglier and harder for the reader to follow.

Norm

[Norman Megill]

On Monday, September 11, 2017 at 5:12:22 PM UTC-4, Cris wrote:

The thing I see missing from these "axioms" for division is that they do not rule out the possibility that A / 0 is a complex number. I find this to be important in showing properly that certain problems (e.g. equations) do not have solutions.

What is an example of where this would arise?  I have never heard of this.  How would other provers solve such a problem since for some of them A/0 is a complex number?

Norm

[Cris Perdue]

OK, well first let me admit I'll be preferring to think of the real numbers as the domain, as I am much more comfortable there than with the complex numbers, sorry. I know division by zero is a case where the issue occurs for both domains.

The issue arises for one thing in basic textbook mathematics. Here is a nice clear example from a well-known online source: https://www.khanacademy.org/math/algebra/introduction-to-algebra/division-by-zero/v/why-dividing-by-zero-is-undefined. The main text of the page is:

As much as we would like to have an answer for "what's 1 divided by 0?" it's sadly impossible to have an answer. The reason, in short, is that whatever we may answer, we will then have to agree that that answer times 0 equals to 1, and that cannot be true, because anything times 0 is 0.

In a basic "real-world" problem with speed and distance and time, when the speed turns out to be zero, the answer to "How long will it take?" is "Sorry, not at any time." (Never mind the cases where you are going in the wrong direction!)

In the world of Metamath, interactive theorem provers and the like, Mario Carneiro reported on this list a conversation with a member of the Mizar team on division by zero. (https://groups.google.com/forum/#!searchin/metamath/mizar$20zero$20carneiro%7Csort:date/metamath/VAGNmzFkHCs/X1H3n5C6B4cJ)

The claim was made that Mizar defines x / 0 = 0, and not to fit the type system, but on principle, and Mario seemed to find merit in this in simplifying numerous math identities.

But clearly that does not mean that if you are trying to get somewhere at zero miles per hour, you are already there! I mean, unless indeed you are already there. (!!!)

In the world of automated theorem proving, the IMPS system was built from the ground up to handle partial functions routinely, and distinguishes for example between "undefined" values and (normal) numbers.  IMPS is in the simple type theory family, based on Q0, with fundamental support for partial functions.

For other provers such as the well-known members of the HOL family or Mizar, my personal sense is that there is an unspoken expectation in the community that the users are big boys and girls who know enough to use the system and its math thoughtfully and with care.

-Cris

 

Norm