HomeUnicode version.
| Home |
Metamath Proof Explorer | < Wrap Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-11415) |
Hilbert Space Explorer
(11416-13002) |
Users' Mathboxes
(13003-19465) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Pre-logic | ||
| Dummy link theorem for assisting proof development | ||
| Theorem | dummylink 1 |
(Note: This theorem will never appear in a completed proof and can be
ignored if you are using this database to learn logic - please start
with the next statement, wn 2.)
This is a technical theorem to assist proof development. It provides a temporary way to add an independent subproof to a proof under development, for later assignment to a normal proof step. The Metamath program's Proof Assistant requires proofs to be developed backwards from the conclusion with no gaps, and it has no mechanism that lets the user to work on isolated subproofs. This theorem provides a workaround for this limitation. It can be inserted at any point in a proof to allow an independent subproof to be developed on the side, for later use as part of the final proof. Instructions: (1) Assign this theorem to any unknown step in the proof. Typically, the last unknown step is the most convenient, since 'assign last' can be used. This step will be replicated in hypothesis dummylink.1, from where the development of the main proof can continue. (2) Develop the independent subproof backwards from hypothesis dummylink.2. If desired, use a 'let' command to pre-assign the conclusion of the independent subproof to dummylink.2. (3) After the independent subproof is complete, use 'improve all' to assign it automatically to an unknown step in the main proof that matches it. (4) After the entire proof is complete, use 'minimize */n/b/e 3syl,we?,wsb' to clean up (discard) all dummylink references automatically. This theorem was originally designed to assist importing partially completed Proof Worksheets from Mel O'Cat's mmj2 Proof Assistant GUI, but it can also be useful on its own. Interestingly, this "theorem" - or more precisely, inference - requires no axioms for its proof. |
     | ||
| Propositional calculus | ||
| Recursively define primitive wffs for propositional calculus | ||
| Syntax | wn 2 |
If is a wff, so
is  or "not ." Part of the
recursive definition of a wff (well-formed formula). In classical logic
(which is our logic), a wff is interpreted as either true or false. So if
is true,
then is false; if is false, then
is true.
Traditionally, Greek letters are used to represent
wffs, and we follow this convention. In propositional calculus, we define
only wffs built up from other wffs, i.e. there is no starting or
"atomic"
wff. Later, in predicate calculus, we will extend the basic wff
definition by including atomic wffs (weq 1616 and wel 1618).
|
 | ||
| Syntax | wi 3 |
If and are wff's, so is    or " implies
." Part of
the recursive definition of a wff. The resulting wff
is (interpreted as) false when is true and is false; it is
true otherwise. (Think of the truth table for an OR gate with input
connected
through an inverter.) The left-hand wff is called the
antecedent, and the right-hand wff is called the consequent. In the case
of
 , the
middle may be
informally called
either an antecedent or part of the consequent depending on context.
|
| | ||
| The axioms of propositional calculus | ||
| Axiom | ax-1 4 |
Axiom Simp. Axiom A1 of [Margaris] p.
49. One of the 3 axioms of
propositional calculus. The 3 axioms are also given as Definition 2.1 of
[Hamilton] p. 28. This axiom is called
Simp or "the principle of
simplification" in Principia Mathematica (Theorem *2.02 of
[WhiteheadRussell] p. 100)
because "it enables us to pass from the joint
assertion of
and to the assertion
of simply."
General remarks: Propositional calculus (axioms ax-1 4 through ax-3 6 and rule ax-mp 7) can be thought of as asserting formulas that are universally "true" when their variables are replaced by any combination of "true" and "false." Propositional calculus was first formalized by Frege in 1879, using as his axioms (in addition to rule ax-mp 7) the wffs ax-1 4, ax-2 5, pm2.04 72, con3 158, notnot2 135, and notnot1 149. Around 1930, Lukasiewicz simplified the system by eliminating the third (which follows from the first two, as you can see by looking at the proof of pm2.04 72) and replacing the last three with our ax-3 6. (Thanks to Ted Ulrich for this information.) The theorems of propositional calculus are also called tautologies. Tautologies can be proved very simply using truth tables, based on the true/false interpretation of propositional calculus. To do this, we assign all possible combinations of true and false to the wff variables and verify that the result (using the rules described in wi 3 and wn 2) always evaluates to true. This is called the semantic approach. Our approach is called the syntactic approach, in which everything is derived from axioms. A metatheorem called the Completeness Theorem for Propositional Calculus shows that the two approaches are equivalent and even provides an algorithm for automatically generating syntactic proofs from a truth table. Those proofs, however, tend to be long, and the much shorter proofs that we show here were found manually. Truth tables grow exponentially with the number of variables, but it is unknown if the same is true of proofs - an answer to this would resolve the P=NP conjecture in complexity theory. |
| | ||
| Axiom | ax-2 5 | Axiom Frege. Axiom A2 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known as Frege in the literature. It is also proved as Theorem *2.77 of [WhiteheadRussell] p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 428. |
|
| ||
| Axiom | ax-3 6 | Axiom Transp. Axiom A3 of [Margaris] p. 49. One of the 3 axioms of propositional calculus. It swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This axiom is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103). We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning. |
| | ||
| Axiom | ax-mp 7 |
Rule of Modus Ponens. The postulated inference rule of propositional
calculus. See e.g. Rule 1 of [Hamilton] p. 73. The rule says, "if
is true,
and implies , then must also be
true." This rule is sometimes called "detachment," since
it detaches
the minor premise from the major premise.
Note: In some web page displays such as the Statement List, the symbols "&" and "=>" informally indicate the relationship between the hypotheses and the assertion (conclusion), abbreviating the English words "and" and "implies." They are not part of the formal language. |
| | ||
| Logical implication | ||
| Theorem | a1i 8 | Inference derived from axiom ax-1 4. See a1d 18 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 31. |
| | ||
| Theorem | a1i12 9 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) |
| | ||
| Theorem | a2i 10 | Inference derived from axiom ax-2 5. |
| | ||
| Theorem | mpd 11 | A modus ponens deduction. |
| | ||
| Theorem | imim2i 12 | Inference adding common antecedents in an implication. |
| | ||
| Theorem | syl 13 |
An inference version of the transitive laws for implication imim2 29
and
imim1 58, which Russell and Whitehead call "the
principle of the
syllogism...because...the syllogism in Barbara is derived from
them"
(quote after Theorem *2.06 of [WhiteheadRussell] p. 101). Some authors
call this law a "hypothetical syllogism." (The proof was
shortened by
O'Cat, 20-Oct-2011.) (The proof was shortened by Wolf Lammen,
26-Jul-2012.)
(A bit of trivia: this is the most commonly referenced assertion in our database. In second place is ax-mp 7, followed by visset 2572, bitri 306, imp 489, and ex 494. The Metamath program command 'show usage' shows the number of references.) |
| | ||
| Theorem | sylOLD 14 | Obsolete previous proof of syl 13. |
| | ||
| Theorem | id 15 | Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 16. (The proof was shortened by Stefan Allan, 20-Mar-2006.) |
| | ||
| Theorem | id1 16 | Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. This version is proved directly from the axioms for demonstration purposes. This proof is a popular example in the literature and is identical, step for step, to the proofs of Theorem 1 of [Margaris] p. 51, Example 2.7(a) of [Hamilton] p. 31, Lemma 10.3 of [BellMachover] p. 36, and Lemma 1.8 of [Mendelson] p. 36. It is also "Our first proof" in Hirst and Hirst's A Primer for Logic and Proof p. 16 (PDF p. 22) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. For a shorter version of the proof that takes advantage of previously proved theorems, see id 15. |
| | ||
| Theorem | idd 17 | Principle of identity with antecedent. |
| | ||
| Theorem | a1d 18 |
Deduction introducing an embedded antecedent. (The proof was revised by
Stefan Allan, 20-Mar-2006.)
Naming convention: We often call a theorem a
"deduction" and suffix
its label with "d" whenever the hypotheses and conclusion are
each
prefixed with the same antecedent. This allows us to use the theorem in
places where (in traditional textbook formalizations) the standard
Deduction Theorem would be used; here |
| | ||
| Theorem | a2d 19 | Deduction distributing an embedded antecedent. |
 | ||
| Theorem | mpdd 20 | A nested modus ponens deduction. |
|
| ||
| Theorem | mpid 21 | A nested modus ponens deduction. |
|
| ||
| Theorem | pm2.43a 22 | Inference absorbing redundant antecedent. (The proof was shortened by O'Cat, 28-Nov-2008.) |
| | ||
| Theorem | sylcom 23 | Syllogism inference with commutation of antecedents. (The proof was shortened by O'Cat, 2-Feb-2006.) (The proof was shortened by Stefan Allan, 23-Feb-2006.) |
|
| ||
| Theorem | syl5com 24 | Syllogism inference with commuted antecedents. |
| | ||
| Theorem | syl5comOLD 25 | Syllogism inference with commuted antecedents. |
|
| ||
| Theorem | com12 26 | Inference that swaps (commutes) antecedents in an implication. (The proof was shortened by Wolf Lammen, 4-Aug-2012.) |
|
| ||
| Theorem | com12OLD 27 | Inference that swaps (commutes) antecedents in an implication. |
|
| ||
| Theorem | imim2d 28 | Deduction adding nested antecedents. |
| | ||
| Theorem | imim2 29 | A closed form of syllogism (see syl 13). Theorem *2.05 of [WhiteheadRussell] p. 100. (The proof was shortened by Wolf Lammen, 6-Sep-2012.) |
| | ||
| Theorem | imim2OLD 30 | A closed form of syllogism (see syl 13). Theorem *2.05 of [WhiteheadRussell] p. 100. |
| | ||
| Theorem | syld 31 |
Syllogism deduction. (The proof was shortened by O'Cat, 19-Feb-2008.)
(The proof was shortened by Wolf Lammen, 3-Aug-2012.)
Notice that syld 31 has the same form as syl 13 with
|
| | ||
| Theorem | syldOLD 32 | Syllogism deduction. (The proof was shortened by O'Cat, 19-Feb-2008.). |
| | ||
| Theorem | syl5 33 | A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (The proof was shortened by Wolf Lammen, 25-May-2013.) |
|
| ||
| Theorem | syl2im 34 | Replace two antecedents. Implication-only version of syl2an 699. (Contributed by Wolf Lammen, 14-May-2013.) |
 | ||
| Theorem | imim12i 35 | Inference joining two implications. (The proof was shortened by O'Cat, 29-Oct-2011.) |
| | ||
| Theorem | imim1i 36 | Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (The proof was shortened by Wolf Lammen, 4-Aug-2012.) |
| | ||
| Theorem | imim3i 37 | Inference adding three nested antecedents. |
| | ||
| Theorem | 3syl 38 | Inference chaining two syllogisms. |
| | ||
| Theorem | syl6 39 | A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (The proof was shortened by Wolf Lammen, 30-Jul-2012.) |
|
| ||
| Theorem | syl6OLD 40 | Obsolete proof of syl6 39. |
|
| ||
| Theorem | sylc 41 | A syllogism inference combined with contraction. |
| | ||
| Theorem | sylcOLD 42 | A syllogism inference combined with contraction. (OBSOLETE - replaced by new sylc 41 21-Mar-2012. --NM) |
|
| ||
| Theorem | syl6c 43 | Inference combining syl6 39 with contraction. (Contributed by Alan Sare, 2-May-2011.) |
|
| ||
| Theorem | syldd 44 | Nested syllogism deduction. (The proof was shortened by Wolf Lammen, 11-May-2013.) |
|
| ||
| Theorem | sylddOLD 45 | Obsolete proof of syldd 44. |
|
| ||
| Theorem | syl5d 46 | A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-2000 and shortened further by O'Cat, 2-Feb-2006.) |
|
| ||
| Theorem | syl5dOLD 47 | A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-2000 and shortened further by O'Cat, 2-Feb-2006.) |
| | ||
| Theorem | syl7 48 | A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise. (The proof was shortened by Wolf Lammen, 3-Aug-2012.) |
|
| ||
| Theorem | syl6d 49 | A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-2000 and shortened further by O'Cat, 2-Feb-2006.) |
| | ||
| Theorem | syl8 50 | A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (The proof was shortened by Wolf Lammen, 3-Aug-2012.) |
|
| ||
| Theorem | syl8OLD 51 | Obsolete proof of syl8. |
|
| ||
| Theorem | syl9 52 | A nested syllogism inference with different antecedents. (The proof was shortened by Josh Purinton, 29-Dec-2000.) |
|
| ||
| Theorem | syl9r 53 | A nested syllogism inference with different antecedents. |
|
| ||
| Theorem | 3syld 54 | Triple syllogism deduction. (Contributed by Jeff Hankins, 4-Aug-2009.) |
| | ||
| Theorem | sylsyld 55 | Virtual deduction rule e12 17688 without virtual deduction symbols. (Contributed by Alan Sare, 20-Apr-2011.) |
|
| ||
| Theorem | imim12d 56 | Deduction combining antecedents and consequents. (The proof was shortened by O'Cat, 30-Oct-2011.) |
| | ||
| Theorem | imim1d 57 | Deduction adding nested consequents. (The proof was shortened by Wolf Lammen, 12-Sep-2012.) |
| | ||
| Theorem | imim1 58 | A closed form of syllogism (see syl 13). Theorem *2.06 of [WhiteheadRussell] p. 100. (The proof was shortened by Wolf Lammen, 25-May-2013.) |
| | ||
| Theorem | imim1OLD 59 | Obsolete proof of imim1 58. |
| | ||
| Theorem | imim1iOLD 60 | Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. |
| | ||
| Theorem | imim1dOLD 61 | Deduction adding nested consequents. |
| | ||
| Theorem | pm2.83 62 | Theorem *2.83 of [WhiteheadRussell] p. 108. |
|
| ||
| Theorem | syl5OLD 63 | A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise. (The proof was shortened by Wolf Lammen, 3-Aug-2012.) |
|
| ||
| Theorem | syl5OLDOLD 64 | Obsolete previous proof. |
|
| ||
| Theorem | syl7OLD 65 | A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise. (The proof was shortened by Wolf Lammen, 3-Aug-2012.) |
|
| ||
| Theorem | syl7OLDOLD 66 | Obsolete proof of syl7. |
|
| ||
| Theorem | pm2.27 67 | This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 7. Theorem *2.27 of [WhiteheadRussell] p. 104. |
| | ||
| Theorem | com23 68 | Commutation of antecedents. Swap 2nd and 3rd. (The proof was shortened by Wolf Lammen, 4-Aug-2012.) |
|
| ||
| Theorem | com3r 69 | Commutation of antecedents. Rotate right. |
| | ||
| Theorem | com13 70 | Commutation of antecedents. Swap 1st and 3rd. (The proof was shortened by Wolf Lammen, 28-Jul-2012.) |
|
| ||
| Theorem | com3l 71 | Commutation of antecedents. Rotate left. (The proof was shortened by Wolf Lammen, 28-Jul-2012.) |
|
| ||
| Theorem | pm2.04 72 | Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100. (The proof was shortened by Wolf Lammen, 12-Sep-2012.) |
|
| ||
| Theorem | pm2.04OLD 73 | Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100. |
|
| ||
| Theorem | com23OLD 74 | Commutation of antecedents. Swap 2nd and 3rd. |
|
| ||
| Theorem | com13OLD 75 | Commutation of antecedents. Swap 1st and 3rd. |
|
| ||
| Theorem | com3lOLD 76 | Commutation of antecedents. Rotate left. |
|
| ||
| Theorem | com3rOLD 77 | Commutation of antecedents. Rotate right. |
| | ||
| Theorem | com34 78 | Commutation of antecedents. Swap 3rd and 4th. |
|
| ||
| Theorem | com4l 79 | Commutation of antecedents. Rotate left. (The proof was shortened by O'Cat, 15-Aug-2004.) |
|
| ||
| Theorem | com4t 80 | Commutation of antecedents. Rotate twice. |
|
| ||
| Theorem | com4r 81 | Commutation of antecedents. Rotate right. |
|
| ||
| Theorem | com24 82 | Commutation of antecedents. Swap 2nd and 4th. (The proof was shortened by Wolf Lammen, 28-Jul-2012.) |
|
| ||
| Theorem | com14 83 | Commutation of antecedents. Swap 1st and 4th. (The proof was shortened by Wolf Lammen, 28-Jul-2012.) |
|
| ||
| Theorem | com24OLD 84 | Commutation of antecedents. Swap 2nd and 4th. |
|
| ||
| Theorem | com14OLD 85 | Commutation of antecedents. Swap 1st and 4th. |
|
| ||
| Theorem | com4lOLD 86 | Commutation of antecedents. Rotate left. (The proof was shortened by O'Cat, 15-Aug-2004.) |
|
| ||
| Theorem | com45 87 | Commutation of antecedents. Swap 4th and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) |
| ||
| Theorem | com35 88 | Commutation of antecedents. Swap 3rd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) |
|
| ||
| Theorem | com25 89 | Commutation of antecedents. Swap 2nd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) |
|
| ||
| Theorem | com5l 90 | Commutation of antecedents. Rotate left. (Contributed by Jeff Hankins, 28-Jun-2009.) (The proof was shortened by Wolf Lammen, 29-Jul-2012.) |
|
| ||
| Theorem | com15 91 | Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (The proof was shortened by Wolf Lammen, 29-Jul-2012.) |
|
| ||
| Theorem | com15OLD 92 | Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) |
|
| ||
| Theorem | com5lOLD 93 | Commutation of antecedents. Rotate left. (Contributed by Jeff Hankins, 28-Jun-2009.) |
|
| ||
| Theorem | com52l 94 | Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28-Jun-2009.) |
|
| ||
| Theorem | com52r 95 | Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.) |
|
| ||
| Theorem | com5r 96 | Commutation of antecedents. Rotate right. (Contributed by Wolf Lammen, 29-Jul-2012.) |
|
| ||
| Theorem | a1dd 97 | Deduction introducing a nested embedded antecedent. (The proof was shortened by O'Cat, 15-Jan-2008.) |
| | ||
| Theorem | mp2 98 | A double modus ponens inference. |
|
| ||
| Theorem | mp2d 99 | A double modus ponens deduction. |
| | ||
| Theorem | mp2b 100 | A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.) |
| | ||
| MPE Home Contents | Copyright terms: Public domain | < Wrap Next > |