Home | Metamath
Proof ExplorerTheorem List
(p. 1 of 309)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |

Type | Label | Description | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|

Statement | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

PART 1 CLASSICAL FIRST ORDER LOGIC WITH
EQUALITY
Logic can be defined as the "study of the principles of correct
reasoning"
(Merrilee H. Salmon's 1991 "Informal Reasoning and Informal Logic"
in
This section formally defines the logic system we will use. In particular, it defines symbols for declaring truthful statements, along with rules for deriving truthful statements from other truthful statements. The system defined here is classical first order logic with equality (the most common logic system used by mathematicians). We begin with a few housekeeping items in pre-logic, and then introduce propositional calculus (both its axioms and important theorems that can be derived from them). Propositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. This is followed by proofs that other axiomatizations of classical propositional calculus can be derived from the axioms we have chosen to use. We then define predicate calculus, which adds additional symbols and rules useful for discussing objects (beyond simply true or false). In particular it introduces the symbols ("equals"), ("is a member of"), and ("for all"). The first two are called "predicates." A predicate specifies a true or false relationship between its two arguments. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.1 Pre-logicThis section includes a few "housekeeping" mechanisms before we begin defining the basics of logic. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.1.1 Inferences for assisting proof
development | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | dummylink 1 |
(Note: This inference rule and the next one, idi 2, will
normally
never appear in a completed proof. It can be ignored if you are using
this database to assist learning logic - please start with the statement
wn 5 instead.)
This is a technical inference 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 inference 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.
This inference was originally designed to assist importing partially completed Proof Worksheets from the mmj2 Proof Assistant GUI, but it can also be useful on its own. Interestingly, no axioms are required for its proof. (Contributed by NM?, 7-Feb-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | idi 2 | Inference form of id 21. This inference rule, which requires no axioms for its proof, is useful as a copy-paste mechanism during proof development in mmj2. It is normally not referenced in the final version of a proof, since it is always redundant and can be removed using the 'minimize *' command in the metamath program's Proof Assistant. (Contributed by Alan Sare, 31-Dec-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.2 ConventionsThis section describes the conventions we use. However, these conventions often refer to existing mathematical practices, which are discussed in more detail in other references. Logic and set theory provide a foundation for all of mathematics. To learn about them, you should study one or more of the references listed below. We indicate references using square brackets. The textbooks provide a motivation for what we are doing, whereas Metamath lets you see in detail all hidden and implicit steps. Most standard theorems are accompanied by citations. Some closely followed texts include the following: - Axioms of propositional calculus - [Margaris].
- Axioms of predicate calculus - [Megill] (System S3' in the article referenced).
- Theorems of propositional calculus - [WhiteheadRussell].
- Theorems of pure predicate calculus - [Margaris].
- Theorems of equality and substitution - [Monk2], [Tarski], [Megill].
- Axioms of set theory - [BellMachover].
- Development of set theory - [TakeutiZaring]. (The first part of [Quine] has a good explanation of the powerful device of "virtual" or class abstractions, which is essential to our development.)
- Construction of real and complex numbers - [Gleason]
- Theorems about real numbers - [Apostol]
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | conventions 3 |
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 12036) which denotes that index variable ranges over when evaluating . Thus, means 1/2 + 1/4 + 1/8 + ... = 1 (geoihalfsum 12212). 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 8675, proven by the preceding theorem ax1cn 8651. 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 8675 (not ax1cn 8651) and ax-1ne0 8686 (not ax1ne0 8662), as these are proven axioms for complex arithmetic. Thus, both ax1cn 8651 and ax1ne0 8662 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 7627) 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 6866) does not use the axiom of choice. In some cases, the weaker axiom of countable choice (ax-cc 7945) or axiom of dependent choice (ax-dc 7956) 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 ".**Substitution.**" " should be read "the wff that results from the proper substitution of for in wff ." See df-sb 1883 and the related df-sbc 2922 and df-csb 3010.**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 2729 and isset 2731.**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 4596. This can be used to define a subset, e.g., df-tan 12227 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 12304). 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 4608. 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 5713). For example, the in ; see 2p2e4 9721. 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 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 (see wel 1622), equality (see df-cleq 2246), subset (see df-ss 3089), and less-than (see df-lt 8630). For the general definition of a binary relation in the form , see df-br 3921. For example, ( see 0lt1 9176) 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 8918.**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 12220). The function is then defined labelled df-NAME; definitions are typically given using the maps-to notation (e.g., df-cos 12226). Typically there are other proofs such as its closure labelled NAMEcl (e.g., coscl 12281), its function application form labelled NAMEval (e.g., cosval 12277), and at least one simple value (e.g., cos0 12304).**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 11167 and fac4 11174).**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 8624), while "" is the group identity element (df-0g 13278), "" is the poset zero (df-p0 13989), "" is the zero polynomial (df-0p 18857), "" is the zero vector in a normed complex vector space (df-0v 20984), and "" is a class variable for use as a connective symbol (this is used, for example, in p0val 13991). 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-n 9627) for the integer numbers starting from 1, and (df-n0 9845) 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 10004, e.g., ;;; (see 4001prm 13017 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 24. A deduction hypothesis can have an indirect antecedent via definitions, e.g., see lhop 19195. 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 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 2120 derived from df-eu 2118. 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 4407 vs. uniexg 4408. Label names are relatively short while suggesting their purpose, e.g., 2p2e4 9721 is the label for 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 3511, which works in certain cases in set theory. We also sometimes use dedhb 2872. 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 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 in df-recs 6274, in df-rdg 6309, seq_{𝜔}in df-seqom 6346, and in df-seq 10925. These have characteristic function and initial value . (_{g}in df-gsum 13279 isn't really designed for arbitrary recursion, but you could do it with the right magma.) The logically primary one is df-recs 6274, but for the "average user" the most useful one is probably df-seq 10925- 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 13024.**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 6856 is the first lemma for sbth 6866. 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.**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/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:
- is read " is not free in (wff) "; see df-nf 1540. Similarly, is read is not free in (class) , see df-nfc 2374.
- "$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 1540) in place of "$d $." 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 2120 from df-eu 2118.
- "$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 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' 'set width 79' 'write source set.mm /rewrap' .**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.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | natded 4 |
Here are typical natural deduction (ND) rules in the style of Gentzen
and Jaśkowski, along with MPE translations of them.
This also shows the recommended theorems when you find yourself
needing these rules (the recommendations encourage a slightly
different proof style that works more naturally with metamath).
A decent list of the standard rules of natural deduction can be
found beginning with definition /\I in [Pfenning] p. 18.
For information about ND and Metamath, see the
page on Deduction Form and Natural Deduction
in Metamath Proof Explorer.
Many more citations could be added.
Note that MPE uses classical logic, not intuitionist logic. As is conventional, the "I" rules are introduction rules, "E" rules are elimination rules, the "C" rules are conversion rules, and represents the set of (current) hypotheses. We use wff variable names beginning with to provide a closer representation of the Metamath equivalents (which typically use the antedent to represent the context ). Most of this information was developed by Mario Carneiro and posted on 3-Feb-2017. For more information, see the page on Deduction Form and Natural Deduction in Metamath Proof Explorer. For annotated examples where some traditional ND rules are directly applied in MPE, see ex-natded5.2 20649, ex-natded5.3 20652, ex-natded5.5 20655, ex-natded5.7 20656, ex-natded5.8 20658, ex-natded5.13 20660, ex-natded9.20 20662, and ex-natded9.26 20664. (Contributed by DAW, 4-Feb-2017.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.3 Propositional calculusPropositional calculus deals with general truths about well-formed formulas (wffs) regardless of how they are constructed. The simplest propositional truth is , which can be read "if something is true, then it is true" - rather trivial and obvious, but nonetheless it must be proved from the axioms (see theorem id 21). Our system of propositional calculus consists of three basic axioms and another axiom that defines the modus-ponens inference rule. It is attributed to Jan Lukasiewicz (pronounced woo-kah-SHAY-vitch) and was popularized by Alonzo Church, who called it system P2. (Thanks to Ted Ulrich for this information.) These axioms are ax-1 7, ax-2 8, ax-3 9, and (for modus ponens) ax-mp 10. Some closely followed texts include [Margaris] for the axioms and [WhiteheadRussell] for the theorems. The propositional calculus used here is the classical system widely used by mathematicians. In particular, this logic system accepts the "law of the excluded middle" as proven in exmid 406, which says that a logical statement is either true or not true. This is an essential distinction of classical logic and is not a theorem of intuitionistic logic.
All 194 axioms, definitions, and theorems for propositional calculus in
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.3.1 Recursively define primitive wffs for
propositional calculus | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | wn 5 | 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 1620 and wel 1622). | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Syntax | wi 6 |
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. After we define the axioms of
propositional calculus (ax-1 7, ax-2 8, ax-3 9, and ax-mp 10), the
biconditional (df-bi 179), the constant true (df-tru 1315), and the
constant false (df-fal 1316), we will be able to prove these truth
table values:
(truimtru 1340),
(truimfal 1341),
(falimtru 1342), and
(falimfal 1343). These
have straightforward meanings, for example,
just means "the value of is
".
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. Contrast with (df-bi 179), (df-an 362), and (df-or 361). This is called "material implication" and the arrow is usually read as "implies." However, material implication is not identical to the meaning of "implies" in natural language. For example, the word "implies" may suggest a causal relationship in natural language. Material implication does not require any causal relationship. Also note that in material implication, if the consequent is true then the wff is always true (even if the antecedent is false). Thus, if "implies" means material implication, it is true that "if the moon is made of green cheese that implies that 5=5" (because 5=5). Similarly, if the antecedent is false, the wff is always true. Thus, it is true that, "if the moon made of green cheese that implies that 5=7" (because the moon is not actually made of green cheese). A contradiction implies anything (pm2.21i 125). In short, material implication has a very specific technical definition, and misunderstandings of it are sometimes called "paradoxes of logical implication." | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.3.2 The axioms of propositional
calculusPostulate the three axioms of classical propositional calculus. Propositional calculus (axioms ax-1 7 through ax-3 9 and rule ax-mp 10) 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 10) the wffs ax-1 7, ax-2 8, pm2.04 78, con3 128, notnot2 106, and notnot1 116. 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 78) and replacing the last three with our ax-3 9. (Thanks to Ted Ulrich for this information.)
The theorems of propositional calculus are also called | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Axiom | ax-1 7 |
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."
(Contributed by NM, 5-Aug-1993.)
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Axiom | ax-2 8 |
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 355. (Contributed by NM,
5-Aug-1993.)
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Axiom | ax-3 9 |
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. (Contributed by NM, 5-Aug-1993.)
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Axiom | ax-mp 10 |
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. "Modus ponens" is
short for
"modus ponendo ponens," a Latin phrase that means "the
mood that by
affirming affirms" [Sanford] p.
39. This rule is similar to the rule of
modus tollens mto 169.
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. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.3.3 Logical implicationThe results in this section are based on implication only, and avoid ax-3. In an implication, the wff before the arrow is called the "antecedent" and the wff after the arrow is called the "consequent." We will use the following descriptive terms very loosely: A "closed form" or "tautology" has no $e hypotheses. An "inference" has one or more $e hypotheses. A "deduction" is an inference in which the hypotheses and the conclusion share the same antecedent. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mp2b 11 | A double modus ponens inference. (Contributed by Mario Carneiro, 24-Jan-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a1i 12 | Inference derived from axiom ax-1 7. See a1d 24 for an explanation of our informal use of the terms "inference" and "deduction." See also the comment in syld 42. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mp1i 13 | Drop and replace an antecedent. (Contributed by Stefan O'Rear, 29-Jan-2015.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a2i 14 | Inference derived from axiom ax-2 8. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim2i 15 | Inference adding common antecedents in an implication. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpd 16 | A modus ponens deduction. A translation of natural deduction rule E ( elimination), see natded 4. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl 17 |
An inference version of the transitive laws for implication imim2 51
and
imim1 72, 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."
(A bit of trivia: this is the most commonly referenced assertion in our database. In second place is eqid 2253, followed by syl2anc 645, adantr 453, syl3anc 1187, and ax-mp 10. The Metamath program command 'show usage' shows the number of references.) (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 20-Oct-2011.) (Proof shortened by Wolf Lammen, 26-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpi 18 | A nested modus ponens inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mp2 19 | A double modus ponens inference. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3syl 20 | Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | id 21 | Principle of identity. Theorem *2.08 of [WhiteheadRussell] p. 101. For another version of the proof directly from axioms, see id1 22. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Stefan Allan, 20-Mar-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | id1 22 |
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. 17 (PDF p. 23) 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 21. (Contributed by NM, 5-Aug-1993.)
(Proof modification is discouraged.)
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | idd 23 | Principle of identity with antecedent. (Contributed by NM, 26-Nov-1995.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a1d 24 |
Deduction introducing an embedded antecedent.
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a2d 25 | Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a1ii 26 | Add two antecedents to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sylcom 27 | Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl5com 28 | Syllogism inference with commuted antecedents. (Contributed by NM, 24-May-2005.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com12 29 | Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl5 30 | A syllogism rule of inference. The first premise is used to replace the second antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl6 31 | A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl56 32 | Combine syl5 30 and syl6 31. (Contributed by NM, 14-Nov-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl6com 33 | Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpcom 34 | Modus ponens inference with commutation of antecedents. (Contributed by NM, 17-Mar-1996.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syli 35 | Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl2im 36 | Replace two antecedents. Implication-only version of syl2an 465. (Contributed by Wolf Lammen, 14-May-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.27 37 | This theorem, called "Assertion," can be thought of as closed form of modus ponens ax-mp 10. Theorem *2.27 of [WhiteheadRussell] p. 104. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpdd 38 | A nested modus ponens deduction. (Contributed by NM, 12-Dec-2004.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpid 39 | A nested modus ponens deduction. (Contributed by NM, 14-Dec-2004.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpdi 40 | A nested modus ponens deduction. (Contributed by NM, 16-Apr-2005.) (Proof shortened by O'Cat, 15-Jan-2008.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpii 41 | A doubly nested modus ponens inference. (Contributed by NM, 31-Dec-1993.) (Proof shortened by Wolf Lammen, 31-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syld 42 |
Syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened
by O'Cat, 19-Feb-2008.) (Proof shortened by Wolf Lammen, 3-Aug-2012.)
Notice that syld 42 has the same form as syl 17 with added in front of each hypothesis and conclusion. When all theorems referenced in a proof are converted in this way, we can replace with a hypothesis of the proof, allowing the hypothesis to be eliminated with id 21 and become an antecedent. The Deduction Theorem for propositional calculus, e.g. Theorem 3 in [Margaris] p. 56, tells us that this procedure is always possible. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mp2d 43 | A double modus ponens deduction. (Contributed by NM, 23-May-2013.) (Proof shortened by Wolf Lammen, 23-Jul-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | a1dd 44 | Deduction introducing a nested embedded antecedent. (Contributed by NM, 17-Dec-2004.) (Proof shortened by O'Cat, 15-Jan-2008.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.43i 45 | Inference absorbing redundant antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.43d 46 | Deduction absorbing redundant antecedent. (Contributed by NM, 18-Aug-1993.) (Proof shortened by O'Cat, 28-Nov-2008.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.43a 47 | Inference absorbing redundant antecedent. (Contributed by NM, 7-Nov-1995.) (Proof shortened by O'Cat, 28-Nov-2008.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.43b 48 | Inference absorbing redundant antecedent. (Contributed by NM, 31-Oct-1995.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.43 49 | Absorption of redundant antecedent. Also called the "Contraction" or "Hilbert" axiom. Theorem *2.43 of [WhiteheadRussell] p. 106. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 15-Aug-2004.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim2d 50 | Deduction adding nested antecedents. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim2 51 | A closed form of syllogism (see syl 17). Theorem *2.05 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Sep-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | embantd 52 | Deduction embedding an antecedent. (Contributed by Wolf Lammen, 4-Oct-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | 3syld 53 | Triple syllogism deduction. (Contributed by Jeff Hankins, 4-Aug-2009.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sylsyld 54 | Virtual deduction rule e12 27189 without virtual deduction symbols. (Contributed by Alan Sare, 20-Apr-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim12i 55 | Inference joining two implications. (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 29-Oct-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim1i 56 | Inference adding common consequents in an implication, thereby interchanging the original antecedent and consequent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim3i 57 | Inference adding three nested antecedents. (Contributed by NM, 19-Dec-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | sylc 58 | A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl3c 59 | A syllogism inference combined with contraction. e111 27136 without virtual deductions. (Contributed by Alan Sare, 7-Jul-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl6mpi 60 | e20 27192 without virtual deductions. (Contributed by Alan Sare, 8-Jul-2011.) (Proof shortened by Wolf Lammen, 13-Sep-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | mpsyl 61 | Modus ponens combined with a syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl6c 62 | Inference combining syl6 31 with contraction. (Contributed by Alan Sare, 2-May-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syldd 63 | Nested syllogism deduction. (Contributed by NM, 12-Dec-2004.) (Proof shortened by Wolf Lammen, 11-May-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl5d 64 | A nested syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by O'Cat, 2-Feb-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl7 65 | A syllogism rule of inference. The first premise is used to replace the third antecedent of the second premise. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Aug-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl6d 66 | A nested syllogism deduction. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) (Proof shortened by O'Cat, 2-Feb-2006.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl8 67 | A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994.) (Proof shortened by Wolf Lammen, 3-Aug-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl9 68 | A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Josh Purinton, 29-Dec-2000.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | syl9r 69 | A nested syllogism inference with different antecedents. (Contributed by NM, 5-Aug-1993.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim12d 70 | Deduction combining antecedents and consequents. (Contributed by NM, 7-Aug-1994.) (Proof shortened by O'Cat, 30-Oct-2011.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim1d 71 | Deduction adding nested consequents. (Contributed by NM, 3-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | imim1 72 | A closed form of syllogism (see syl 17). Theorem *2.06 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 25-May-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.83 73 | Theorem *2.83 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com23 74 | Commutation of antecedents. Swap 2nd and 3rd. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Aug-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com3r 75 | Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com13 76 | Commutation of antecedents. Swap 1st and 3rd. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com3l 77 | Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.04 78 | Swap antecedents. Theorem *2.04 of [WhiteheadRussell] p. 100. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Sep-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com34 79 | Commutation of antecedents. Swap 3rd and 4th. (Contributed by NM, 25-Apr-1994.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com4l 80 | Commutation of antecedents. Rotate left. (Contributed by NM, 25-Apr-1994.) (Proof shortened by O'Cat, 15-Aug-2004.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com4t 81 | Commutation of antecedents. Rotate twice. (Contributed by NM, 25-Apr-1994.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com4r 82 | Commutation of antecedents. Rotate right. (Contributed by NM, 25-Apr-1994.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com24 83 | Commutation of antecedents. Swap 2nd and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com14 84 | Commutation of antecedents. Swap 1st and 4th. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 28-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com45 85 | Commutation of antecedents. Swap 4th and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com35 86 | Commutation of antecedents. Swap 3rd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com25 87 | Commutation of antecedents. Swap 2nd and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com5l 88 | Commutation of antecedents. Rotate left. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com15 89 | Commutation of antecedents. Swap 1st and 5th. (Contributed by Jeff Hankins, 28-Jun-2009.) (Proof shortened by Wolf Lammen, 29-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com52l 90 | Commutation of antecedents. Rotate left twice. (Contributed by Jeff Hankins, 28-Jun-2009.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com52r 91 | Commutation of antecedents. Rotate right twice. (Contributed by Jeff Hankins, 28-Jun-2009.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | com5r 92 | Commutation of antecedents. Rotate right. (Contributed by Wolf Lammen, 29-Jul-2012.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | jarr 93 | Elimination of a nested antecedent as a kind of reversal of inference ja 155. (Contributed by Wolf Lammen, 9-May-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.86i 94 | Inference based on pm2.86 96. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.86d 95 | Deduction based on pm2.86 96. (Contributed by NM, 29-Jun-1995.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.86 96 | Converse of axiom ax-2 8. Theorem *2.86 of [WhiteheadRussell] p. 108. (Contributed by NM, 25-Apr-1994.) (Proof shortened by Wolf Lammen, 3-Apr-2013.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | loolinALT 97 | The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. This version of loolin 175 does not use ax-3 9, meaning that this theorem is intuitionistically valid. (Contributed by O'Cat, 12-Aug-2004.) (New usage is discouraged.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | loowoz 98 |
An alternate for the Linearity Axiom of the infinite-valued sentential
logic (L-infinity) of Lukasiewicz, due to Barbara Wozniakowska, Reports
on Mathematical Logic 10, 129-137 (1978). (Contributed by O'Cat,
8-Aug-2004.)
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

1.3.4 Logical negationThis section makes our first use of the third axiom of propositional calculus, ax-3 9. | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | con4d 99 | Deduction derived from axiom ax-3 9. (Contributed by NM, 26-Mar-1995.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

Theorem | pm2.21d 100 | A contradiction implies anything. Deduction from pm2.21 102. (Contributed by NM, 10-Feb-1996.) | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |