Grounding the axiomatic reals

[Mario Carneiro]

Hi All,

I am wondering if I can get any traction on the following "axiom of the reals":

ax-cngd $a |- CC e. ( R1 ` ( om +o om ) ) $.

This axiom is unspecific about exactly which level of the universe hierarchy the reals live in (if I did my math correctly, with our current construction (rank`CC) = om+8), but is still strong enough to ensure that the reals are contained in not too many powerset iterations, as well as ensure that all the elements of CC are well-founded without the axiom of foundation. This is useful for some foundational issues - we would like ( R1 ` ( om +o om ) ) to be big enough for most "normal" mathematics (it is a model of ZC), but due to our separation of the explicit construction from the axiomatization, nothing stops the elements in CC from living in some unimaginably huge universe, so that many small-seeming constructions like the polynomial ring construction get pushed to very large universes due to the embedded usage of real number constructs like NN.

One specific application I've been thinking about is the category of sets. After some deliberation I think that using large categories in Metamath is more trouble than it's worth, so this means we need universes. However, I am not convinced that ZF universes are actually needed; most categorical constructions are well-served by a collection of sets closed under subset, union, and powerset, and ( R1 ` ( om +o om ) ) is the smallest of these which contains an infinite member. This suggests having an operation analogous to tarskiMap which produces a universe closed under these things and containing a given set x, and then this universe will have all the nice categorical properties that Set has: initial/terminal objects, products/coproducts, small (indexed) limits, exponential objects.

It would be very nice if these same universes could be used for categories of groups, etc. but this hits some problems when, for example, the free group on X does not live in the same universe as X because it refers to the unimaginably huge NN (instead of om, which is at a known location in the cumulative hierarchy).

Mario

[David A. Wheeler]

On Tue, 13 Dec 2016 05:52:17 -0500, Mario Carneiro <di....@gmail.com> wrote:
> Hi All,
>
> I am wondering if I can get any traction on the following "axiom of the
> reals":
>
> ax-cngd $a |- CC e. ( R1 ` ( om +o om ) ) $.

I really hate to see us adding new axioms, especially ones
that don't have any precedence in the literature.
It's great that there are so *few* true axioms (not counting definitions).
Is there somewhere common where this has been accepted?

> One specific application I've been thinking about is the category of sets.
> After some deliberation I think that using large categories in Metamath is
> more trouble than it's worth, so this means we need universes.

What's the trouble that makes it more trouble than it's worth? Any examples?
Preferably an example mortals can understand... :-).

--- David A. Wheeler

[Mario Carneiro]

On Tue, Dec 13, 2016 at 5:44 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Tue, 13 Dec 2016 05:52:17 -0500, Mario Carneiro <di....@gmail.com> wrote:
> Hi All,
>
> I am wondering if I can get any traction on the following "axiom of the
> reals":
>
> ax-cngd $a |- CC e. ( R1 ` ( om +o om ) ) $.

I really hate to see us adding new axioms, especially ones
that don't have any precedence in the literature.
It's great that there are so *few* true axioms (not counting definitions).
Is there somewhere common where this has been accepted?

Note that this is not an *actual* axiom, in the sense that it follows from the construction so the axiom is conservative over ZFC. It is simply preserving a property that we had in the construction and lost in the axiomatization. It can also be read as a compatibility between the axioms of the reals and those of ZFC, relating pure set theory and axiomatic real numbers. In particular, it would be immediately preceded by a theorem

axcngd $p |- CC e. ( R1 ` ( om +o om ) ) $= ... $.

which proves the statement from the construction of CC.

It would be nice if the HTML display showed the real number axioms in a different place than the other axioms, down by the definitions, because like the definitions they are conservative extensions. If we had a general mechanism for this, it would really cut down on the axiom list length for most later theorems, better reflecting the fact that those 23 axioms are not really axioms in the philosophical sense.

 

> One specific application I've been thinking about is the category of sets.
> After some deliberation I think that using large categories in Metamath is
> more trouble than it's worth, so this means we need universes.

What's the trouble that makes it more trouble than it's worth?  Any examples?
Preferably an example mortals can understand... :-).

Most of our algebraic constructions, such as A e. Grp, are sets. The natural thing to do by analogy would be to have A e. Cat, to say that A is a category, but then A is necessarily a set (a.k.a a small category), so in particular many categories of interest such as the category of sets, groups, rings etc. are not categories by this definition. It is possible to state "A is a large category" in Metamath, as a class predicate "wff LargeCat A", but then the collection of all large categories is not a category (or even well-formed - LargeCat has no independent existence that we can refer to). Although this whole "category of categories" thing may seem gratuitous, this is exactly the sort of thing that is exploited in serious category theory, forming functor categories and iterating this operation to get larger categories.

ZFC is of course well-suited to flattening this type-theoretic hierarchy into one large universe of sets. The catch is that we must commit to small categories all the way. This is still sufficient for all purposes, in particular if the TG axiom is used, because then there are sets that satisfy all the properties that the full universe of ZFC does. If large categories are defined within such a framework, they will certainly be "second-class citizens": we will not be able to perform most categorical constructions on them. This is analogous to how certain operations like <. A , B >. cease to operate correctly when the arguments are proper classes. For a proper algebra of categories and their operations, we need them to be sets.

One thing that I would like to investigate for doing category theory without the TG axiom is a "weak universe" (for lack of a better name), which is a set closed under powerset, union, and subset. ZF proves that every set is contained in a weak universe, and every stage ( R1 ` A ) of the cumulative hierarchy, where A is a limit ordinal, is a weak universe. A weak universe is a model for ZC, and is sufficient to be a model of the categorical set theory ETCS. The big difference between a weak universe and a Grothendieck universe is some equivalent of the replacement axiom. A Grothendieck universe is closed under "small unions", meaning that if F : I --> U and I e. U, then U_ x e. I ( F ` x ) e. U. If you additionally require this, a limit ordinal is not sufficient - you need A to be an inaccessible cardinal. This is also expressed categorically by saying that the large category Set is closed under small limits, but Set_U where U is a weak universe is only closed under finite limits. (For example, R1(om+om) is a weak universe, and contains the index set om, but the function F = (n e. om |-> R1(om+n)) has no union inside R1(om+om).)

The paper https://arxiv.org/abs/0810.1279 is a good discussion of the many ways to do category theory in ZFC and extensions. Around page 31 (section 11), there is a good discussion of how to call this category Set_U complete even though it is not in the "naive" sense used above, by arguing that the function (n e. om |-> R1(om+n)) is "illegitimate". This weaker kind of completeness is more appropriate for the strongly constructive style in which most category theory is conducted, so I anticipate that weak universes will be sufficient.

(I'm not sure I reached "an example mortals can understand" with this discussion, but somehow category theory always stymies attempts at plain explanations...)

Mario

[Jens-Wolfhard Schicke-Uffmann]

On Wed, Dec 14, 2016 at 02:30:26AM -0500, Mario Carneiro wrote:
>In particular, it would be immediately preceded by a theorem
>
> axcngd $p |- CC e. ( R1 ` ( om +o om ) ) $= ... $.
>
> which proves the statement from the construction of CC.
>
> It would be nice if the HTML display showed the real number axioms in a
> different place than the other axioms, down by the definitions, because like
> the definitions they are conservative extensions.

What exactly is the purpose of the real number $a statements anyway? In
particular, if it's just isolation of the later theorems from the construction,
why do we not have trivial $p statements instead?


Regards,
Drahflow

[Norman Megill]

On Wednesday, December 14, 2016 at 2:30:28 AM UTC-5, Mario Carneiro wrote:

On Tue, Dec 13, 2016 at 5:44 PM, David A. Wheeler <dwhe...@dwheeler.com> wrote:

On Tue, 13 Dec 2016 05:52:17 -0500, Mario Carneiro <di....@gmail.com> wrote:
> Hi All,
>
> I am wondering if I can get any traction on the following "axiom of the
> reals":
>
> ax-cngd $a |- CC e. ( R1 ` ( om +o om ) ) $.

I really hate to see us adding new axioms, especially ones
that don't have any precedence in the literature.

Like David, I dislike adding new axioms without a compelling reason.  You present a good reason below, which is that it allows us to avoid or postpone the use of ax-groth in category theory.

However, I think it would cause the least confusion for someone studying the CC axioms if we introduced it where it becomes needed and not as part of the main CC work.  In particular, just understanding the notations om, +o, and R1 (not to mention what the compound expression "means") could be off-putting for beginners, whereas the rest of the CC axioms use only the much more elementary set theory concepts of membership and subset.

Another issue is that it places restrictions on possible constructions of CC (in a similar sense as having 0ncn as an axiom would have) that lies outside of what is normally thought of as a "complex number system".  This is another reason to introduce it much later when it is first needed.
 

It's great that there are so *few* true axioms (not counting definitions).
Is there somewhere common where this has been accepted?

Note that this is not an *actual* axiom, in the sense that it follows from the construction so the axiom is conservative over ZFC. It is simply preserving a property that we had in the construction and lost in the axiomatization. It can also be read as a compatibility between the axioms of the reals and those of ZFC, relating pure set theory and axiomatic real numbers. In particular, it would be immediately preceded by a theorem

axcngd $p |- CC e. ( R1 ` ( om +o om ) ) $= ... $.

which proves the statement from the construction of CC.

I think axcngd should be in the CC construction section (along with its "(New usage is discouraged.)" tags) to help keep that section isolated and swappable with another construction in the future.  So to satisfy my first request above, ax-cngd would occur well after axcngd.  I don't see this as a problem since the comment can explain things clearly.
 

It would be nice if the HTML display showed the real number axioms in a different place than the other axioms, down by the definitions, because like the definitions they are conservative extensions.

Yes and no.  By referencing the CC axioms instead of their construction theorems, we suppress the true axioms behind them, thus making the CC axioms true axioms and not just definitions.  For example, 2p2e4 ultimately requires considerably more set theory axioms than just the ax-ext shown after "This theorem was proved from axioms".  Unlike definitions, the CC axioms can't be eliminated without invoking additional ZFC axioms.

Another murky area is the df-clab, df-cleq, df-clel triple, but (without getting into subtle issues we've discussed extensively)  they can be eliminated mechanically without invoking ZFC axioms (except to eliminate the ax-ext hypothesis of df-clel).

Right now, the CC axioms stand out somewhat in the axiom list with the different color of their higher theorem numbers.  Possibly in the future we could have a "This theorem was proved from derived axioms" list, possibly with a third prefix extending "ax-" and "df-", but it would take time and effort because the latter are deeply hard-coded into the web page generation software and other places.  I would want to be convinced that the present method really causes confusion.  I think the explanations in the CC axiom descriptions are pretty clear and thorough.
 

If we had a general mechanism for this, it would really cut down on the axiom list length for most later theorems, better reflecting the fact that those 23 axioms are not really axioms in the philosophical sense.

 

> One specific application I've been thinking about is the category of sets.
> After some deliberation I think that using large categories in Metamath is
> more trouble than it's worth, so this means we need universes.

What's the trouble that makes it more trouble than it's worth?  Any examples?
Preferably an example mortals can understand... :-).

Most of our algebraic constructions, such as A e. Grp, are sets. The natural thing to do by analogy would be to have A e. Cat, to say that A is a category, but then A is necessarily a set (a.k.a a small category), so in particular many categories of interest such as the category of sets, groups, rings etc. are not categories by this definition. It is possible to state "A is a large category" in Metamath, as a class predicate "wff LargeCat A", but then the collection of all large categories is not a category (or even well-formed - LargeCat has no independent existence that we can refer to). Although this whole "category of categories" thing may seem gratuitous, this is exactly the sort of thing that is exploited in serious category theory, forming functor categories and iterating this operation to get larger categories.

ZFC is of course well-suited to flattening this type-theoretic hierarchy into one large universe of sets. The catch is that we must commit to small categories all the way. This is still sufficient for all purposes, in particular if the TG axiom is used, because then there are sets that satisfy all the properties that the full universe of ZFC does. If large categories are defined within such a framework, they will certainly be "second-class citizens": we will not be able to perform most categorical constructions on them. This is analogous to how certain operations like <. A , B >. cease to operate correctly when the arguments are proper classes. For a proper algebra of categories and their operations, we need them to be sets.

One thing that I would like to investigate for doing category theory without the TG axiom is a "weak universe" (for lack of a better name), which is a set closed under powerset, union, and subset. ZF proves that every set is contained in a weak universe, and every stage ( R1 ` A ) of the cumulative hierarchy, where A is a limit ordinal, is a weak universe. A weak universe is a model for ZC, and is sufficient to be a model of the categorical set theory ETCS. The big difference between a weak universe and a Grothendieck universe is some equivalent of the replacement axiom. A Grothendieck universe is closed under "small unions", meaning that if F : I --> U and I e. U, then U_ x e. I ( F ` x ) e. U. If you additionally require this, a limit ordinal is not sufficient - you need A to be an inaccessible cardinal. This is also expressed categorically by saying that the large category Set is closed under small limits, but Set_U where U is a weak universe is only closed under finite limits. (For example, R1(om+om) is a weak universe, and contains the index set om, but the function F = (n e. om |-> R1(om+n)) has no union inside R1(om+om).)

The paper https://arxiv.org/abs/0810.1279 is a good discussion of the many ways to do category theory in ZFC and extensions. Around page 31 (section 11), there is a good discussion of how to call this category Set_U complete even though it is not in the "naive" sense used above, by arguing that the function (n e. om |-> R1(om+n)) is "illegitimate". This weaker kind of completeness is more appropriate for the strongly constructive style in which most category theory is conducted, so I anticipate that weak universes will be sufficient.

(I'm not sure I reached "an example mortals can understand" with this discussion, but somehow category theory always stymies attempts at plain explanations...)

My trouble with category theory is that the literature never seems to give a true formal definition: what are the primitives, the syntax of legal wffs, and the actual formal axioms and rules of inference, in the same sense as set.mm does for ZFC.  I think it would be very useful to have a .mm file for category theory, just as we do for NF and HOL, that at least spells out the axioms and maybe has a handful of starting theorems.

Norm

[Norman Megill]

It is primarily to make the "This theorem was proved from axioms" list on the web pages reflect only the ZFC axioms needed on top of the construction.  The construction is meant to be portable, and a different construction might have different ZFC axioms behind it.  Each axiom and the corresponding $p have clear comments referencing each other, so it becomes easy to identify what was needed for the provided construction without having it propagate to all CC theorems.

As a side effect, the large number of definitions used by the construction are completely suppressed in the "This theorem depends on definitions" list.

There are other axioms which we derive from ZFC, such as ax-sep after proving axsep, in order to be able to isolate where the weaker ax-sep can be used in place of the stronger ax-rep.

BTW this separation of axioms is a relatively recent (last 10 years) feature added to set.mm, that (particularly for ax-sep) was suggested by several people.

Norm

[David A. Wheeler]

Mario Carneiro:

> Note that this is not an *actual* axiom, in the sense that it follows from
> the construction so the axiom is conservative over ZFC. It is simply
> preserving a property that we had in the construction and lost in the axiomatization.

Ah, that's different. But this is confusing. At the least, this should happen later
as suggested by Norm, to reduce confusion. But this raises a broader issue...

> On Wednesday, December 14, 2016 at 6:15:06 AM UTC-5, drahflow wrote:
> > What exactly is the purpose of the real number $a statements anyway? In
> > particular, if it's just isolation of the later theorems from the
> > construction,
> > why do we not have trivial $p statements instead?

On Wed, 14 Dec 2016 06:32:21 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> It is primarily to make the "This theorem was proved from axioms" list on
> the web pages reflect only the ZFC axioms needed on top of the
> construction. The construction is meant to be portable, and a different

> construction might have different ZFC axioms behind it...

Every new axiom risks creating an inconsistency; there are a *lot* of
these "axioms" that are actually just restatements of proven theorems.
I *definitely* agree that having portable constructions is very valuable,
but perhaps we could do this a different way.

We already have several statements that help scope theorems
to support portability.
How about adding something like "(This theorem should be treated as an axiom.)"
or something like that, so that HTML displays that trace back to axioms *stop*
at these? Then many of the "axioms" no longer need to be axioms.
That would decrease the number of statements in set.mm, and
increase the number of things checked/proven by the tools.
Smaller set.mm size, better checking, no change to the fundamental language :-).

--- David A. Wheeler

[Norman Megill]

On Wednesday, December 14, 2016 at 9:56:42 AM UTC-5, David A. Wheeler wrote:
...

We already have several statements that help scope theorems
to support portability.
How about adding something like "(This theorem should be treated as an axiom.)"
or something like that, so that HTML displays that trace back to axioms *stop*
at these?  Then many of the "axioms" no longer need to be axioms.
That would decrease the number of statements in set.mm, and
increase the number of things checked/proven by the tools.
Smaller set.mm size, better checking, no change to the fundamental language :-).

There aren't as many theorems restated as axioms as one might think.  I counted:

Prop calc (1)
ax-meredith

Pred calc (7)
ax-9 ax-12o ax-5o ax-6o ax-9o ax-10o ax-11o

ZFC (7)
ax-sep ax-nul ax-pow ax-pr ax-inf2 ax-cc ax-dc

CC (26)
ax-cnex ax-resscn ax-1cn ax-icn ax-addcl ax-addrcl ax-mulcl ax-mulrcl ax-mulcom ax-addass ax-mulass ax-distr ax-i2m1 ax-1ne0 ax-1rid ax-rnegex ax-rrecex ax-cnre ax-pre-lttri ax-pre-lttrn ax-pre-ltadd ax-pre-mulgt0 ax-pre-sup ax-addf ax-mulf

I am not including the Hilbert Space Explorer (it will become obsolete), unused axioms like Mario's ax-8d, and mathboxes.

The pred calc *o axioms mainly arose as a result of simplifications or redundancies found over many years.  In principle they could all go away but are currently kept so I can play with different axiomatizations.  Eventually I anticipate that none of the *o's will not be used outside of localized studies of equivalence, and some may be deleted.

I don't think the rather significant effort to modify the software, which will also create yet another markup concept (pseudo axiom) for users to become familiar with, is worth it for this small number of cases, all of which have been carefully vetted.

Maybe a custom tool could, for each ax-* $a, see if there is a $p without the hyphen and check that the content matches.  But I think even that would be overkill, since it's easy to do it by hand for these small number of cases.

We have no plans to add new axioms to the main set.mm on a casual basis.  That is why we are debating Mario's proposed ax-cngd.

Norm

[Norman Megill]

On Wednesday, December 14, 2016 at 10:55:44 AM UTC-5, Norman Megill wrote:

I don't think the rather significant effort to modify the software, which will also create yet another markup concept (pseudo axiom) for users to become familiar with, is worth it for this small number of cases, all of which have been carefully vetted.

Maybe a custom tool could, for each ax-* $a, see if there is a $p without the hyphen and check that the content matches.  But I think even that would be overkill, since it's easy to do it by hand for these small number of cases.

I will look at adding the following to "verify markup":  if a $a label starting with "ax-" has a $p version without the hyphen, check that their assertions, mandatory hypotheses, and mandatory $d's match exactly.  The would verify the existing informal convention without adding any new markup tags.

Norm

[Mario Carneiro]

I really like this idea. Here's a proposed algorithm for finding "the true axioms" for a statement:

Precompute: For each axiom ax-XXX, if a theorem axXXX appears earlier in the database and has the same statement, register axXXX as a proof for ax-XXX, and calculate its axiom usage.

For a given theorem T, first calculate the axioms used in the usual way, and discard df-* axioms as is currently done. The remaining axioms are what currently appear in the axioms used list. Starting from the end and working backwards, if an axiom in the list has a proof, and all the axioms for this proof appear in the list, then cross it off the list.

For example, suppose that we have:

* axioms A,B prove C

* axioms A,C prove E

* axioms A,F prove G

and theorem T is proven from axioms A,B,C,E,G. Then:

* G is not removed because F is not in the list

* E is removed because A,C are present

* C is removed because A,B are present

* B is not removed because it has no proof

* A is not removed because it has no proof

Thus the final reported list is that theorem T is proven from A,B,G. If you are not confident of the validity of this procedure, you can also report that axioms C,E are also used but are provable given A,B,G.

Note that this will not needlessly pollute statements like 2p2e4 with set theory axioms, but will remove ax-sep from proofs that use ax-rep and the rest of the zoo, and will remove real number axioms from any statements that use all ZF axioms in addition.

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 metamath+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[David A. Wheeler]

It's still a remarkably high percentage.
By the count above, at least 1+7+7+26=41
are simply restatements of already-proven theorems.

I grepped for 'ax-.*$a', then removed ax-8d and all axioms
starting with ax-hilex (Hilbert Space Explorer).
By that process, I found that there are 72 defined axioms.

That means that 57% (a *majority*) of these axioms are restatements
of already-proven theorems. Not exactly what you would expect
when you see the word "axiom" :-). Especially since every axiom can,
in theory, create inconsistencies.

--- David A. Wheeler

[fl]

My trouble with category theory is that the literature never seems to give a true formal definition: what are the primitives, the syntax of legal wffs, and the actual formal axioms and rules of inference, in the same sense as set.mm does for ZFC.

I vaguely remember that they don't exist and can't exist. Category theory can't be a replacement for set theory. It must be built
over it (or an equivalent theory).

--
FL

[fl]

Something like that.

http://homepages.vub.ac.be/~mcabbole/papers/ImportanceCAforCT.pdf

--
FL

[fl]

My opinion about using a predicate to define categories (what Mario calls "large categories" above) is that:

 1) Norm doesn't like this.
 2) In Metamath it's a nightmare. Not a pure nightmare but a nightmare.
 3) But it is the only way to understand what a "large category" is.
 4) If you fall back to a structure, I advise you to formalize object-free categories.
     It has a very pleasant tiny footprint.

--
FL

[Norman Megill]

On Thursday, December 15, 2016 at 2:12:28 PM UTC-5, David A. Wheeler wrote:

Most of the theorems restated as axioms are the complex number axioms, which are all in one place.  Hopefully you understand the motivation for doing that, which has been discussed quite a bit and is carefully explained in the comments in the respective theorems and axioms.

Of the others, ax-meredith is confined to a small, self-contained section that can be deleted or extracted to a separate database by anyone who finds it bothersome.  The ax-*o axioms in pred calc are just for my personal convenience and can easily be eliminated (and likely will someday, or confined to a special section or even moved to my mathbox).

There are 6 redundant set theory axioms (not 7; I included ax-pow by mistake).  ax-inf2 is a special case we can discuss separately, but the other 5 are included as redundant axioms in many if not most set theory books.  The authors (1) want to introduce concepts slowly by introducing say ax-pr before the more complex ax-rep it is derived from and/or (2) think it is important to use the weakest axioms possible for a given result and/or (3) aren't bothered by redundant axioms, especially when they feel the benefits outweigh the drawbacks.  Because of our minimalist philosophy, we have adopted only non-redundant axioms as "official", but in a nod to standard literature we derive and restate as axioms the standard redundant ones.  In other words, we aren't doing anything much different from the literature.

Changing all of the software and commands to recognize theorems marked as pseudo axioms by a markup tag is a rather large task.  It will also make things slower - 'verify markup *' is already getting a little sluggish because of all the string searching and manipulation.  Overall, it seems like a lot of effort to address a problem that has never happened, involving a handful of stable axioms that have been tested thoroughly and are unlikely to change over time.
 

Especially since every axiom can,
in theory, create inconsistencies.

Checking the derived ones against their corresponding theorems using the existing label convention of axXXX vs. ax-XXX, as I proposed, will prevent this.

Norm

[David A. Wheeler]

On Thu, 15 Dec 2016 14:49:35 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:
> Most of the theorems restated as axioms are the complex number axioms,
> which are all in one place. Hopefully you understand the motivation for

> doing that...

Sure. I don't mind using "$a" per se for these situations; the "$a" is being used
to control the scope of information.

That said, I think statements that are proven by another theorem
are really different than you-must-accept-this-without-proof axioms.

I see two issues:
1. If practical, there should be some kind of automated check that the
the statements that are supposed to be proven are actually proven.
Otherwise there's a risk that the new $a statements are subtly different
than their proof (possibly due to changes in one but not the other).
I agree that checking the derived ones against their corresponding theorems using the
existing label convention of axXXX vs. ax-XXX, as I proposed, will solve this.
2. It should be really obvious to humans that this is happening, without requiring them
to carefully read and parse the commentary text.
I think there should be some conventional phrase
that's always used in these cases, just to point out when it happens. Something like:
"This is stated as an axiom, but is proven by ~ NAME " (or whatever).
The tools don't need to treat this magic phrase specially, its purpose is simply
to make the situation very obvious. (The markup checker could warn
when there's both ax-BLAH and axBLAH but the magic phrase is missing.)

--- David A. Wheeler

[David A. Wheeler]

When I said:
> existing label convention of axXXX vs. ax-XXX, as I proposed, will solve this.

Um, the "I" there is actually Norm :-). Bad cut-and-paste, sorry.

--- David A. Wheeler