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
--
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/a9457ec0-2b52-4bff-b670-2750e7c1542b%40googlegroups.com.
