ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  conventions Unicode version

Theorem conventions 12372
Description: Unless there is a reason to diverge, we follow the conventions of the Metamath Proof Explorer (MPE, 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 12427 (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 5689, 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). For this reason, we generally need to prove we are evaluating functions within their domains and avoid the reverse closure theorems of the Metamath Proof Explorer.
  • 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 which is an implication in should have a "r" (for the reverse direction), or "i"/"im" (for the forward direction) appended. A theorem in which has a decidability condition added should add "dc" to the theorem name. A theorem in where "nonempty class" is changed to "inhabited class" should add "m" (for member) to the theorem name.
  • versus names

    Theorems which are the same as in 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 and, when possible choose a name which reflect the difference in the theorems. For example, if a theorem in is an equality and the analogue is a subset, add "ss" to the name. If need be, add "i" to the name (usually as a prefix to some portion of the name).

    As with, we welcome suggestions for better names (such as names which are more consistent with naming conventions).

    We do try to keep and similar where we can. For example, if a theorem exists in both places but the name in isn't great, we tend to keep that name for, 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 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 theorems.

AbbreviationMnenomic/MeaningSource ExpressionSyntax?Example(s)
apapart df-ap 8156 Yes apadd1 8182, apne 8197
gwith "is a set" condition 1stvalg 5951, brtposg 6057, setsmsbasg 12281
seq3, sum3recursive sequence df-seq3 10003 Yes seq3-1 10023, fsum3 10946
iseq , isumrecursive sequence df-iseq 10002 Yes subject to change as this is being replaced by seq3

  • Community. The Metamath mailing list also covers the Intuitionistic Logic Explorer and is at:!forum/metamath.
  • (Contributed by Jim Kingdon, 24-Feb-2020.)

    Ref Expression
    conventions.1  |-  ph
    Ref Expression
    conventions  |-  ph

    Proof of Theorem conventions
    StepHypRef Expression
    1 conventions.1 1  |-  ph
    Colors of variables: wff set class
    This theorem is referenced by: (None)
      Copyright terms: Public domain W3C validator