Description: Unless there is a reason to diverge, we follow the conventions of the
Metamath Proof Explorer (MPE, set.mm). This list of conventions is
intended to be read in conjunction with the corresponding conventions in
the Metamath Proof Explorer, and only the differences are described
below.
- Minimizing axioms and the axiom of choice.
We prefer proofs that depend on fewer and/or weaker axioms,
even if the proofs are longer. In particular, our choice of IZF
(Intuitionistic Zermelo-Fraenkel) over CZF (Constructive
Zermelo-Fraenkel, a weaker system) was just an expedient choice
because IZF is easier to formalize in Metamath. You can find some
development using CZF in BJ's mathbox starting at wbd 15458 (and the
section header just above it).
As for the axiom of choice, the full axiom of choice implies
excluded middle as seen at acexmid 5921, although some authors will
use countable choice or dependent choice. For example, countable
choice or excluded middle is needed to show that the Cauchy reals
coincide with the Dedekind reals - Corollary 11.4.3 of [HoTT],
p. (varies).
- Junk/undefined results.
Much of the discussion of this topic in the Metamath Proof
Explorer applies except that certain techniques are not
available to us. For example, the Metamath Proof Explorer will
often say "if a function is evaluated within its domain, a
certain result follows; if the function is evaluated outside
its domain, the same result follows. Since the function must
be evaluated within its domain or outside it, the result follows
unconditionally" (the use of excluded middle in this argument is
perhaps obvious when stated this way). Often, the easiest fix
will be to prove we are evaluating functions within
their domains, other times it will be possible to use a theorem
like relelfvdm 5590 which says that if a function value produces
an inhabited set, then the function is being evaluated within
its domain.
- Bibliography references.
The bibliography for the Intuitionistic Logic Explorer is
separate from the one for the Metamath Proof Explorer but feel
free to copy-paste a citation in either direction in order to
cite it.
Label naming conventions
Here are a few of the label naming conventions:
- Suffixes.
We follow the conventions of the Metamath Proof Explorer with a few
additions. A biconditional in set.mm which is an implication in
iset.mm should have a "r" (for the reverse direction), or "i"/"im"
(for the forward direction) appended. A theorem in set.mm which has
a decidability condition added should add "dc" to the theorem name.
A theorem in set.mm where "nonempty class" is changed to "inhabited
class" should add "m" (for member) to the theorem name.
- iset.mm versus set.mm names
Theorems which are the same as in set.mm should be named the same
(that is, where the statement of the theorem is the same; the proof
can differ without a new name being called for). Theorems which are
different should be named differently (we do have a small number of
intentional exceptions to this rule but on the whole it serves us
well).
As for how to choose names so they are different between iset.mm
and set.mm, when possible choose a name which reflect the difference
in the theorems. For example, if a theorem in set.mm is an equality
and the iset.mm analogue is a subset, add "ss" to the iset.mm name.
If need be, add "i" to the iset.mm name (usually as a prefix to
some portion of the name).
As with set.mm, we welcome suggestions for better names (such
as names which are more consistent with naming conventions).
We do try to keep set.mm and iset.mm similar where we can. For
example, if a theorem exists in both places but the name in set.mm
isn't great, we tend to keep that name for iset.mm, or change it
in both files together. This is mainly to make it easier to copy
theorems, but also to generally help people browse proofs, find
theorems, write proofs, etc.
The following table shows some commonly-used abbreviations in labels
which are not found in the Metamath Proof Explorer,
in alphabetical order.
For each abbreviation we provide a mnenomic to help you remember it,
the source theorem/assumption defining it, an expression showing
what it looks like, whether or not it is a "syntax fragment"
(an abbreviation that indicates a particular kind of syntax), and
hyperlinks to label examples that use the abbreviation.
The abbreviation is bolded if there is a df-NAME definition but
the label fragment is not NAME.
For the "g" abbreviation, this is related to the set.mm usage,
in which "is a set" conditions are converted from hypotheses
to antecedents, but is also used where "is a set" conditions are added
relative to similar set.mm theorems.
(Contributed by Jim Kingdon, 24-Feb-2020.)
(New usage is discouraged.) |
