>
>
> Someone suggested using Bourbaki as a guide for ordering the definitions
> and theories related to structures. I think this is a good idea.
> It is the longest and most comprehensive treatise on structures.
>
>
It's a good idea. I insist.
Netflix streaming when the planet is burning is
I agree that both dummylink and idi should not be deleted or discouraged.
While mmj2 should normally detect and collapse reused steps, I don't know
if this behavior should be relied upon, and if a proof assistant finds a
proof using idi then that is just as good, since it produces the right
proof
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
On January 12, 2020 3:25:13 PM PST, "David A. Wheeler"
wrote:
>I propose that dummylink & idi be marked with
>"(New usage is discouraged.)".
Makes sense to me. I'm not thinking of any disadvantages.
--
You received this message because you are subscribed to the Google Groups
"Metamath"
On Sunday, January 12, 2020 at 7:09:17 PM UTC-5, Norman Megill wrote:
>
> As for idi, I don't really care - mmj2 used to make use of it but I don't
> think it does anymore. As far as I am concerned, we can delete idi unless
> someone has a use for it.
>
>
Alan Sare's tool "completeusersproof"
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
This was proposed in PR #1105. There is an ensuing discussion.
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 metamath+unsubscr...@googlegroups.com.
To
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
> 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
On Sun, Jan 12, 2020 at 5:25 PM Benoit 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
I don't think it's necessarily because both of these will automatically be
removed with 'minimize'.
While I may be the only one to do so, I have used dummylink to build proofs
in MM-PA to work around the "backwards only" method it requires. Making it
'discouraged' will be a nuisance that I'll
On Sunday, January 12, 2020 at 11:51:10 PM UTC+1, Jim Kingdon wrote:
>
> Heh, maybe it is a generational thing because I look at the HoTT book as
> the thing to be studied and formalized.
>
Please note that Bourbaki was not brought up in this discussion (in the
link I gave above) as the thing
On Sun, 12 Jan 2020 18:02:14 -0800 (PST), Norman Megill
wrote:
> >
> Alan Sare's tool "completeusersproof" appears to make use of idi, at least
> it appears in his C code and is referenced extensively in the program
> comments. Although this program probably has a very small user base, I
>
On January 12, 2020 11:04:54 PM EST, Norman Megill wrote:
>I'm unclear about what prompted this and why it is considered a
>problem.
No problem, you answered my question. No change in set.mm is fine. Carry on!
--- David A.Wheeler
--
You received this message because you are subscribed to the
On January 12, 2020 10:17:49 AM PST, vvs wrote:
>I have no opinion about Bourbaki, though. That might be the problem...
Heh, maybe it is a generational thing because I look at the HoTT book as the
thing to be studied and formalized.
Like Bourbaki, it was written by a number of
I propose that dummylink & idi be marked with
"(New usage is discouraged.)".
As noted in the text,
they should normally never appear in a completed proof.
Marking them this way will prevent them from being
automatically used, and I think that's usually what is wanted.
The normal mmj2 invocation
On Sun, 12 Jan 2020 16:09:16 -0800 (PST), Norman Megill
wrote:
> I don't think it's necessarily because both of these will automatically be
> removed with 'minimize'. ...
Okay, how about marking just idi with "(New usage is discouraged.)"?
I *do* refer to idi in a tutorial, and it's useful in
I'm unclear about what prompted this and why it is considered a problem. I
don't see why we should care whether someone wants to use dummylink or idi
for whatever reason. They are harmless, and all they do is make the proof
slightly less efficient. It is a trivial and temporary cosmetic
> Though, you should ignore me, because I'm a grouchy oddball.
>
Don't be so negative. You don't like smartphones and don't watch Netflix:
you look like a very brave man. Your grandchildren will show off proudly
your photograph
in their atomic shelter to their relatives as THE guy who did
>
> Guys once again. Do something for the planet: renounce to netflix and your
> smartphones and adopt Bourbaki.
> Your children and grandchildren will look up to you as heroes and not as
> those who did nothing.
>
I don't like smartphones, don't watch Netflix and I'm trying to learn
On Saturday, January 11, 2020 at 1:33:13 PM UTC-5, Jon P wrote:
>
> Quick question: Why are the following sections marked as depricated in
> set.mm?
>
> PART 18 ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS (DEPRECATED)
>
> PART 19 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)
>
The
Jon P wrote:
>> Quick question: Why are the following sections marked as depricated in
>> set.mm?
...
>> PART 18 ADDITIONAL MATERIAL ON GROUPS, RINGS, AND FIELDS
>(DEPRECATED)
>>
>> PART 19 COMPLEX TOPOLOGICAL VECTOR SPACES (DEPRECATED)
Norman Megill:
>The intent is for these deprecated
Guys once again. Do something for the planet: renounce to netflix and your
smartphones and adopt Bourbaki.
Your children and grandchildren will look up to you as heroes and not as
those who did nothing.
--
FL
--
You received this message because you are subscribed to the Google Groups
23 matches
Mail list logo
