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 (df-sum 12408) which denotes that index
variable ranges over when evaluating . Thus,
means 1/2 + 1/4 + 1/8 + ...
= 1 (geoihalfsum 12587). 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 4 (df-bi,
df-cleq, df-clel, df-clab) 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/mpeuni/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 8982,
proven by the preceding theorem ax1cn 8958.
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.
- Statements with hypotheses. Many theorems and some axioms,
such as ax-mp 8, have hypotheses that must be satisfied in order for
the conclusion to hold, in this case min and maj. When presented in
summarized form such as in the Theorem List (click on "Nearby theorems"
on the ax-mp 8 page), the hypotheses are connected with an ampersand and
separated from the conclusion with a big arrow, such as in "
& => ". These symbols are not
part of the Metamath language but are just informal notation meaning
"and" and "implies".
- 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 8982 (not ax1cn 8958) and ax-1ne0 8993 (not ax1ne0 8969), as these
are proven axioms for complex arithmetic. Thus, both
ax1cn 8958 and ax1ne0 8969 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 instead of sinh
for the hyperbolic sine.
- Axiom of choice.
The axiom of choice (df-ac 7931) 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 7164)
does not use the axiom of choice.
In some cases, the weaker axiom of countable choice (ax-cc 8249)
or axiom of dependent choice (ax-dc 8260) can be used instead.
- Variables.
Typically, Greek letters
( = phi, = psi, = chi, etc.),... are used for
propositional (wff) variables;
, , ,... for individual (set) variables;
and , , ,... 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 ".
- Biconditional ().
There are basically two ways to maximize the effectiveness of
biconditionals ():
you can either have one-directional simplifications of all theorems
that produce biconditionals, or you can have one-directional
simplifications of theorems that consume biconditionals.
Some tools (like Lean) follow the first approach, but set.mm follows
the second approach. Practically, this means that in set.mm, for
every theorem that uses an implication in the hypothesis, like
ax-mp 8, there is a corresponding version with a biconditional or a
reversed biconditional, like mpbi 200 or mpbir 201. We prefer this
second approach because the number of duplications in the second
approach is bounded by the size of the propositional calculus section,
which is much smaller than the number of possible theorems in all later
sections that produce biconditionals. So although theorems like
biimpi 187 are available, in most cases there is already a theorem that
combines it with your theorem of choice, like mpbir2an 887, sylbir 205,
or 3imtr4i 258.
- Substitution.
" " should be read "the wff that results from the
proper substitution of for in wff ." See df-sb 1656
and the related df-sbc 3106 and df-csb 3196.
- Is-a set.
" " should be read
"Class is a set (i.e. exists)."
This is a convenient convention based on
Definition 2.9 of [Quine] p. 19. See df-v 2902 and isset 2904.
- Converse.
"" should be read "converse of (relation) "
and is the same as the more standard notation R^{-1}
(the standard notation is ambiguous). See df-cnv 4827.
This can be used to define a subset, e.g., df-tan 12602 notates
"the set of values whose cosine is a nonzero complex number" as
.
- Function application.
"()" should be read "the value
of function at " and has the same meaning as the more
familiar but ambiguous notation F(x). For example,
(see cos0 12679). 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 5403.
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 6024).
For example, the in ; see 2p2e4 10031.
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
, , , and
(see wi 4, df-or 360, df-an 361, and df-bi 178 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 (see wel 1718),
equality (see df-cleq 2381),
subset (see df-ss 3278), and
less-than (see df-lt 8937). For the general definition
of a binary relation in the form , see df-br 4155.
For example, ( see 0lt1 9483) does not use parentheses.
- Unary minus.
The symbol is used to indicate a unary minus, e.g., .
It is specially defined because it is so commonly used.
See cneg 9225.
- 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 12595).
The function is then defined labelled df-NAME; definitions
are typically given using the maps-to notation (e.g., df-cos 12601).
Typically, there are other proofs such as its
closure labelled NAMEcl (e.g., coscl 12656), its
function application form labelled NAMEval (e.g., cosval 12652),
and at least one simple value (e.g., cos0 12679).
- Factorial.
The factorial function is traditionally a postfix operation,
but we treat it as a normal function applied in prefix form, e.g.,
; (df-fac 11495 and fac4 11502).
- 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
"" always means the value zero (df-0 8931), while
"" is the group identity element (df-0g 13655),
"" is the poset zero (df-p0 14396),
"" is the zero polynomial (df-0p 19430),
"" is the zero vector in a normed complex vector space
(df-0v 21926), and
"" is a class variable for use as a connective symbol
(this is used, for example, in p0val 14398).
There are other class variables used as connective symbols
where traditional notation would use ambiguous symbols, including
"", "", "", 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 (df-nn 9934) for the integer numbers starting
from 1, and (df-n0 10155) 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 10316, e.g.,
;;; (see 4001prm 13392 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 . 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 23.
A deduction hypothesis can have an indirect antecedent via definitions,
e.g., see lhop 19768. 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 11.
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.
- 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/mpeuni/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 3724,
which works in certain cases in set theory. We also
sometimes use dedhb 3048.
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 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 21560.
- 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 in df-recs 6570,
in df-rdg 6605, seq_{𝜔} in df-seqom 6642, and
in df-seq 11252.
These have characteristic function and initial value .
(_{g} in df-gsum 13656 isn't really designed for arbitrary recursion,
but you could do it with the right magma.)
The logically primary one is df-recs 6570, but for the "average user"
the most useful one is probably df-seq 11252- 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 13399.
- 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 7154 is the first lemma for sbth 7164. 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., "é" for "é").
- Information on syntax, axioms, and definitions.
For a hyperlinked list of syntax, axioms, and definitions, see
http://us.metamath.org/mpeuni/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.
Naming conventions
Every statement has a unique identifying label.
We use various label naming conventions to provide
easy-to-remember hints about their contents.
Labels are not a 1-to-1 mapping, because that would create
long names that would be difficult to remember and tedious to type.
Instead, label names are relatively short while
suggesting their purpose.
Names are occasionally changed to make them more consistent or
as we find better ways to name them.
Here are a few of the label naming conventions:
- Axioms, definitions, and wff syntax.
As noted earlier, axioms are named "ax-NAME",
proofs of proven axioms are named "axNAME", and
definitions are named "df-NAME".
Wff syntax declarations have labels beginning with "w"
followed by short fragment suggesting its purpose.
- Hypotheses.
Hypotheses have the name of the final axiom or theorem, followed by
".", followed by a unique id.
- Common names.
If a theorem has a well-known name, that name (or a short version of it)
is sometimes used directly. Examples include
barbara 2336 and stirling 27507.
- Syntax label fragments.
Most theorems are named using syntax label fragments.
Almost every syntactic construct has a definition labelled "df-NAME",
and NAME normally is the syntax label fragment.
For example, the difference construct
is defined in df-dif 3267, and thus its syntax label fragment is "dif".
Similarly, the singleton construct
has syntax label fragment "sn"
(because it is defined in df-sn 3764),
the subclass (subset) relation has "ss"
(because it is defined in df-ss 3278), and
the pair construct has "pr" (df-pr 3765).
Theorem names are often a concatenation of the syntax label fragments
(omitting variables).
For example, a theorem about
involves a difference ("dif")
of a subset ("ss"), and thus is named difss 3418.
Digits are used to represent themselves.
Suffixes (e.g., with numbers) are sometimes used to distinguish
multiple theorems that would otherwise produce the same label.
- Phantom definitions.
In some cases there are common label fragments for something that
could be in a definition, but for technical reasons is not.
The is-element-of (is member of) construct
does not have a df-NAME definition; in this case its syntax
label fragment is "el".
Thus, because the theorem beginning with
uses is-element-of ("el")
of a difference ("dif") of a singleton ("sn"), it is named eldifsn 3871.
An "n" is often used for negation (), e.g., nan 564.
- Exceptions.
Sometimes there is a definition df-NAME but the
label fragment is not the NAME part.
The table below attempts to list all such cases and marks them in bold.
For example, label fragment
"cn" represents complex numbers (even though its definition
is in df-c 8930) and "re" represents real numbers .
The empty set often uses fragment 0, even though it is defined
in df-nul 3573.
Syntax construct usually uses the fragment "add"
(which is consistent with df-add 8935),
but "p" is used as the fragment for constant theorems.
Equality often uses "e" as the fragment.
As a result, "two plus two equals four" is named 2p2e4 10031.
- Other markings.
In labels we sometimes use "com" for "commutative",
"ass" for "associative", "rot" for "rotation",
and "di" for "distributive".
- Principia Mathematica.
Proofs of theorems from Principia Mathematica often use a different
naming convention.
They are instead often named "pm" followed by its identifier.
For example, Theorem *2.27 of [WhiteheadRussell] p. 104 is named
pm2.27 37.
- Closures and values.
As noted above,
if a function df-NAME is defined, there is typically a proof
of its value named "NAMEval" and its closure named "NAMEcl".
E.g., for cosine (df-cos 12601) we have
value cosval 12652 and closure coscl 12656.
- Special cases.
Sometimes syntax and related markings are
insufficient to distinguish different theorems.
For example, there are over 100 different
implication-exclusive theorems.
These are then grouped in a more ad-hoc way that attempts to
make their distinctions clearer.
These often use abbreviations such as "mp" for "modus ponens",
"syl" for syllogism, and "id" for "identity".
It's especially hard to give good names in the propositional
calculus section because there are so few primitives. However,
in most cases this is not a serious problem. There are a few
very common theorems like ax-mp 8 and syl 16 that you will have no
trouble remembering, a few theorem series like syl*anc and simp*
that you can use parametrically, and a few other useful glue things
for destructuring 'and's and 'or's (see natded 21560 for a list),
and that's about all you need for most things. As for the rest,
you can just assume that if it involves three or less connectives
we probably already have a proof, and searching for it will give
you the name.
- Suffixes.
We sometimes suffix with "v" the label of a theorem
eliminating a hypothesis such as in 19.21 1804 via the use of
distinct variable conditions combined with nfv 1626. 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 2245 derived from df-eu 2243. 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 16) -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 4646 vs. uniexg 4647.
A theorem name is suffixed with "ALT" if it's an alternative
less-preferred proof of a theorem.
- Reuse.
When creating a new theorem or axiom, try to reuse abbreviations
used elsewhere. A comment should explain the first use of an
abbreviation.
The following table shows some commonly-used abbreviations in labels,
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.
This is not a complete list of abbreviations, though
we do want this to eventually be a complete list of exceptions.
Abbreviation | Mnenomic | Source |
Expression | Syntax? | Example(s) |
add | add (see "p") | df-add 8935 |
| Yes |
addcl 9006, addcom 9185, addass 9011 |
ALT | alternative/less preferred (suffix) | |
| No | |
an | and | df-an 361 |
| Yes |
anor 476, iman 414, imnan 412 |
ass | associative | |
| No | biass 349, orass 511, mulass 9012 |
bi | biconditional | df-bi 178 |
| Yes | impbid 184 |
cn | complex numbers | df-c 8930 |
| Yes | nnsscn 9938, nncn 9941 |
com | commutative | |
| No | orcom 377, bicomi 194, eqcomi 2392 |
d | deduction form | |
| No | idd 22, impbid 184 |
di, distr | distributive | |
| No |
andi 838, imdi 353, ordi 835, difindi 3539, ndmovdistr 6176 |
dif | difference | df-dif 3267 |
| Yes |
difss 3418, difindi 3539 |
div | division | df-div 9611 |
| Yes |
divcl 9617, divval 9613, divmul 9614 |
e, eq | equals | df-cleq 2381 |
| Yes | 2p2e4 10031, uneqri 3433 |
el | element of | |
| Yes |
eldif 3274, eldifsn 3871, elssuni 3986 |
f | "not free in" (suffix) | |
| No | |
g | more general (suffix); eliminates "is a set"
hypothsis | |
| No | uniexg 4647 |
id | identity | |
| No | |
idm | idempotent | |
| No | anidm 626, tpidm13 3850 |
im, imp | implication (label often omitted) |
df-im 11834 | | Yes |
iman 414, imnan 412, impbidd 182 |
in | intersection | df-in 3271 |
| Yes |
elin 3474, incom 3477 |
is... | is (something a) ...? | |
| No |
isrng 15596 |
mp | modus ponens | ax-mp 8 |
| No | mpd 15, mpi 17 |
mul | multiplication (see "t") | df-mul 8936 |
| Yes |
mulcl 9008, divmul 9614, mulcom 9010, mulass 9012 |
n, not | not | |
| Yes |
nan 564, notnot2 106 |
ne0 | not equal to zero (see n0) | |
| No |
negne0d 9342, ine0 9402, gt0ne0 9426 |
nn | natural numbers | df-nn 9934 |
| Yes | nnsscn 9938, nncn 9941 |
n0 | not the empty set (see ne0) | |
| No | n0i 3577, vn0 3579, ssn0 3604 |
or | or | df-or 360 |
| Yes |
orcom 377, anor 476 |
p | plus (see "add"), for all-constant
theorems |
df-add 8935 |
| Yes |
3p2e5 10044 |
pm | Principia Mathematica | |
| No | pm2.27 37 |
pr | pair | df-pr 3765 |
| Yes |
elpr 3776, prcom 3826, prid1g 3854, prnz 3867 |
q | (quotients) | df-q 10508 |
| Yes |
elq 10509 |
re | real numbers | df-r 8934 |
| Yes | recn 9014, 0re 9025 |
rng | ring | df-rng 15591 |
| Yes |
rngidval 15594, isrng 15596, rnggrp 15597 |
rot | rotation | |
| No | 3anrot 941, 3orrot 942 |
s | eliminates need for syllogism (suffix) |
| | No | |
sn | singleton | df-sn 3764 |
| Yes | eldifsn 3871 |
ss | subset | df-ss 3278 |
| Yes | difss 3418 |
sub | subtract | df-sub 9226 |
| Yes |
subval 9230, subaddi 9320 |
syl | syllogism | syl 16 |
| No | 3syl 19 |
t |
times (see "mul"), for all-constant theorems |
df-mul 8936 |
| Yes |
3t2e6 10061 |
tp | triple | df-tp 3766 |
| Yes |
eltpi 3796, tpeq1 3836 |
un | union | df-un 3269 |
| Yes |
uneqri 3433, uncom 3435 |
v | distinct variable conditions used when
a not-free hypothesis (suffix) |
| | No | spimv 1954 |
xr | eXtended reals | df-xr 9058 |
| Yes | ressxr 9063, rexr 9064, 0xr 9065 |
z | (integers, from German Zahlen) |
df-z 10216 | | Yes |
elz 10217, zcn 10220 |
0, z |
slashed zero (empty set) (see n0) | df-nul 3573 |
| Yes |
n0i 3577, vn0 3579; snnz 3866, prnz 3867 |
Distinctness or freeness
Here are some conventions that address distinctness or freeness of a
variable:
- is read " is not free in (wff) ";
see df-nf 1551 (whose description has some important technical
details). Similarly, is read is not free in (class)
, see df-nfc 2513.
- "$d x y $." should be read "Assume x and y are distinct
variables."
- "$d x $." should be read "Assume x does not occur in phi $."
Sometimes a theorem is proved using
(df-nf 1551) in place of
"$d $." when a more general result is desired;
ax-17 1623 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 2245 from df-eu 2243.
- "$d x A $." should be read "Assume x is not a variable occurring in
class A."
- "$d x A $. $d x ps $. $e |- $."
is an idiom
often used instead of explicit substitution, meaning "Assume psi results
from the proper substitution of A for x in phi."
- " " 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.) |