Home Intuitionistic Logic ExplorerTheorem List (p. 16 of 106) < Previous  Next > Browser slow? Try the Unicode version. Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1501-1600   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremexlimi 1501 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremexlimd2 1502 Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1503 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.)

Theoremexlimdh 1503 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)

Theoremexlimd 1504 Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.)

Theoremexlimiv 1505* 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 1505 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 7 to arrive at the final theorem . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.)

Theoremexim 1506 Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)

Theoremeximi 1507 Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)

Theorem2eximi 1508 Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)

Theoremeximii 1509 Inference associated with eximi 1507. (Contributed by BJ, 3-Feb-2018.)

Theoremalinexa 1510 A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)

Theoremexbi 1511 Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Theoremexbii 1512 Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)

Theorem2exbii 1513 Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Theorem3exbii 1514 Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)

Theoremexancom 1515 Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)

Theoremalrimdd 1516 Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremalrimd 1517 Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremeximdh 1518 Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)

Theoremeximd 1519 Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremnexd 1520 Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)

Theoremexbidh 1521 Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)

Theoremalbid 1522 Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremexbid 1523 Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremexsimpl 1524 Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Theoremexsimpr 1525 Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)

Theoremalexdc 1526 Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1552. (Contributed by Jim Kingdon, 2-Jun-2018.)
DECID

Theorem19.29 1527 Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Theorem19.29r 1528 Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)

Theorem19.29r2 1529 Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)

Theorem19.29x 1530 Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)

Theorem19.35-1 1531 Forward direction of Theorem 19.35 of [Margaris] p. 90. The converse holds for classical logic but not (for all propositions) in intuitionistic logic (Contributed by Mario Carneiro, 2-Feb-2015.)

Theorem19.35i 1532 Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)

Theorem19.25 1533 Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)

Theorem19.30dc 1534 Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.)
DECID

Theorem19.43 1535 Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)

Theorem19.33b2 1536 The antecedent provides a condition implying the converse of 19.33 1389. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1537 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.)

Theorem19.33bdc 1537 Converse of 19.33 1389 given and a decidability condition. Compare Theorem 19.33 of [Margaris] p. 90. For a version which does not require a decidability condition, see 19.33b2 1536 (Contributed by Jim Kingdon, 23-Apr-2018.)
DECID

Theorem19.40 1538 Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Theorem19.40-2 1539 Theorem *11.42 in [WhiteheadRussell] p. 163. Theorem 19.40 of [Margaris] p. 90 with 2 quantifiers. (Contributed by Andrew Salmon, 24-May-2011.)

Theoremexintrbi 1540 Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)

Theoremexintr 1541 Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)

Theoremalsyl 1542 Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.)

Theoremhbex 1543 If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)

Theoremnfex 1544 If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

Theorem19.2 1545 Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.)

Theoremi19.24 1546 Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1531, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)

Theoremi19.39 1547 Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1531, and is a theorem of classical logic, but in intuitionistic logic it will only be provable for some propositions. (Contributed by Jim Kingdon, 22-Jul-2018.)

Theorem19.9ht 1548 A closed version of one direction of 19.9 1551. (Contributed by NM, 5-Aug-1993.)

Theorem19.9t 1549 A closed version of 19.9 1551. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.)

Theorem19.9h 1550 A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.)

Theorem19.9 1551 A wff may be existentially quantified with a variable not free in it. Theorem 19.9 of [Margaris] p. 89. (Contributed by FL, 24-Mar-2007.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.)

Theoremalexim 1552 One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1526. (Contributed by Jim Kingdon, 2-Jul-2018.)

Theoremexnalim 1553 One direction of Theorem 19.14 of [Margaris] p. 90. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)

Theoremexanaliim 1554 A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.)

Theoremalexnim 1555 A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.)

Theoremax6blem 1556 If is not free in , it is not free in . This theorem doesn't use ax6b 1557 compared to hbnt 1559. (Contributed by GD, 27-Jan-2018.)

Theoremax6b 1557 Quantified Negation. Axiom C5-2 of [Monk2] p. 113.

(Contributed by GD, 27-Jan-2018.)

Theoremhbn1 1558 is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)

Theoremhbnt 1559 Closed theorem version of bound-variable hypothesis builder hbn 1560. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)

Theoremhbn 1560 If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.)

Theoremhbnd 1561 Deduction form of bound-variable hypothesis builder hbn 1560. (Contributed by NM, 3-Jan-2002.)

Theoremnfnt 1562 If is not free in , then it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) (Revised by BJ, 24-Jul-2019.)

Theoremnfnd 1563 Deduction associated with nfnt 1562. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremnfn 1564 Inference associated with nfnt 1562. (Contributed by Mario Carneiro, 11-Aug-2016.)

Theoremnfdc 1565 If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.)
DECID

Theoremmodal-5 1566 The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)

Theorem19.9d 1567 A deduction version of one direction of 19.9 1551. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Theorem19.9hd 1568 A deduction version of one direction of 19.9 1551. This is an older variation of this theorem; new proofs should use 19.9d 1567. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)

Theoremexcomim 1569 One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Theoremexcom 1570 Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Theorem19.12 1571 Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! (Contributed by NM, 5-Aug-1993.)

Theorem19.19 1572 Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Theorem19.21-2 1573 Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.)

Theoremnf2 1574 An alternative definition of df-nf 1366, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremnf3 1575 An alternative definition of df-nf 1366. (Contributed by Mario Carneiro, 24-Sep-2016.)

Theoremnf4dc 1576 Variable is effectively not free in iff is always true or always false, given a decidability condition. The reverse direction, nf4r 1577, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.)
DECID

Theoremnf4r 1577 If is always true or always false, then variable is effectively not free in . The converse holds given a decidability condition, as seen at nf4dc 1576. (Contributed by Jim Kingdon, 21-Jul-2018.)

Theorem19.36i 1578 Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)

Theorem19.36-1 1579 Closed form of 19.36i 1578. One direction of Theorem 19.36 of [Margaris] p. 90. The converse holds in classical logic, but does not hold (for all propositions) in intuitionistic logic. (Contributed by Jim Kingdon, 20-Jun-2018.)

Theorem19.37-1 1580 One direction of Theorem 19.37 of [Margaris] p. 90. The converse holds in classical logic but not, in general, here. (Contributed by Jim Kingdon, 21-Jun-2018.)

Theorem19.37aiv 1581* Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Theorem19.38 1582 Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Theorem19.23t 1583 Closed form of Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 7-Nov-2005.) (Proof shortened by Wolf Lammen, 2-Jan-2018.)

Theorem19.23 1584 Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.)

Theorem19.32dc 1585 Theorem 19.32 of [Margaris] p. 90, where is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.)
DECID

Theorem19.32r 1586 One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if is decidable, as seen at 19.32dc 1585. (Contributed by Jim Kingdon, 28-Jul-2018.)

Theorem19.31r 1587 One direction of Theorem 19.31 of [Margaris] p. 90. The converse holds in classical logic, but not intuitionistic logic. (Contributed by Jim Kingdon, 28-Jul-2018.)

Theorem19.44 1588 Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Theorem19.45 1589 Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)

Theorem19.34 1590 Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)

Theorem19.41h 1591 Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1592 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.)

Theorem19.41 1592 Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 12-Jan-2018.)

Theorem19.42h 1593 Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1594 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.)

Theorem19.42 1594 Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)

Theoremexcom13 1595 Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.)

Theoremexrot3 1596 Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)

Theoremexrot4 1597 Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)

Theoremnexr 1598 Inference from 19.8a 1498. (Contributed by Jeff Hankins, 26-Jul-2009.)

Theoremexan 1599 Place a conjunct in the scope of an existential quantifier. (Contributed by NM, 18-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Theoremhbexd 1600 Deduction form of bound-variable hypothesis builder hbex 1543. (Contributed by NM, 2-Jan-2002.)

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-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-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10511
 Copyright terms: Public domain < Previous  Next >