Metamath Proof Explorer

Home	Metamath Proof Explorer	< Wrap Next >
		Browser slow? Try the Unicode version.

Jump to page: 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5787

Color key:

Metamath Proof Explorer (1-4957)

Hilbert Space Explorer (4958-5787)

**Statement List for Metamath Proof Explorer -** 1-100 - Page 1 of 58
Type	Label	Description
Statement

Syntax	wn 1	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 797 and wel 803).


Syntax	wi 2	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.


Axiom	ax-1 3	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." Propositional calculus (axioms ax-1 3 through ax-3 5 and rule ax-mp 6) 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 6) the wffs ax-1 3, ax-2 4, pm2.04 31, con3 86, nega 78, and negb 79. 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 31) and replacing the last three with our ax-3 5. (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. 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.


Axiom	ax-2 4	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.


Axiom	ax-3 5	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).


Axiom	ax-mp 6	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.


Theorem	a1i 7	Inference derived from axiom ax-1 3. See a1d 14 for an explanation of our informal use of the terms "inference" and "deduction".


Theorem	a2i 8	Inference derived from axiom ax-2 4.


Theorem	id 9	Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 10.


Theorem	id1 10	Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. This version is proved directly from the axioms for demonstration purposes. This proof is identical, step for step, to the proofs of Theorem 1 of [Margaris] p. 51 and Example 2.7(a) of [Hamilton] p. 31. For a shorter version of the proof that takes advantage of a previously proved inference, see id 9.


Theorem	idd 11	Principle of identity with antecedent.


Theorem	syl 12	Syllogism inference. (A bit of trivia: this is the most commonly referenced assertion in our database. In second place is ax-mp 6, followed by visset 1350, bitr 151, imp 277, and exp 291. The Metamath program command 'show usage' shows the number of references.)


Theorem	com12 13	Inference that swaps (commutes) antecedents in an implication.


Theorem	a1d 14	Deduction introducing an embedded antecedent. 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 would be replaced with a conjunction (df-an 198) of the hypotheses of the would-be deduction. By contrast, we tend to call the simpler version with no common antecedent an "inference" and suffix its label with "i"; compare theorem a1i 7. Finally, a "theorem" would be the form with no hypotheses; in this case the "theorem" form would be the original axiom ax-1 3. In propositional calculus we usually prove the theorem form first without a suffix on its label (e.g. pm2.43 57 vs. pm2.43i 58 vs. pm2.43d 59), but (much) later we often suffix the theorem form's label with "t" as in negnegt 4157 vs. negneg 4154, especially when our "weak deduction theorem" dedth 1784 is used to prove the theorem form from its inference form. When an inference is converted to a theorem by eliminating an "is a set" hypothesis, we sometimes suffix the theorem form with "g" (for somewhat misnamed "generalized") as in uniex 1947 vs. uniexg 1948.


Theorem	a2d 15	Deduction distributing an embedded antecedent.


Theorem	syl1 16	A closed form of syllogism. Theorem *2.05 of [WhiteheadRussell] p. 100.


Theorem	syl2 17	A closed form of syllogism. Theorem *2.06 of [WhiteheadRussell] p. 100.


Theorem	syl3 18	Inference adding common antecedents in an implication.


Theorem	syl4 19	Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent.


Theorem	syl34 20	Inference joining two implications.


Theorem	3syl 21	Inference chaining two syllogisms.


Theorem	syl5 22	A syllogism rule of inference. The second premise is used to replace the second antecedent of the first premise.


Theorem	syl6 23	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.


Theorem	syl7 24	A syllogism rule of inference. The second premise is used to replace the third antecedent of the first premise.


Theorem	syl8 25	A syllogism rule of inference. The second premise is used to replace the consequent of the first premise.


Theorem	syl3d 26	Deduction adding nested antecedents.


Theorem	syld 27	Syllogism deduction. (The proof was shortened by Mel L. O'Cat, 7-Aug-04.)


Theorem	syl4d 28	Deduction adding nested consequents.


Theorem	syl34d 29	Deduction combining antecedents and consequents.


Theorem	pm2.27 30	This theorem, called "Assertion," can be thought of as closed form of modus ponens. Theorem *2.27 of [WhiteheadRussell] p. 104.


Theorem	pm2.04 31	Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100.


Theorem	com23 32	Commutation of antecedents. Swap 2nd and 3rd.


Theorem	com13 33	Commutation of antecedents. Swap 1st and 3rd.


Theorem	com3l 34	Commutation of antecedents. Rotate left.


Theorem	com3r 35	Commutation of antecedents. Rotate right.


Theorem	com34 36	Commutation of antecedents. Swap 3rd and 4th.


Theorem	com24 37	Commutation of antecedents. Swap 2nd and 4th.


Theorem	com14 38	Commutation of antecedents. Swap 1st and 4th.


Theorem	com4l 39	Commutation of antecedents. Rotate left. (The proof was shortened by Mel L. O'Cat, 15-Aug-04.)


Theorem	com4t 40	Commutation of antecedents. Rotate twice.


Theorem	com4r 41	Commutation of antecedents. Rotate right.


Theorem	a1dd 42	Deduction introducing a nested embedded antecedent.


Theorem	mp2 43	A double modus ponens inference.


Theorem	mpi 44	A nested modus ponens inference.


Theorem	mpii 45	A doubly nested modus ponens inference.


Theorem	mpd 46	A modus ponens deduction.


Theorem	mpdd 47	A nested modus ponens deduction.


Theorem	mpid 48	A nested modus ponens deduction.


Theorem	mpcom 49	Modus ponens inference with commutation of antecedents.


Theorem	syldd 50	Nested syllogism deduction.


Theorem	sylcom 51	Syllogism inference with commutation of antecedents.


Theorem	syli 52	Syllogism inference with common nested antecedent.


Theorem	syl5d 53	A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-00.)


Theorem	syl6d 54	A nested syllogism deduction. (The proof was shortened by Josh Purinton, 29-Dec-00.)


Theorem	syl9 55	A nested syllogism inference with different antecedents. (The proof was shortened by Josh Purinton, 29-Dec-00.)


Theorem	syl9r 56	A nested syllogism inference with different antecedents.


Theorem	pm2.43 57	Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of [WhiteheadRussell] p. 106. (The proof was shortened by Mel L. O'Cat, 15-Aug-04.)