Home | Intuitionistic Logic Explorer Theorem List (p. 18 of 20) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | sb9i 1701 | Commutation of quantification and substitution variables. |
Theorem | sb9 1702 | Commutation of quantification and substitution variables. |
Theorem | ax11v 1703* | This is a version of ax-11o 1654 when the variables are distinct. Axiom (C8) of [Monk2] p. 105. See theorem ax11v2 1651 for the rederivation of ax-11o 1654 from this theorem. |
Theorem | sb56 1704* | Two equivalent ways of expressing the proper substitution of for in , when and are distinct. Theorem 6.2 of [Quine] p. 40. The proof does not involve df-sb 1606. |
Theorem | sb6 1705* | Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70. |
Theorem | sb5 1706* | Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40. |
Theorem | ax16i 1707* | Inference with ax-16 1644 as its conclusion, that doesn't require ax-10 1388, ax-11 1389, or ax-12 1393 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. |
Theorem | ax16ALT 1708* | Version of ax16 1643 that doesn't require ax-10 1388 or ax-12 1393 for its proof. |
Theorem | a4v 1709* | Specialization, using implicit substitition. |
Theorem | a4imev 1710* | Distinct-variable version of a4ime 1593. |
Theorem | a4eiv 1711* | Inference from existential specialization, using implicit substitition. |
Theorem | equvin 1712* | A variable introduction law for equality. Lemma 15 of [Monk2] p. 109. |
Theorem | a16g 1713* | A generalization of axiom ax-16 1644. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | a16gb 1714* | A generalization of axiom ax-16 1644. |
Theorem | albidv 1715* | Formula-building rule for universal quantifier (deduction rule). |
Theorem | exbidv 1716* | Formula-building rule for existential quantifier (deduction rule). |
Theorem | 2albidv 1717* | Formula-building rule for 2 existential quantifiers (deduction rule). |
Theorem | 2exbidv 1718* | Formula-building rule for 2 existential quantifiers (deduction rule). |
Theorem | 3exbidv 1719* | Formula-building rule for 3 existential quantifiers (deduction rule). |
Theorem | 4exbidv 1720* | Formula-building rule for 4 existential quantifiers (deduction rule). |
Theorem | 19.9v 1721* | Special case of Theorem 19.9 of [Margaris] p. 89. |
Theorem | 19.21v 1722* | Special case of Theorem 19.21 of [Margaris] p. 90. Notational convention: We sometimes suffix with "v" the label of a theorem eliminating a hypothesis such as in 19.21 1464 via the use of distinct variable conditions combined with ax-17 1402. 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 1835 derived from df-eu 1833. The "f" stands for "not free in" which is less restrictive than "does not occur in." |
Theorem | alrimiv 1723* | Inference from Theorem 19.21 of [Margaris] p. 90. |
Theorem | alrimivv 1724* | Inference from Theorem 19.21 of [Margaris] p. 90. |
Theorem | alrimdv 1725* | Deduction from Theorem 19.21 of [Margaris] p. 90. |
Theorem | 2ax17 1726* | Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.) |
Theorem | alimdv 1727* | Deduction from Theorem 19.20 of [Margaris] p. 90. |
Theorem | eximdv 1728* | Deduction from Theorem 19.22 of [Margaris] p. 90. |
Theorem | 2alimdv 1729* | Deduction from Theorem 19.22 of [Margaris] p. 90. |
Theorem | 2eximdv 1730* | Deduction from Theorem 19.22 of [Margaris] p. 90. |
Theorem | 19.23v 1731* | Special case of Theorem 19.23 of [Margaris] p. 90. |
Theorem | 19.23vv 1732* | Theorem 19.23 of [Margaris] p. 90 extended to two variables. |
Theorem | exlimiv 1733* |
Inference from Theorem 19.23 of [Margaris] p.
90.
This inference, along with our many variants is used to implement a metatheorem called "Rule C" that is given in many logic textbooks. See, for example, Rule C in [Mendelson] p. 81, Rule C in [Margaris] p. 40, or Rule C in Hirst and Hirst's A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. In informal proofs, the statement "Let C be an element such that..." almost always means an implicit application of Rule C. In essence, Rule C states that if we can prove that some element exists satisfying a wff, i.e. where has free, then we can use C as a hypothesis for the proof where C is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier. We cannot do this in Metamath directly. Instead, we use the original (containing ) as an antecedent for the main part of the proof. We eventually arrive at where is the theorem to be proved and does not contain . Then we apply exlimiv 1733 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 8 to arrive at the final theorem . |
Theorem | pm11.53 1734* | Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
Theorem | exlimivv 1735* | Inference from Theorem 19.23 of [Margaris] p. 90. |
Theorem | exlimdvv 1736* | Deduction from Theorem 19.23 of [Margaris] p. 90. |
Theorem | 19.27v 1737* | Theorem 19.27 of [Margaris] p. 90. |
Theorem | 19.28v 1738* | Theorem 19.28 of [Margaris] p. 90. |
Theorem | 19.36v 1739* | Special case of Theorem 19.36 of [Margaris] p. 90. |
Theorem | 19.36aiv 1740* | Inference from Theorem 19.36 of [Margaris] p. 90. |
Theorem | 19.12vv 1741* | Special case of 19.12 1535 where its converse holds. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.) |
Theorem | 19.37v 1742* | Special case of Theorem 19.37 of [Margaris] p. 90. |
Theorem | 19.37aiv 1743* | Inference from Theorem 19.37 of [Margaris] p. 90. |
Theorem | 19.41v 1744* | Special case of Theorem 19.41 of [Margaris] p. 90. |
Theorem | 19.41vv 1745* | Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers. |
Theorem | 19.41vvv 1746* | Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers. |
Theorem | 19.41vvvv 1747* | Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.) |
Theorem | 19.42v 1748* | Special case of Theorem 19.42 of [Margaris] p. 90. |
Theorem | exdistr 1749* | Distribution of existential quantifiers. |
Theorem | 19.42vv 1750* | Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers. |
Theorem | 19.42vvv 1751* | Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers. |
Theorem | exdistr2 1752* | Distribution of existential quantifiers. |
Theorem | 3exdistr 1753* | Distribution of existential quantifiers. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | 4exdistr 1754* | Distribution of existential quantifiers. |
Theorem | cbvalv 1755* | Rule used to change bound variables, using implicit substitition. |
Theorem | cbvexv 1756* | Rule used to change bound variables, using implicit substitition. |
Theorem | cbval2 1757* | Rule used to change bound variables, using implicit substitition. |
Theorem | cbvex2 1758* | Rule used to change bound variables, using implicit substitition. |
Theorem | cbval2v 1759* | Rule used to change bound variables, using implicit substitition. |
Theorem | cbvex2v 1760* | Rule used to change bound variables, using implicit substitition. |
Theorem | cbvald 1761* | Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1799. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | cbvexd 1762* | Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1799. |
Theorem | cbvex4v 1763* | Rule used to change bound variables, using implicit substitition. |
Theorem | eean 1764 | Rearrange existential quantifiers. |
Theorem | eeanv 1765* | Rearrange existential quantifiers. |
Theorem | eeeanv 1766* | Rearrange existential quantifiers. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | ee4anv 1767* | Rearrange existential quantifiers. |
Theorem | nexdv 1768* | Deduction for generalization rule for negated wff. |
Theorem | chvarv 1769* | Implicit substitution of for into a theorem. |
Theorem | cleljust 1770* | When the class variables of set theory are replaced with set variables, this theorem of predicate calculus is the result. This theorem provides part of the justification for the consistency of that definition, which "overloads" the set variables in wel 1386 with the class variables in wcel 1385. |
Theorem | equsb3lem 1771* | Lemma for equsb3 1772. (The proof was shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | equsb3 1772* | Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.) |
Theorem | elsb3 1773* | Substitution applied to an atomic membership wff. (The proof was shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | elsb4 1774* | Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010.) (The proof was shortened by Andrew Salmon, 14-Jun-2011.) |
Theorem | hbs1 1775* | is not free in when and are distinct. |
Theorem | sbhb 1776* | Two ways of expressing " is (effectively) not free in ." |
Theorem | sbhb2 1777* | Two ways of expressing " is (effectively) not free in ." (Contributed by Gérard Lang, 14-Nov-2013.) |
Theorem | hbsb 1778* | If is not free in , it is not free in when and are distinct. |
Theorem | hbsbd 1779* | Deduction version of hbsb 1778. |
Theorem | 2sb5 1780* | Equivalence for double substitution. |
Theorem | 2sb6 1781* | Equivalence for double substitution. |
Theorem | sbcom2 1782* | Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). |
Theorem | pm11.07 1783* | Theorem *11.07 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.) |
Theorem | sb6a 1784* | Equivalence for substitution. |
Theorem | 2sb5rf 1785* | Reversed double substitution. |
Theorem | 2sb6rf 1786* | Reversed double substitution. |
Theorem | dfsb7 1787* | An alternate definition of proper substitution df-sb 1606. By introducing a dummy variable in the definiens, we are able to eliminate any distinct variable restrictions among the variables , , and of the definiendum. No distinct variable conflicts arise because effectively insulates from . To achieve this, we use a chain of two substitutions in the form of sb5 1706, first for then for . Compare Definition 2.1'' of [Quine] p. 17. Theorem sb7f 1788 provides a version where and don't have to be distinct. |
Theorem | sb7f 1788* | This version of dfsb7 1787 does not require that and be distinct. This permits it to be used as a definition for substitution in a formalization that omits the logically redundant axiom ax-17 1402 i.e. that doesn't have the concept of a variable not occurring in a wff. (df-sb 1606 is also suitable, but its mixing of free and bound variables is distasteful to some logicians.) (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | sb10f 1789* | Hao Wang's identity axiom P6 in Irving Copi, Symbolic Logic (5th ed., 1979), p. 328. In traditional predicate calculus, this is a sole axiom for identity from which the usual ones can be derived. |
Theorem | sbid2v 1790* | An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint). |
Theorem | sbelx 1791* | Elimination of substitution. |
Theorem | sbel2x 1792* | Elimination of double substitution. |
Theorem | sbal1 1793* | A theorem used in elimination of disjoint variable restriction on and by replacing it with a distinctor . |
Theorem | sbal 1794* | Move universal quantifier in and out of substitution. |
Theorem | sbex 1795* | Move existential quantifier in and out of substitution. |
Theorem | sbalv 1796* | Quantify with new variable inside substitution. |
Theorem | exsb 1797* | An equivalent expression for existence. |
Theorem | 2exsb 1798* | An equivalent expression for double existence. |
Theorem | dvelim 1799* |
This theorem can be used to eliminate a distinct variable restriction on
and and replace it with the
"distinctor"
as an antecedent. normally has free and can be read
, and
substitutes for and can be read
. We don't require that and be distinct: if
they aren't, the distinctor will become false (in multiple-element
domains of discourse) and "protect" the consequent.
To obtain a closed-theorem form of this inference, prefix the hypotheses with , conjoin them, and apply dvelimdf 1689. Other variants of this theorem are dvelimf 1688 (with no distinct variable restrictions), dvelimfALT 1585 (that avoids ax-11 1389), and dvelimALT 1800 (that avoids ax-10 1388). |
Theorem | dvelimALT 1800* | Version of dvelim 1799 that doesn't use ax-10 1388. (See dvelimfALT 1585 for a version that doesn't use ax-11 1389.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |