HomeHome Intuitionistic Logic Explorer
Theorem List (p. 18 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1701-1800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremsb9i 1701 Commutation of quantification and substitution variables.
 
Theoremsb9 1702 Commutation of quantification and substitution variables.
 
1.5.4  Predicate calculus with distinct variables (cont.)
 
Theoremax11v 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.
 
Theoremsb56 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.
 
Theoremsb6 1705* Equivalence for substitution. Compare Theorem 6.2 of [Quine] p. 40. Also proved as Lemmas 16 and 17 of [Tarski] p. 70.
 
Theoremsb5 1706* Equivalence for substitution. Similar to Theorem 6.1 of [Quine] p. 40.
 
Theoremax16i 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.
   &       =>   
 
Theoremax16ALT 1708* Version of ax16 1643 that doesn't require ax-10 1388 or ax-12 1393 for its proof.
 
Theorema4v 1709* Specialization, using implicit substitition.
   =>   
 
Theorema4imev 1710* Distinct-variable version of a4ime 1593.
   =>   
 
Theorema4eiv 1711* Inference from existential specialization, using implicit substitition.
   &       =>   
 
Theoremequvin 1712* A variable introduction law for equality. Lemma 15 of [Monk2] p. 109.
 
Theorema16g 1713* A generalization of axiom ax-16 1644. (The proof was shortened by Andrew Salmon, 25-May-2011.)
 
Theorema16gb 1714* A generalization of axiom ax-16 1644.
 
Theoremalbidv 1715* Formula-building rule for universal quantifier (deduction rule).
   =>   
 
Theoremexbidv 1716* Formula-building rule for existential quantifier (deduction rule).
   =>   
 
Theorem2albidv 1717* Formula-building rule for 2 existential quantifiers (deduction rule).
   =>   
 
Theorem2exbidv 1718* Formula-building rule for 2 existential quantifiers (deduction rule).
   =>   
 
Theorem3exbidv 1719* Formula-building rule for 3 existential quantifiers (deduction rule).
   =>   
 
Theorem4exbidv 1720* Formula-building rule for 4 existential quantifiers (deduction rule).
   =>   
 
Theorem19.9v 1721* Special case of Theorem 19.9 of [Margaris] p. 89.
 
Theorem19.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."
 
Theoremalrimiv 1723* Inference from Theorem 19.21 of [Margaris] p. 90.
   =>   
 
Theoremalrimivv 1724* Inference from Theorem 19.21 of [Margaris] p. 90.
   =>   
 
Theoremalrimdv 1725* Deduction from Theorem 19.21 of [Margaris] p. 90.
   =>   
 
Theorem2ax17 1726* Quantification of two variables over a formula in which they do not occur. (Contributed by Alan Sare, 12-Apr-2011.)
 
Theoremalimdv 1727* Deduction from Theorem 19.20 of [Margaris] p. 90.
   =>   
 
Theoremeximdv 1728* Deduction from Theorem 19.22 of [Margaris] p. 90.
   =>   
 
Theorem2alimdv 1729* Deduction from Theorem 19.22 of [Margaris] p. 90.
   =>   
 
Theorem2eximdv 1730* Deduction from Theorem 19.22 of [Margaris] p. 90.
   =>   
 
Theorem19.23v 1731* Special case of Theorem 19.23 of [Margaris] p. 90.
 
Theorem19.23vv 1732* Theorem 19.23 of [Margaris] p. 90 extended to two variables.
 
Theoremexlimiv 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 .

   =>   
 
Theorempm11.53 1734* Theorem *11.53 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
 
Theoremexlimivv 1735* Inference from Theorem 19.23 of [Margaris] p. 90.
   =>   
 
Theoremexlimdvv 1736* Deduction from Theorem 19.23 of [Margaris] p. 90.
   =>   
 
Theorem19.27v 1737* Theorem 19.27 of [Margaris] p. 90.
 
Theorem19.28v 1738* Theorem 19.28 of [Margaris] p. 90.
 
Theorem19.36v 1739* Special case of Theorem 19.36 of [Margaris] p. 90.
 
Theorem19.36aiv 1740* Inference from Theorem 19.36 of [Margaris] p. 90.
   =>   
 
Theorem19.12vv 1741* Special case of 19.12 1535 where its converse holds. (Unnecessary distinct variable restrictions were removed by Andrew Salmon, 11-Jul-2011.)
 
Theorem19.37v 1742* Special case of Theorem 19.37 of [Margaris] p. 90.
 
Theorem19.37aiv 1743* Inference from Theorem 19.37 of [Margaris] p. 90.
   =>   
 
Theorem19.41v 1744* Special case of Theorem 19.41 of [Margaris] p. 90.
 
Theorem19.41vv 1745* Theorem 19.41 of [Margaris] p. 90 with 2 quantifiers.
 
Theorem19.41vvv 1746* Theorem 19.41 of [Margaris] p. 90 with 3 quantifiers.
 
Theorem19.41vvvv 1747* Theorem 19.41 of [Margaris] p. 90 with 4 quantifiers. (Contributed by FL, 14-Jul-2007.)
 
Theorem19.42v 1748* Special case of Theorem 19.42 of [Margaris] p. 90.
 
Theoremexdistr 1749* Distribution of existential quantifiers.
 
Theorem19.42vv 1750* Theorem 19.42 of [Margaris] p. 90 with 2 quantifiers.
 
Theorem19.42vvv 1751* Theorem 19.42 of [Margaris] p. 90 with 3 quantifiers.
 
Theoremexdistr2 1752* Distribution of existential quantifiers.
 
Theorem3exdistr 1753* Distribution of existential quantifiers. (The proof was shortened by Andrew Salmon, 25-May-2011.)
 
Theorem4exdistr 1754* Distribution of existential quantifiers.
 
Theoremcbvalv 1755* Rule used to change bound variables, using implicit substitition.
   =>   
 
Theoremcbvexv 1756* Rule used to change bound variables, using implicit substitition.
   =>   
 
Theoremcbval2 1757* Rule used to change bound variables, using implicit substitition.
   &       &       &       &       =>   
 
Theoremcbvex2 1758* Rule used to change bound variables, using implicit substitition.
   &       &       &       &       =>   
 
Theoremcbval2v 1759* Rule used to change bound variables, using implicit substitition.
   =>   
 
Theoremcbvex2v 1760* Rule used to change bound variables, using implicit substitition.
   =>   
 
Theoremcbvald 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.)
   &       &       =>   
 
Theoremcbvexd 1762* Deduction used to change bound variables, using implicit substitition, particularly useful in conjunction with dvelim 1799.
   &       &       =>   
 
Theoremcbvex4v 1763* Rule used to change bound variables, using implicit substitition.
   &       =>   
 
Theoremeean 1764 Rearrange existential quantifiers.
   &       =>   
 
Theoremeeanv 1765* Rearrange existential quantifiers.
 
Theoremeeeanv 1766* Rearrange existential quantifiers. (The proof was shortened by Andrew Salmon, 25-May-2011.)
 
Theoremee4anv 1767* Rearrange existential quantifiers.
 
Theoremnexdv 1768* Deduction for generalization rule for negated wff.
   =>   
 
Theoremchvarv 1769* Implicit substitution of for into a theorem.
   &       =>   
 
Theoremcleljust 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.
 
1.5.5  More substitution theorems
 
Theoremequsb3lem 1771* Lemma for equsb3 1772. (The proof was shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremequsb3 1772* Substitution applied to an atomic wff. (Contributed by Raph Levien and FL, 4-Dec-2005.)
 
Theoremelsb3 1773* Substitution applied to an atomic membership wff. (The proof was shortened by Andrew Salmon, 14-Jun-2011.)
 
Theoremelsb4 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.)
 
Theoremhbs1 1775* is not free in when and are distinct.
 
Theoremsbhb 1776* Two ways of expressing " is (effectively) not free in ."
 
Theoremsbhb2 1777* Two ways of expressing " is (effectively) not free in ." (Contributed by Gérard Lang, 14-Nov-2013.)
 
Theoremhbsb 1778* If is not free in , it is not free in when and are distinct.
   =>   
 
Theoremhbsbd 1779* Deduction version of hbsb 1778.
   &       &       =>   
 
Theorem2sb5 1780* Equivalence for double substitution.
 
Theorem2sb6 1781* Equivalence for double substitution.
 
Theoremsbcom2 1782* Commutativity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint).
 
Theorempm11.07 1783* Theorem *11.07 in [WhiteheadRussell] p. 159. (Contributed by Andrew Salmon, 17-Jun-2011.)
 
Theoremsb6a 1784* Equivalence for substitution.
 
Theorem2sb5rf 1785* Reversed double substitution.
   &       =>   
 
Theorem2sb6rf 1786* Reversed double substitution.
   &       =>   
 
Theoremdfsb7 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.
 
Theoremsb7f 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.)
   =>   
 
Theoremsb10f 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.
   =>   
 
Theoremsbid2v 1790* An identity law for substitution. Used in proof of Theorem 9.7 of [Megill] p. 449 (p. 16 of the preprint).
 
Theoremsbelx 1791* Elimination of substitution.
 
Theoremsbel2x 1792* Elimination of double substitution.
 
Theoremsbal1 1793* A theorem used in elimination of disjoint variable restriction on and by replacing it with a distinctor .
 
Theoremsbal 1794* Move universal quantifier in and out of substitution.
 
Theoremsbex 1795* Move existential quantifier in and out of substitution.
 
Theoremsbalv 1796* Quantify with new variable inside substitution.
   =>   
 
Theoremexsb 1797* An equivalent expression for existence.
 
Theorem2exsb 1798* An equivalent expression for double existence.
 
Theoremdvelim 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).

   &       =>   
 
TheoremdvelimALT 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 >

Page List
Jump to page: Contents  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-1914
  Copyright terms: Public domain < Previous  Next >