On Sat, Jan 11, 2020 at 11:24 AM Benoit <[email protected]> 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
--
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/CAFXXJSvWkBeXQWR3daK9_xYbrKAB_wDgVvdm022kvD1uH%3DSWoA%40mail.gmail.com.
