Also,
Why not put in set.mm,
a definition of ">" relating it to the "negation of <_"
And put a "you are absolutely forbidden to use this definition to write
theorems,
usage is discouraged, you'll be cursed and a ghost will haunt you if you
do ! "
With some explanation ?
(arghh I'm meddling ^^)
Happy funny sunday every one :)
Le 26/01/2020 à 08:50, Mario Carneiro a écrit :
On Sat, Jan 25, 2020 at 11:36 PM David A. Wheeler
<[email protected] <mailto:[email protected]>> wrote:
On Sat, 25 Jan 2020 18:40:53 -0800 (PST), Norman Megill
<[email protected] <mailto:[email protected]>> wrote:
> I know I keep harping on not wanting to add a catalog of
definitions (with
> shallow theorems) that are otherwise unused, but it has been
done in the
> past with the work essentially wasted, sometimes causing
resentment, and I
> want to avoid that. With an ambitious goal like "all of
mathematics," it
> will be very tempting to start collecting definitions, leading
to a false
> sense of accomplishment to see the syntax errors ironed out and
simple
> property theorems proved.
Not just tempting. Necessary.
I think I would also advocate a "theorems first" approach here.
Assuming that mathematicians have done their work right, definitions
should naturally fall out of the commonalities between theorems that
are stated in the literature. We don't need to give them any help in
this - good definitions make themselves known. After writing the same
sequence of characters enough times you get tired and want to compact
it to something more manageable.
I think the point about wasted work causing resentment also requires
acknowledgement. I would give at least a 50% chance, maybe more, that
an untested definition will need to be rewritten when one really gets
around to using it, and attribution at this point becomes messy,
because the original author may feel slighted by a rewrite (they
shouldn't, set.mm <http://set.mm> is public domain and we have always
recognized that your theorems may be rewritten to suit future work,
but sometimes we get attached to things anyway). While I don't really
want to enforce a policy along these lines, I certainly place the
worth of untested definitions very low. They can be recreated on first
use with little trouble.
> But in the end it is busywork with a good chance
> of being discarded later. Moreover, a few shallow value and
property
> theorems don't ensure that the definition is correct, possibly
misleading
> someone who might want to use set.mm <http://set.mm> as a
reference source that can be
> trusted to be rigorously correct.
*Nothing* other than human review ensures a definition is correct.
If we defined 9 as "( 8 + 3 )" there is no tool that could detect
the error.
Tools can detect if a definition is syntactically valid,
but no tool can figure out "was this really what you meant?"
I disagree with this sentiment. If you define 9 to be 8 + 3, then you
will later stumble when trying to prove that 9 * 9 is 81, or 9 + 1 =
10, or 9 is the first odd composite greater than 1. Basically, proving
theorems about a definition boxes it in, making it much less likely
that you got the statement wrong if all the expected proofs go
through. If the only proof you do is the definitional theorem, you
only get a very weak version of this, because the definitional theorem
is much more likely to be correlated with the definition itself, so it
is quite possible for errors to make it past both the axiom and the
definitional theorem.
The best solution for that is to provide definitions & enable
multi-person
human review to *detect* those problems. Failing to formalize those
definitions means that the needed multi-person review can't ever
happen.
If it isn't in set.mm <http://set.mm>, it doesn't need to be reviewed.
Review only happens *after* some development is submitted. And again,
I can't properly appraise the appropriateness of a definition without
seeing how it is going to be used.
A useful additional step would be to prove some "expected"
properties to
ensure that they "do what's expected". Again, that requires that they
be formalized in the database itself somewhere.
If you are talking about "unit tests" like 9 + 3 = 12, that's good,
but it is no substitute for general theorems, which constrain the
definition in a much broader way.
> This is the motivation for rule 2 I
> proposed, "definitions shouldn't be introduced unless there is
an actual
> need in the work at hand."
I would add:
... or if the definition will *never* be used by the rest of
set.mm <http://set.mm>, and it is
there solely to help translate widely-used constructs used in the
literature.
I can actually see a use for this, in the sense that having a
definition in main blocks future attempts to add that definition. If
we have a definition for greater-than, then we won't get repeated
requests to add it because it's already there. At the same time,
that's a bunch of unnecessary axioms to add to the database, and we
would have to guard them against use, which sounds like extra
complexity for the review process. (Yes I know we have discouraged
theorems, but it's still something we have to monitor.)
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 [email protected]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSsAZNLFTEWnFL1knc7qt4vAL-8sO0NWBWnU3JgCfEd-bw%40mail.gmail.com
<https://groups.google.com/d/msgid/metamath/CAFXXJSsAZNLFTEWnFL1knc7qt4vAL-8sO0NWBWnU3JgCfEd-bw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/b88c252e-1c32-1d7f-535c-c4fc5b2d9fb0%40gmail.com.
