MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  conventions Unicode version

Theorem conventions 3
Description: Here are some of the conventions we use in the Metamath Proof Explorer (aka "set.mm"), and how they correspond to typical textbook language (skipping the many cases where they're identical):

  • Notation. Where possible, the notation attempts to conform to modern conventions, with variations due to our choice of the axiom system or to make proofs shorter. However, our notation is strictly sequential (left-to-right). For example, summation is written in the form  sum_ k  e.  A B (df-sum 12125) which denotes that index variable  k ranges over  A when evaluating  B. Thus,  sum_ k  e.  NN  ( 1  /  ( 2 ^ k ) )  =  1 means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 12301). Also, the method of definition, the axioms for predicate calculus, and the development of substitution are somewhat different from those found in standard texts. For example, the expressions for the axioms were designed for direct derivation of standard results without excessive use of metatheorems. (See Theorem 9.7 of [Megill] p. 448 for a rigorous justification.) The notation is usually explained in more detail when first introduced.
  • Axiomatic assertions ($a). All axiomatic assertions ($a statements) starting with "  |-" have labels starting with "ax-" (axioms) or "df-" (definitions). A statement with a label starting with "ax-" corresponds to what is traditionally called an axiom. A statement with a label starting with "df-" introduces new symbols or a new relationship among symbols that can be eliminated; they always extend the definition of a wff or class. Metamath blindly treats $a statements as new given facts but does not try to justify them. The mmj2 program will justify the definitions as sound, except for 5 (df-bi, df-cleq, df-clel, df-clab, df-sbc) that require a more complex metalogical justification by hand.
  • Proven axioms. In some cases we wish to treat an expression as an axiom in later theorems, even though it can be proved. For example, we derive the postulates or axioms of complex arithmetic as theorems of ZFC set theory. For convenience, after deriving the postulates we re-introduce them as new axioms on top of set theory. This lets us easily identify which axioms are needed for a particular complex number proof, without the obfuscation of the set theory used to derive them. For more, see http://us.metamath.org/mpegif/mmcomplex.html. When we wish to use a previously-proven assertion as an axiom, our convention is that we use the regular "ax-NAME" label naming convention to define the axiom, but we precede it with a proof of the same statement with the label "axNAME" . An example is complex arithmetic axiom ax-1cn 8763, proven by the preceding theorem ax1cn 8739. The metamath.exe program will warn if an axiom does not match the preceding theorem that justifies it if the names match in this way.
  • Definitions (df-...). We encourage definitions to include hypertext links to proven examples.
  • Discouraged use and modification. If something should only be used in limited ways, it is marked with "(New usage is discouraged.)". This is used, for example, when something can be constructed in more than one way, and we do not want later theorems to depend on that specific construction. This marking is also used if we want later proofs to use proven axioms. For example, we want later proofs to use ax-1cn 8763 (not ax1cn 8739) and ax-1ne0 8774 (not ax1ne0 8750), as these are proven axioms for complex arithmetic. Thus, both ax1cn 8739 and ax1ne0 8750 are marked as "(New usage is discouraged.)". In some cases a proof should not normally be changed, e.g., when it demonstrates some specific technique. These are marked with "(Proof modification is discouraged.)".
  • New definitions infrequent. Typically we are minimalist when introducing new definitions; they are introduced only when a clear advantage becomes apparent for reducing the number of symbols, shortening proofs, etc. We generally avoid the introduction of gratuitous definitions because each one requires associated theorems and additional elimination steps in proofs. For example, we use  < and  <_ for inequality expressions, and use  ( ( sin `  ( _i  x.  A ) )  /  _i ) instead of  (sinh `  A ) for the hyperbolic sine.
  • Axiom of choice. The axiom of choice (df-ac 7711) is widely accepted, and ZFC is the most commonly-accepted fundamental set of axioms for mathematics. However, there have been and still are some lingering controversies about the Axiom of Choice. Therefore, where a proof does not require the axiom of choice, we prefer that proof instead. E.g., our proof of the Schroeder-Bernstein Theorem (sbth 6949) does not use the axiom of choice. In some cases, the weaker axiom of countable choice (ax-cc 8029) or axiom of dependent choice (ax-dc 8040) can be used instead.
  • Variables. Typically, Greek letters ( ph = phi,  ps = psi,  ch = chi, etc.),... are used for propositional (wff) variables;  x,  y,  z,... for individual (set) variables; and  A,  B,  C,... for class variables.
  • Turnstile. " |-", meaning "It is provable that," is the first token of all assertions and hypotheses that aren't syntax constructions. This is a standard convention in logic. For us, it also prevents any ambiguity with statements that are syntax constructions, such as "wff  -.  ph".
  • Substitution. " [ y  /  x ] ph" should be read "the wff that results from the proper substitution of  y for  x in wff  ph." See df-sb 1884 and the related df-sbc 2967 and df-csb 3057.
  • Is-a set. " A  e.  _V" should be read "Class  A is a set (i.e. exists)." This is a convenient convention based on Definition 2.9 of [Quine] p. 19. See df-v 2765 and isset 2767.
  • Converse. " `' R" should be read "converse of (relation)  R" and is the same as the more standard notation R^{-1} (the standard notation is ambiguous). See df-cnv 4677. This can be used to define a subset, e.g., df-tan 12316 notates "the set of values whose cosine is a nonzero complex number" as  ( `' cos " ( CC  \  { 0 } ) ).
  • Function application. "( F `  x)" should be read "the value of function  F at  x" and has the same meaning as the more familiar but ambiguous notation F(x). For example,  ( cos `  0 )  =  1 (see cos0 12393). The left apostrophe notation originated with Peano and was adopted in Definition *30.01 of [WhiteheadRussell] p. 235, Definition 10.11 of [Quine] p. 68, and Definition 6.11 of [TakeutiZaring] p. 26. See df-fv 4689. In the ASCII (input) representation there are spaces around the grave accent; there is a single accent when it is used directly, and it is doubled within comments.
  • Infix and parentheses. When a function that takes two classes and produces a class is applied as part of an infix expression, the expression is always surrounded by parentheses (see df-ov 5795). For example, the  + in  ( 2  +  2 ); see 2p2e4 9810. Function application is itself an example of this. Similarly, predicate expressions in infix form that take two or three wffs and produce a wff are also always surrounded by parentheses, such as  ( ph  ->  ps ),  ( ph  \/  ps ),  ( ph  /\  ps ), and  ( ph  <->  ps ) (see wi 6, df-or 361, df-an 362, and df-bi 179 respectively). In contrast, a binary relation (which compares two classes and produces a wff) applied in an infix expression is not surrounded by parentheses. This includes set membership  A  e.  B (see wel 1622), equality  A  =  B (see df-cleq 2251), subset  A  C_  B (see df-ss 3141), and less-than  A  <  B (see df-lt 8718). For the general definition of a binary relation in the form  A R B, see df-br 3998. For example,  0  <  1 ( see 0lt1 9264) does not use parentheses.
  • Unary minus. The symbol  -u is used to indicate a unary minus, e.g.,  -u 1. It is specially defined because it is so commonly used. See cneg 9006.
  • Function definition. Functions are typically defined by first defining the constant symbol (using $c) and declaring that its symbol is a class with the label cNAME (e.g., ccos 12309). The function is then defined labelled df-NAME; definitions are typically given using the maps-to notation (e.g., df-cos 12315). Typically there are other proofs such as its closure labelled NAMEcl (e.g., coscl 12370), its function application form labelled NAMEval (e.g., cosval 12366), and at least one simple value (e.g., cos0 12393).
  • Factorial. The factorial function is traditionally a postfix operation, but we treat it as a normal function applied in prefix form, e.g.,  ( ! `  4 )  = ; 2 4 (df-fac 11256 and fac4 11263).
  • Unambiguous symbols. A given symbol has a single unambiguous meaning in general. Thus, where the literature might use the same symbol with different meanings, here we use different (variant) symbols for different meanings. These variant symbols often have suffixes, subscripts, or underlines to distinguish them. For example, here " 0" always means the value zero (df-0 8712), while " 0g" is the group identity element (df-0g 13367), " 0." is the poset zero (df-p0 14108), " 0 p" is the zero polynomial (df-0p 18988), " 0vec" is the zero vector in a normed complex vector space (df-0v 21115), and " .0." is a class variable for use as a connective symbol (this is used, for example, in p0val 14110). There are other class variables used as connective symbols where traditional notation would use ambiguous symbols, including " .1.", " .+", " .*", and " .||". These symbols are very similar to traditional notation, but because they are different symbols they eliminate ambiguity.
  • Natural numbers. There are different definitions of "natural" numbers in the literature. We use  NN (df-n 9715) for the integer numbers starting from 1, and  NN0 (df-n0 9934) for the set of nonnegative integers starting at zero.
  • Decimal numbers. Numbers larger than ten are often expressed in base 10 using the decimal constructor df-dec 10093, e.g., ;;; 4 0 0 1 (see 4001prm 13106 for a proof that 4001 is prime).
  • Theorem forms. We often call a theorem a "deduction" whenever the conclusion and all hypotheses are each prefixed with the same antecedent  ph  ->. Deductions are often the preferred form for theorems because they allow us to easily use the theorem in places where (in traditional textbook formalizations) the standard Deduction Theorem would be used. See, for example, a1d 24. A deduction hypothesis can have an indirect antecedent via definitions, e.g., see lhop 19326. Deductions have a label suffix of "d" if there are other forms of the same theorem. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 12. Finally, a "tautology" would be the form with no hypotheses, and its label would have no suffix. For example, see pm2.43 49, pm2.43i 45, and pm2.43d 46.
  • Label names. Every statement has a unique identifying label; here are few additional label name conventions. Hypotheses have the name of final axiom or theorem, followed by ".", followed by a unique id. We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as  F/ x ph in 19.21 1771 via the use of distinct variable conditions combined with nfv 1629. Conversely, we sometimes suffix with "f" the label of a theorem introducing such a hypothesis to eliminate the need for the distinct variable condition; e.g. euf 2124 derived from df-eu 2122. The "f" stands for "not free in" which is less restrictive than "does not occur in." We sometimes suffix with "s" the label of an inference that manipulates an antecedent, leaving the consequent unchanged. The "s" means that the inference eliminates the need for a syllogism (syl 17) -type inference in a proof. When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for "more general") as in uniex 4488 vs. uniexg 4489. Label names are relatively short while suggesting their purpose, e.g., 2p2e4 9810 is the label for  ( 2  +  2 )  =  4 because it is "2 plus 2 equals 4". When creating a new theorem or axiom, try to reuse abbreviations used elsewhere. A comment should explain the first use of an abbreviation.
  • Deduction theorem. The Deduction Theorem is a metalogical theorem that provides an algorithm for constructing a proof of a theorem from the proof of its corresponding deduction. In ordinary mathematics, no one actually carries out the algorithm, because (in its most basic form) it involves an exponential explosion of the number of proof steps as more hypotheses are eliminated. Instead, in ordinary mathematics the Deduction Theorem is invoked simply to claim that something can be done in principle, without actually doing it. For more details, see http://us.metamath.org/mpegif/mmdeduction.html. The Deduction Theorem is a metalogical theorem that cannot be applied directly in metamath, and the explosion of steps would be a problem anyway, so alternatives are used. One alternative we use sometimes is the "weak deduction theorem" dedth 3580, which works in certain cases in set theory. We also sometimes use dedhb 2910. However, the primary mechanism we use today for emulating the deduction theorem is to write proofs in the deduction theorem form (aka "deduction style") described earlier; the prefixed  ph  -> mimics the context in a deduction proof system. In practice this mechanism works very well. This approach is described in the deduction form and natural deduction page; a list of translations for common natural deduction rules is given in natded 4.
  • Recursion. We define recursive functions using various "recursion constructors". These allow us to define, with compact direct definitions, functions that are usually defined in textbooks with indirect self-referencing recursive definitions. This produces compact definition and much simpler proofs, and greatly reduces the risk of creating unsound definitions. Examples of recursion constructors include recs ( F ) in df-recs 6356,  rec ( F ,  I ) in df-rdg 6391, seq𝜔 ( F ,  I ) in df-seqom 6428, and  seq  M (  .+  ,  F ) in df-seq 11014. These have characteristic function  F and initial value  I. ( gsumg in df-gsum 13368 isn't really designed for arbitrary recursion, but you could do it with the right magma.) The logically primary one is df-recs 6356, but for the "average user" the most useful one is probably df-seq 11014- provided that a countable sequence is sufficient for the recursion.
  • Extensible structures. Mathematics includes many structures such as ring, group, poset, etc. We define an "extensible structure" which is then used to define group, ring, poset, etc. This allows theorems from more general structures (groups) to be reused for more specialized structures (rings) without having to reprove them. See df-struct 13113.
  • Organizing proofs. Humans have trouble understanding long proofs. It is often preferable to break longer proofs into smaller parts (just as with traditional proofs). In Metamath this is done by creating separate proofs of the separate parts. A proof with the sole purpose of supporting a final proof is a lemma; the naming convention for a lemma is the final proof's name followed by "lem", and a number if there is more than one. E.g., sbthlem1 6939 is the first lemma for sbth 6949. Also, consider proving reusable results separately, so that others will be able to easily reuse that part of your work.
  • Hypertext links. We strongly encourage comments to have many links to related material, with accompanying text that explains the relationship. These can help readers understand the context. Links to other statements, or to HTTP/HTTPS URLs, can be inserted in ASCII source text by prepending a space-separated tilde. When metamath.exe is used to generate HTML it automatically inserts hypertext links for syntax used (e.g., every symbol used), every axiom and definition depended on, the justification for each step in a proof, and to both the next and previous assertion.
  • Bibliography references. Please include a bibliographic reference to any external material used. A name in square brackets in a comment indicates a bibliographic reference. The full reference must be of the form KEYWORD IDENTIFIER? NOISEWORD(S)* [AUTHOR(S)] p. NUMBER - note that this is a very specific form that requires a page number. There should be no comma between the author reference and the "p." (a constant indicator). Whitespace, comma, period, or semicolon should follow NUMBER. An example is Theorem 3.1 of [Monk1] p. 22, The KEYWORD, which is not case-sensitive, must be one of the following: Axiom, Chapter, Compare, Condition, Corollary, Definition, Equation, Example, Exercise, Figure, Item, Lemma, Lemmas, Line, Lines, Notation, Part, Postulate, Problem, Property, Proposition, Remark, Rule, Scheme, Section, or Theorem. The IDENTIFIER is optional, as in for example "Remark in [Monk1] p. 22". The NOISEWORDS(S) are zero or more from the list: from, in, of, on. The AUTHOR(S) must be present in the file identified with the htmlbibliography assignment (e.g. mmset.html) as a named anchor (NAME=). If there is more than one document by the same author(s), add a numeric suffix (as shown here). The NUMBER is a page number, and may be any alphanumeric string such as an integer or Roman numeral. Note that we require page numbers in comments for individual $a or $p statements. We allow names in square brackets without page numbers (a reference to an entire document) in heading comments. If this is a new reference, please also add it to the "Bibliography" section of mmset.html. (The file mmbiblio.html is automatically rebuilt, e.g., using the metamath.exe "write bibliography" command.)
  • Input format. The input is in ASCII with two-space indents. Tab characters are not allowed. Use embedded math comments or HTML entities for non-ASCII characters (e.g., "&eacute;" for "é").
  • Information on syntax, axioms, and definitions. For a hyperlinked list of syntax, axioms, and definitions, see http://us.metamath.org/mpegif/mmdefinitions.html. If you have questions about a specific symbol or axiom, it is best to go directly to its definition to learn more about it. The generated HTML for each theorem and axiom includes hypertext links to each symbol's definition.

Here are some conventions that address distinctness or freeness of a variable:

  •  F/ x ph is read "  x is not free in (wff)  ph"; see df-nf 1540. Similarly,  F/_ x A is read  x is not free in (class)  A, see df-nfc 2383.
  • "$d x y $." should be read "Assume x and y are distinct variables."
  • "$d x  ph $." should be read "Assume x does not occur in phi $." Sometimes a theorem is proved using  F/ x ph (df-nf 1540) in place of "$d  x ph $." when a more general result is desired; ax-17 1628 can be used to derive the $d version. For an example of how to get from the $d version back to the $e version, see the proof of euf 2124 from df-eu 2122.
  • "$d x A $." should be read "Assume x is not a variable occurring in class A."
  • "$d x A $. $d x ps $. $e |-  ( x  =  A  ->  ( ph  <->  ps ) ) $." is an idiom often used instead of explicit substitution, meaning "Assume psi results from the proper substitution of A for x in phi."
  • "  |-  ( -.  A. x x  =  y  ->  ..." occurs early in some cases, and should be read "If x and y are distinct variables, then..." This antecedent provides us with a technical device (called a "distinctor" in Section 7 of [Megill] p. 444) to avoid the need for the $d statement early in our development of predicate calculus, permitting unrestricted substitutions as conceptually simple as those in propositional calculus. However, the $d eventually becomes a requirement, and after that this device is rarely used.

Here is more information about our processes for checking and contributing to this work:

  • Multiple verifiers. This entire file is verified by multiple independently-implemented verifiers when it is checked in, giving us extremely high confidence that all proofs follow from the assumptions. The checkers also check for various other problems such as overly long lines.
  • Rewrapped line length. The input file routinely has its text wrapped using metamath 'read set.mm' 'save proof */c/f' 'write source set.mm/rewrap' (so please do the same).
  • Discouraged information. A separate file named "discouraged" lists all discouraged statements and uses of them, and this file is checked. If you change the use of discouraged things, you will need to change this file. This makes it obvious when there is a change to anything discouraged (triggering further review).
  • Proposing specific changes. Please propose specific changes as pull requests (PRs) against the "develop" branch of set.mm, at: https://github.com/metamath/set.mm/tree/develop
  • Community. We encourage anyone interested in Metamath to join our mailing list: https://groups.google.com/forum/#!forum/metamath.

(Contributed by DAW, 27-Dec-2016.)

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

Proof of Theorem conventions
StepHypRef Expression
1 conventions.1 1  |-  ph
Colors of variables: wff set class
  Copyright terms: Public domain W3C validator