On Sun, Jan 12, 2020 at 5:25 PM Benoit <[email protected]> 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 <[email protected]> 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
--
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/CAFXXJSs895As7575RU5JyvVp4OyFfANiLZXt3Sq82j5vN3JL-A%40mail.gmail.com.
