Hi Norm, That's extremely helpful. We will look into enforcing discourage uses in the future, to shorten the loop between our models and set.mm.
Thank you very much. -stan On Tue, Jul 7, 2020 at 5:46 PM Norman Megill <[email protected]> wrote: > > This is nice work Stanislas, thank you. > > On Friday, July 3, 2020 at 5:09:55 AM UTC-4, Stanislas Polu wrote: > >> - `1re` uses more axioms but is much simpler (how do we feel about >> that given the comment there?). > > > A problem with this particular proof is that it uses df-1, which has the tag > "(New usage is discouraged.)". > > Let me explain a little about how the complex numbers are introduced. Our > overall goal in set.mm is to show mathematics that follows from the ZFC > axioms. For complex numbers, we construct a model (a set of axioms stated as > $p statements) starting from ZFC axioms. We then restate these derived > axioms ($p statements) as actual axioms ($a statements) in order to (1) make > the complex number development independent from the construction (so that > alternate models could in principle be "plugged in") and (2) make it easier > to see what complex number axioms are needed for a particular complex number > theorem. So, for example, we derive ax1cn in the model part, then restate > that theorem as axiom ax-1cn. (To help ensure we're not cheating by > introducing new axioms beyond ZFC, the 'verify markup' command in > metamath.exe checks that each ax-* $a statement exactly matches an earlier $p > statement with the "-" removed, if such a $p statement exists.) > > To help prevent the accidental usage of the complex number construction when > we later use complex numbers, we have "(New usage is discouraged.)" in every > statement in the development of the complex number model. df-1 is one such > statement, since it might change if we used a different complex number > construction. > > For our metamath.exe and mmj2 proof assistants, the string "(New usage is > discouraged.)" in a comment tells the proof assistant not to consider that > statement for use in a proof being developed. In addition, the Travis run > that is done after each pull request checks that the usage of statements with > "(New usage is discouraged.)" didn't change as a result of the PR (unless it > was done intentionally and the user has supplied a regenerated "discouraged" > file as part of the PR). > > I would recommend that the OpenAI assistant check statement descriptions for > the string "(New usage is discouraged.)" and avoid considering them for use > in proofs. (The metamath.exe command 'write source set.mm /rewrap' currently > prevents this string from being broken across lines, but I'm not sure we want > to guarantee that, nor can we guarantee the '/rewrap' command was run. But > for a quick and dirty check you can assume it's not broken across lines and > refine it later with a TODO.) > > Norm > > -- > 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/dd8ea31b-8799-4591-a6d4-688c519eedado%40googlegroups.com. -- 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/CACZd_0yJoGqvyCsp1xegaSGrQs7EPL%2Bt_PLe285A2qA%2BvnBQHQ%40mail.gmail.com.
