Handling "undefined terms"

[Benoit]

As promised at the end of https://groups.google.com/d/topic/metamath/yzQnexbXv-8/discussion , I'm going to list a few ways I can think of to avoid "nonsensical", or "junk" theorems in set.mm.  This is not a proposal to change anything in set.mm, at least for the moment.  The only aim of this post is to try and summarize different ways of handling "undefined" cases, and of course to suscitate comments and suggestions.  I may be a bit obsessed with it, since I started discussions on this topic earlier: https://groups.google.com/d/topic/metamath/GQmelsKtaWQ/discussion and https://groups.google.com/d/topic/metamath/0LzmdrbW_yI/discussion

For the sake of concreteness, I'm going to consider a simple example, Russell's definition description binder iota.  Recall that ( iota x ph ) is meant to be "the x such that phi" (where phi typically depends on x).  In the current version of set.mm, it is defined as follows:

cio $a class ( iota x ph ) $.
${
  $d y x $.  $d y ph $.
  df-iota $a |- ( iota x ph ) = U. { y | { x | ph } = { y } } $.
$}

Therefore, it does not precisely mean "the x such that phi": it means it only when there exists a unique x such that phi, else it is the empty set, as proved in ~iotanul.

The problem with this is that for instance, you could prove in set.mm that "the even prime number different from 2 is equal to the odd prime number".  Of course, not literally: you prove its formal version, and then, using blindly the comment that "( iota x ph ) is the only x such that phi", you deduce the above nonsensical sentence.  (Similarly, most undefined things evaluate to the empty set in set.mm, so you could prove that "the tangent space at the square root function of the number 2 is equal to the logarithm of 0", etc.)

To repeat myself: the formal expression ( iota x ph ) is never nonsensical.  Rather, it's reading this expression as "the only x such that phi" which may cause confusions.

Now I'm going to list several ways to avoid theorems of this kind, with pros and cons, from the more strict to the more lax:


1. Forbid the mere writing of nonsensical terms.

Here, this would amount to changing cio as follows:
${
  cio.1 $e |- E! x ph $.
  cio $a |- class ( iota x ph ) $.
$}
and either leaving df-iota unchanged or writing it as in the second proposal.

Pros: you can't even write nonsensical terms, so you can't prove anything about them.
Cons: this would complicate a lot automation tools and type inference, and proofs would be harder since "floating hypotheses" could not be easily automated anymore.  By the way, I think this is currently rejected by mmj2.  I am not clear with all the consequences, so maybe Mario could make this more precise.


2. Do not define undefined terms.

Here, you would leave cio unchanged, but change df-iota as follows:
${
  $d y x $.  $d y ph $.
  df-iota.1 $e |- E! x ph $.
  df-iota $a |- ( iota x ph ) = U. { x | ph } $.
$}

Pros: if you can't prove |- E! x ph, then ( iota x ph ) is some undefined class, so you can prove about it only things true for all classes, like that it is equal to itself, that it contains the empty set, etc.  But not much else.  Bonus: this definition is simpler to understand (that this simpler expression is equivalent to the current version is proved in iotauni).
Cons: in the standard terminology, this is not a real definition, meaning that it does not provide a "definitional extension" of, say, ZF.  It makes proofs harder.  Compared to 1., you can still write "nonsensical things".


3. State the current definition, but discourage its use and only use a weakened form.

Here, you would add to df-iota the "New usage is discouraged." tag, and then you would prove from it the following:
${
  $d y x $.  $d y ph $.
  dfiota.1 $e |- E! x ph $.
  dfiota $p |- ( iota x ph ) = U. { y | { x | ph } = { y } } $= ( df-iota ) ABCE $.

$}

and this should be the only use of df-iota.

Pros: you maintain a "definitional extension", but you still have the advantages of 2.
Cons: Compared to 2., one can still use discouraged statements, although using them unintentionally is less plausible.  Compared to the current state, proofs are longer since you will always have to prove |- E! x ph before using df-iota, and this requirement will propagate to many theorems.  But I think that it's actually a good thing: always prove that you are in the conditions of validity of the theorems you use.


3bis. Variants of 3.

If you are a bit lazy, then you might allow the most basic properties of iota to be proved without the unique existence property, for instance iotabidv, iotabii.  What is important is that iotanul not be provable without infringing discouragement tags.

Pros: compared to 3., shorten some proofs.
Cons: one can still consider iotabidv and iotabii as nonsensical in general.


4. Current state

Pros: this makes proofs easier, especially having iotanul and iotaex.
Cons: it is possible to prove "nonsensical theorems".  Again, the formal statements make perfect sense, it is just the translation back into plain English that can contain subtle errors.


Conclusion

With formal proofs like in set.mm, there is no risk of nonsense in the formal statements (assuming no bug and ZF is consistent).  But there is still a risk: it has been shifted to the problem of understanding what a statement really means.  Of course, the examples I gave above are very blunt, but with definitions piling up one on top of the other, the risk increases.  For instance, taking sqr2irr, I am confident that |- ( sqr ` 2 ) e/ QQ, but does it really mean that the square root of 2 is irrational?  To be sure, I have to check precisely the set.mm-definitions of all these terms (sqr, function application, 2, e/, QQ), and the definitions these definitions rely on, etc.  So definitions should be as simple as possible.  (Nothing is new, here, and Norm explains it well in the Metamath book.)  I find the above dfiota is simpler to understand than the current df-iota, because one does not have to keep in his head the special case when there is no unique existence.

It would be a lot of work to modify existing definitions, but maybe for future definitions, Proposal 3. could be a good compromise ?

Benoît

[Mario Carneiro]

On Sat, Jan 11, 2020 at 11:24 AM Benoit <benoit...@gmail.com> wrote:

1. Forbid the mere writing of nonsensical terms.

Here, this would amount to changing cio as follows:
${
  cio.1 $e |- E! x ph $.
  cio $a |- class ( iota x ph ) $.
$}
and either leaving df-iota unchanged or writing it as in the second proposal.

Pros: you can't even write nonsensical terms, so you can't prove anything about them.
Cons: this would complicate a lot automation tools and type inference, and proofs would be harder since "floating hypotheses" could not be easily automated anymore.  By the way, I think this is currently rejected by mmj2.  I am not clear with all the consequences, so maybe Mario could make this more precise.

This means that "class" is no longer context free, and hence parsing in general becomes undecidable. It would be rejected by mmj2, and would also be rejected by the formalism of "Models for Metamath", which separates typecodes into two classes, logical typecodes and syntax typecodes, and requires that variables only range over syntax typecodes, and requires that the parsing problem for syntax typecodes be context-free by demanding that term constructors have no hypotheses or disjoint variable conditions. Since the notion of "grammatical database" from the "Models for Metamath" paper has been baked into MM0, it will not even let you write this down.

To give an example of how having variables ranging over a non-context-free class can get you into trouble, suppose we had a variable

wthm $f |- THM $.

That is, THM is a variable that ranges only over wffs that are true. Then if there was a theorem

foo $p |- ( ph -> THM ) $= ... $.

(which is easy to prove), then we could write a one step proof like

qed::foo |- ( T. -> RH )

 

and now the parser is being expected to prove the Riemann Hypothesis.

From the point of view of general metamath, this is fine, of course; there is no problem with verifying a theorem like this, but it blurs the distinction between syntax proofs and general proofs.

You can go further in the syntax that you consider automatically derivable; type systems like simple type theory of dependent type theory push quite a bit more computation into this "well formedness" judgement. When you use a set.mm tuned proof assistant like mmj2 on a database like hol.mm, it generally doesn't capture this, so you have to prove all the typing conditions by hand, but an algorithm that is expecting these proof forms will be able to automate them away.

Even in a more advanced type system like Lean, this syntax form would not be allowed, because unique existence of a predicate is not decidable. However, you could have a syntax constructor that takes a proof of uniqueness as an additional argument, so that it is explicitly in the term. This requires a term syntax for proofs, which set.mm does not support (but another database could).

2. Do not define undefined terms.

Here, you would leave cio unchanged, but change df-iota as follows:
${
  $d y x $.  $d y ph $.
  df-iota.1 $e |- E! x ph $.
  df-iota $a |- ( iota x ph ) = U. { x | ph } $.
$}

Pros: if you can't prove |- E! x ph, then ( iota x ph ) is some undefined class, so you can prove about it only things true for all classes, like that it is equal to itself, that it contains the empty set, etc.  But not much else.  Bonus: this definition is simpler to understand (that this simpler expression is equivalent to the current version is proved in iotauni).
Cons: in the standard terminology, this is not a real definition, meaning that it does not provide a "definitional extension" of, say, ZF.  It makes proofs harder.  Compared to 1., you can still write "nonsensical things".

This is not sufficient; you actually want the axiom to be

${
  $d y x $.  $d y ph $.

  df-iota $a |- ( E! x ph -> ( iota x ph ) = U. { x | ph } ) $.
$}

because you will often only be able to prove the side condition in some context. This will be rejected by the definition checker, but the main theoretical reason to reject this axiom is that it breaks equality - the metatheorem ( x = y -> P(x) = P(y) ) fails to hold if definitions don't unfold without some assumptions. That is, iotabidv is no longer provable and must be added as an axiom.

3. State the current definition, but discourage its use and only use a weakened form.

Here, you would add to df-iota the "New usage is discouraged." tag, and then you would prove from it the following:
${
  $d y x $.  $d y ph $.
  dfiota.1 $e |- E! x ph $.
  dfiota $p |- ( iota x ph ) = U. { y | { x | ph } = { y } } $= ( df-iota ) ABCE $.

$}

and this should be the only use of df-iota.

Pros: you maintain a "definitional extension", but you still have the advantages of 2.
Cons: Compared to 2., one can still use discouraged statements, although using them unintentionally is less plausible.  Compared to the current state, proofs are longer since you will always have to prove |- E! x ph before using df-iota, and this requirement will propagate to many theorems.  But I think that it's actually a good thing: always prove that you are in the conditions of validity of the theorems you use.

This is basically the current situation. As long as the usage of well formedness conditions is a mere "gentleman's agreement" that can be circumvented when necessary, there are no theoretical problems. The conventions on what is considered "undefined" vary depending on the syntax. ( iota x ph ) when the argument is not unique is one example, as is function value out of domain in most (but not all) cases, as well as division by zero.

3bis. Variants of 3.

If you are a bit lazy, then you might allow the most basic properties of iota to be proved without the unique existence property, for instance iotabidv, iotabii.  What is important is that iotanul not be provable without infringing discouragement tags.

I will note that the reason df-iota has the more complicated definition is not an accident, and it reflects another way to treat undefined terms: make them evaluate to the empty set whenever possible. While not perfect, it makes it a bit more clear when something is undefined, and it has the advantage that it makes more things equal outside their domain which can remove hypotheses when you feel like exploiting junk theorems. The main place where you see this being systematically exploited is in "reverse closure" theorems like "A e. ( F ` B ) -> B e. dom F", which is useful when F is a family of sets. (That may be an odd thing to say since this is set theory so everything is a set, but I think you know what I mean - it's a set even in a type theoretic interpretation.)

 

Pros: compared to 3., shorten some proofs.
Cons: one can still consider iotabidv and iotabii as nonsensical in general.

As I indicated above, it is important for every syntax constructor to satisty equality theorems *unconditionally*. So ( 1 / 0 ) = ( 1 / 0 ) should not be rejected. This is forced on us by the context free term language, and anything else requires a lot more infrastructure (e.g. a type checker) to support without making everything else more painful to use.

 

4. Current state

Pros: this makes proofs easier, especially having iotanul and iotaex.
Cons: it is possible to prove "nonsensical theorems".  Again, the formal statements make perfect sense, it is just the translation back into plain English that can contain subtle errors.

I think this is largely a non-issue. No one does these things deliberately in "real" situations, and I have never seen this happen accidentally, so it's not clear to me what the worry is.

Conclusion

With formal proofs like in set.mm, there is no risk of nonsense in the formal statements (assuming no bug and ZF is consistent).  But there is still a risk: it has been shifted to the problem of understanding what a statement really means.  Of course, the examples I gave above are very blunt, but with definitions piling up one on top of the other, the risk increases.  For instance, taking sqr2irr, I am confident that |- ( sqr ` 2 ) e/ QQ, but does it really mean that the square root of 2 is irrational?  To be sure, I have to check precisely the set.mm-definitions of all these terms (sqr, function application, 2, e/, QQ), and the definitions these definitions rely on, etc.  So definitions should be as simple as possible.  (Nothing is new, here, and Norm explains it well in the Metamath book.)  I find the above dfiota is simpler to understand than the current df-iota, because one does not have to keep in his head the special case when there is no unique existence.

Typing doesn't do anything to save you from reading all the definitions leading to a theorem in order to check correctness. The main place it helps is in preventing proof authors from accidentally writing nonsense by quickly flagging an error, rather than simply causing statements to be unprovable. Once the proof is done, that worry is gone, so it doesn't have to enter the mind of the reader.

I have had a similar conversation about this in Lean, which is on the whole more strictly typed, of course, but contrary to metamath chooses to define x / 0 = 0 (and exploits this equality without any hedging). The key insight is that because this does not affect consistency (it's a definition), one does not have to worry that the proof that sqrt(2) is irrational depends on dividing by zero. You just have to check that the definition of sqrt makes sense (uses no undefined terms) when applied to 2, and in particular actually defines the square root of 2. A type system can help with the first part of that but not the second part.

It would be a lot of work to modify existing definitions, but maybe for future definitions, Proposal 3. could be a good compromise ?

I contend that we already follow proposal 3 except in specific whitelist situations.

Mario

[Benoit]

On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:

qed::foo |- ( T. -> RH )

I don't understand: it looks like you are using foo with the substitutions ph <- T. and THM <- RH, but in order to make the latter substitution, you need to prove that RH has type |- , which means you need to prove it ?

>This is not sufficient; you actually want the axiom to be

> df-iota $a |- ( E! x ph -> ( iota x ph ) = U. { x | ph } ) $.

Indeed, my bad.

> ... ( x = y -> P(x) = P(y) )

Is this really needed unconditionally ? For instance, for division by zero, do we really need |- ( x = y -> 1/x = 1/y ) ? Isn't it enough to have, for instance, |- ( ( x e. CC \ {0} /\ x = y ) -> 1/x = 1/y ) ?

> So ( 1 / 0 ) = ( 1 / 0 ) should not be rejected.

It would not be rejected with proposals 2 and higher, since every class is equal to itself.

> I have had a similar conversation about this in Lean

If it was online, do you have a link ?

> but contrary to metamath [Lean] chooses to define x / 0 = 0 (and exploits this equality without any hedging).

So it considers the "meadow" (a new term for an older concept) associated with the field CC.  Side remark: I prefer the version 1/0 = \infty that I used in ~df-bj-invc.

> The key insight is that because this does not affect consistency (it's a definition)

I don't understand: definitions like this may lead to inconsistencies (for instance, here, you'd better avoid the axiom x x^{-1} = 1).  The theory of meadows is of course consistent, but in general, one has to be careful.  Or you were referring to something more specific ?

> I contend that we already follow proposal 3 except in specific whitelist situations.

I do not see any discouragement tag for df-iota nor even for iotanul. Or is this part of the whitelist ?  Could we document this whitelist somewhere ?

Benoît

[Norman Megill]

On Sunday, January 12, 2020 at 5:24:59 PM UTC-5, Benoit wrote:

On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:

...
 

> The key insight is that because this does not affect consistency (it's a definition)

I don't understand: definitions like this may lead to inconsistencies (for instance, here, you'd better avoid the axiom x x^{-1} = 1).  The theory of meadows is of course consistent, but in general, one has to be careful.  Or you were referring to something more specific ?

There will never be an axiom x x^{-1} = 1) because the only axioms we use are the axioms of ZFC.  (OK, you could artificially add new axioms and arrive at a contradiction, but the "This theorem was proved from axioms" list will quickly reveal that you're cheating.)  The "axioms" we use for complex numbers are previously proven as theorems that are restated as axioms for convenience, but there still is nothing beyond ZFC.

Definitions can never lead to inconsistency if the pass the soundness check.  Nonsense definitions can lead to results that a mathematician might consider nonsense, but you can't prove a contradiction assuming ZFC is consistent.  We could swap the definitions of 4 and 5 (i.e. swap those symbols throughout set.mm) and have some strange looking results like 2+2=5, but although that violates the human convention for those symbols, we still can't prove a contradiction.

Norm

[Norman Megill]

In the specific case of df-riota, Quine's definition 8.18 is equivalent (see ~ dfiota2), and he mentions (p. 56) he designed it to evaluate to (/) when there isn't unique existence, in particular so that the definition remained a set for all possible arguments.  So we are exactly following the practice of at least one well-regarded authority.

[Benoit]

> There will never be an axiom x x^{-1} = 1) because the only axioms we use are the axioms of ZFC.  (OK, you could artificially add new axioms and arrive at a contradiction, but the "This theorem was proved from axioms" list will quickly reveal that you're cheating.)  The "axioms" we use for complex numbers are previously proven as theorems that are restated as axioms for convenience, but there still is nothing beyond ZFC.

> Definitions can never lead to inconsistency if the pass the soundness check.  Nonsense definitions can lead to results that a mathematician might consider nonsense, but you can't prove a contradiction assuming ZFC is consistent.  We could swap the definitions of 4 and 5 (i.e. swap those symbols throughout set.mm) and have some strange looking results like 2+2=5, but although that violates the human convention for those symbols, we still can't prove a contradiction.

I know this.  The paragraph you're referring to was about the formalization in Lean.  I was reacting to Mario's "it does not affect consistency because it's a definition".  Maybe there is also a definition soundness check in Lean and Mario meant "it does not affect consistency because this definition of inversion passes the definition soundness check".

In the specific case of df-riota, Quine's definition 8.18 is equivalent (see ~ dfiota2), and he mentions (p. 56) he designed it to evaluate to (/) when there isn't unique existence, in particular so that the definition remained a set for all possible arguments.  So we are exactly following the practice of at least one well-regarded authority.

As I wrote in my first post, I took df-iota as an example for the sake of concreteness.  My goal is mainly exploratory, and not restricted to set.mm: see the different things that can be done regarding undefined terms, with their pros and cons.  I already learnt a few things from Mario's answer, maybe some other readers did too, and it's already good enough for me.

Benoît

 

 

On Sunday, January 12, 2020 at 6:09:52 PM UTC-5, Norman Megill wrote:

On Sunday, January 12, 2020 at 5:24:59 PM UTC-5, Benoit wrote:

On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:

...
 

> The key insight is that because this does not affect consistency (it's a definition)

I don't understand: definitions like this may lead to inconsistencies (for instance, here, you'd better avoid the axiom x x^{-1} = 1).  The theory of meadows is of course consistent, but in general, one has to be careful.  Or you were referring to something more specific ?

Norm

[Mario Carneiro]

On Sun, Jan 12, 2020 at 5:25 PM Benoit <benoit...@gmail.com> wrote:

On Saturday, January 11, 2020 at 10:44:31 PM UTC+1, Mario Carneiro wrote:

qed::foo |- ( T. -> RH )

I don't understand: it looks like you are using foo with the substitutions ph <- T. and THM <- RH, but in order to make the latter substitution, you need to prove that RH has type |- , which means you need to prove it ?

Yes, that's the point. The question of whether this is a valid proof boils down to whether |- RH is provable, and the task of doing so has been off-loaded to the parser because it is a substitution. It would not be valid to write

1:: |- RH

qed:1:foo |- ( T. -> RH )

in mmj2 because foo doesn't have any $e hypotheses, so there is no place to provide the proof, and the part of mmj2 that is responsible for syntax axioms has to invent this proof on its own. The underlying metamath proof of course has this basic structure, but the separation of proofs into syntax and logical steps is violated.

> ... ( x = y -> P(x) = P(y) )

Is this really needed unconditionally ? For instance, for division by zero, do we really need |- ( x = y -> 1/x = 1/y ) ? Isn't it enough to have, for instance, |- ( ( x e. CC \ {0} /\ x = y ) -> 1/x = 1/y ) ?

Yes. Without it, the language will contain "non-denoting" terms, which cannot be definitionally unfolded, and this breaks the interpretation as a definitional extension of ZFC; we have to start thinking a lot more carefully about every definition (axiom) because we can't necessarily prove the justification theorem anymore. For instance, suppose that division was guarded as you propose. Then

foo y <-> E. x y = 1/x

does not satisfy the associated justification theorem

E. x y = 1/x <-> E. z y = 1/z

so it is not a valid definition. We've broken alpha renaming. So these non-denoting terms are really not like regular terms at all (in the FOL sense), but the problem of detecting if a term is denoting is undecidable. Not good.

 

> So ( 1 / 0 ) = ( 1 / 0 ) should not be rejected.

It would not be rejected with proposals 2 and higher, since every class is equal to itself.

True, but that's maybe too trivial an example. See the above alpha renaming example. Alternatively: is 1/(0+0) = 1/0 ? What about 1/foo = 1/0 where foo is defined to be 0? In any reasonable foundation that permits definition, the answer should be yes if 1/0 is a valid term of the language, regardless of what its value is.

> I have had a similar conversation about this in Lean

If it was online, do you have a link ?

It's a recurring topic, but Kevin Buzzard's and my comments here [1,2] are on point: ([1] is on zulip, if you have an account, [2] is the archived version)

[1]: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/1.2F0.3D0

[2]: https://leanprover-community.github.io/archive/113489newmembers/83326100.html

 

> but contrary to metamath [Lean] chooses to define x / 0 = 0 (and exploits this equality without any hedging).

So it considers the "meadow" (a new term for an older concept) associated with the field CC.  Side remark: I prefer the version 1/0 = \infty that I used in ~df-bj-invc.

 

> The key insight is that because this does not affect consistency (it's a definition)

I don't understand: definitions like this may lead to inconsistencies (for instance, here, you'd better avoid the axiom x x^{-1} = 1).  The theory of meadows is of course consistent, but in general, one has to be careful.  Or you were referring to something more specific ?

The point is that a definition has the form

foo(x,y) = <term depending on x and y and bound variables>

and no matter what you put in for the term, consistency is not violated by the introduction of foo, because in principle it can be understood as a mere abbreviation for the term on the RHS. This is the criterion that the mmj2 definition checker checks, and anything that compromises the ability for a mechanical tool to check the soundness of definitions gets a big thumbs down from me. (The definition checker is actually part of the trust base of metamath, unless you are okay with proofs relative to a massive 1000+ axiom system. MM0 is a bit more honest on this front in putting the mechanism into the verifier itself.)

As Kevin says in the linked thread, presuming you know what division of nonzero numbers means, you should think of Lean's division operation as defining a separate thing like so:

x /' y = if y != 0 then x / y else 0

and everywhere you see x / y written in lean you should mentally replace it with this funny x /' y operator. There is nothing mathematically dubious about making a definition like this, it's just some function, but it is also clear that if you use it in some place where the division is sensible, for example 1 /' 2, then it evaluates to 1 / 2 as expected, and a proof that uses /' all over the place is no more dubious than the introduction of a new definition like modular forms to solve an old problem like FLT.

> I contend that we already follow proposal 3 except in specific whitelist situations.

I do not see any discouragement tag for df-iota nor even for iotanul. Or is this part of the whitelist ?  Could we document this whitelist somewhere ?

The definition df-iota is not discouraged, nor iotanul, because it is a low level construction - whether out of domain usage is interpreted as okay or not depends on the application. So you should expect the discouraged marking on definitions based on df-iota, not on df-iota itself. (Of course, most definitions will just use it in range anyway so there is no need for a marking.)

 

On Sun, Jan 12, 2020 at 8:20 PM Benoit <benoit...@gmail.com> wrote:

> There will never be an axiom x x^{-1} = 1) because the only axioms we use are the axioms of ZFC.  (OK, you could artificially add new axioms and arrive at a contradiction, but the "This theorem was proved from axioms" list will quickly reveal that you're cheating.)  The "axioms" we use for complex numbers are previously proven as theorems that are restated as axioms for convenience, but there still is nothing beyond ZFC.

> Definitions can never lead to inconsistency if the pass the soundness check.  Nonsense definitions can lead to results that a mathematician might consider nonsense, but you can't prove a contradiction assuming ZFC is consistent.  We could swap the definitions of 4 and 5 (i.e. swap those symbols throughout set.mm) and have some strange looking results like 2+2=5, but although that violates the human convention for those symbols, we still can't prove a contradiction.

I know this.  The paragraph you're referring to was about the formalization in Lean.  I was reacting to Mario's "it does not affect consistency because it's a definition".  Maybe there is also a definition soundness check in Lean and Mario meant "it does not affect consistency because this definition of inversion passes the definition soundness check".

The "definition soundness check in Lean" is baked into the type theory. MM0's definition mechanism is a simplified version of Lean's: certain terms are marked as definitions, given values, and there is a conversion rule for unfolding a definition. Importantly, the "convertibility" or "definitional equality" judgment used for this purpose penetrates through *all* terms unconditionally. Metamath doesn't have definitional equality; we model it using = for classes and <-> for wffs, but for this to work we need equality theorems for *all* term constructors in the language, unconditionally. These have to be axiomatized for primitive term constructors like A. and e., but for definitions they can be proven provided you can unfold definitions unconditionally (which invalidates method 2).

 

Mario

[Benoit]

Thanks for the interesting link. I do not understand Buzzard's comment:

  "It's completely safe because every single theorem where division by 0 isn't allowed contains the hypothesis that the denominator isn't 0 in its statement."

How can you enforce that in the future, someone will not write a theorem not satisfying this ? Or is it again a "gentleman's agreement" ?

> The key insight is that because this does not affect consistency (it's a definition)

I don't understand: definitions like this may lead to inconsistencies (for instance, here, you'd better avoid the axiom x x^{-1} = 1).  The theory of meadows is of course consistent, but in general, one has to be careful.  Or you were referring to something more specific ?

The point is that a definition has the form...

> I was reacting to Mario's "it does not affect consistency because it's a definition".  Maybe there is also a definition soundness check in Lean and Mario meant "it does not affect consistency because this definition of inversion passes the definition soundness check".

The "definition soundness check in Lean" is baked into the type theory. MM0's definition mechanism is a simplified version of Lean's: certain terms are marked as definitions, given values, and there is a conversion rule for unfolding a definition. Importantly, the "convertibility" or "definitional equality" judgment used for this purpose penetrates through *all* terms unconditionally. Metamath doesn't have definitional equality; we model it using = for classes and <-> for wffs, but for this to work we need equality theorems for *all* term constructors in the language, unconditionally. These have to be axiomatized for primitive term constructors like A. and e., but for definitions they can be proven provided you can unfold definitions unconditionally (which invalidates method 2).

Ok, so it's a definition in the sense of "passing the definition soundness check", as I thought.  All is good.  I think the line "Cons" I wrote for proposal 2 summarizes it faithfully with "not a definitional extension".  Thanks for making it clearer.

Benoît

[Mario Carneiro]

On Mon, Jan 13, 2020 at 12:45 PM Benoit <benoit...@gmail.com> wrote:

Thanks for the interesting link. I do not understand Buzzard's comment:

  "It's completely safe because every single theorem where division by 0 isn't allowed contains the hypothesis that the denominator isn't 0 in its statement."

How can you enforce that in the future, someone will not write a theorem not satisfying this ? Or is it again a "gentleman's agreement" ?

It's a tautology, because this is what is meant by "division by 0 isn't allowed". Some theorems, like x * x^-1 = 1, only hold for nonzero arguments, so naturally any theorem stating this will have a nonzero assumption. No gentleman's agreement is necessary, as this is ensured by the soundness of the proof system.

Other theorems, like (-x)^-1 = -(x^-1), are satisfied also when x = 0, but in this case evidently division by 0 *is* allowed. No attempt is made to avoid the statement of such theorems in lean, and it's one less hypothesis to check. (Of course, chances are that you will need to know x is nonzero eventually after you string together 3 or 4 division theorems, but you don't have to provide the hypothesis each time if some have taken advantage of this "hack".)

Mario

[Benoit]

Of course!  Thanks!

By the way: I skimmed through the article that this discussion links to (https://www.hillelwayne.com/post/divide-by-zero/).  Strangely, the author does not mention meadows.  I note that he only mentions in passing the convention 1/0 = \infty, writing "This is what some mathematicians do with the Riemann sphere."  This approach is in set.mm as ~df-bj-invc.

Benoît