Home | Intuitionistic Logic Explorer Theorem 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 |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | exlimi 1501 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exlimd2 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.) |
Theorem | exlimdh 1503 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
Theorem | exlimd 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.) |
Theorem | exlimiv 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.) |
Theorem | exim 1506 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Theorem | eximi 1507 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2eximi 1508 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Theorem | eximii 1509 | Inference associated with eximi 1507. (Contributed by BJ, 3-Feb-2018.) |
Theorem | alinexa 1510 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
Theorem | exbi 1511 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exbii 1512 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Theorem | 2exbii 1513 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Theorem | 3exbii 1514 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Theorem | exancom 1515 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
Theorem | alrimdd 1516 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimd 1517 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | eximdh 1518 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
Theorem | eximd 1519 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nexd 1520 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
Theorem | exbidh 1521 | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Theorem | albid 1522 | Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exbid 1523 | Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exsimpl 1524 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | exsimpr 1525 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | alexdc 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 | ||
Theorem | 19.29 1527 | Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | 19.29r 1528 | Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
Theorem | 19.29r2 1529 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.) |
Theorem | 19.29x 1530 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
Theorem | 19.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.) |
Theorem | 19.35i 1532 | Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.25 1533 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.30dc 1534 | Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.) |
DECID | ||
Theorem | 19.43 1535 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.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.) |
Theorem | 19.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 | ||
Theorem | 19.40 1538 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.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.) |
Theorem | exintrbi 1540 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
Theorem | exintr 1541 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |
Theorem | alsyl 1542 | Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
Theorem | hbex 1543 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfex 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.) |
Theorem | 19.2 1545 | Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.) |
Theorem | i19.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.) |
Theorem | i19.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.) |
Theorem | 19.9ht 1548 | A closed version of one direction of 19.9 1551. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | alexim 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.) |
Theorem | exnalim 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.) |
Theorem | exanaliim 1554 | A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.) |
Theorem | alexnim 1555 | A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | ax6blem 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.) |
Theorem | ax6b 1557 |
Quantified Negation. Axiom C5-2 of [Monk2] p.
113.
(Contributed by GD, 27-Jan-2018.) |
Theorem | hbn1 1558 | is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.) |
Theorem | hbnt 1559 | Closed theorem version of bound-variable hypothesis builder hbn 1560. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | hbn 1560 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hbnd 1561 | Deduction form of bound-variable hypothesis builder hbn 1560. (Contributed by NM, 3-Jan-2002.) |
Theorem | nfnt 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.) |
Theorem | nfnd 1563 | Deduction associated with nfnt 1562. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfn 1564 | Inference associated with nfnt 1562. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfdc 1565 | If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | modal-5 1566 | The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | excomim 1569 | One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | excom 1570 | Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.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.) |
Theorem | 19.19 1572 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21-2 1573 | Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.) |
Theorem | nf2 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.) |
Theorem | nf3 1575 | An alternative definition of df-nf 1366. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nf4dc 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 | ||
Theorem | nf4r 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.) |
Theorem | 19.36i 1578 | Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | 19.37aiv 1581* | Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.38 1582 | Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.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.) |
Theorem | 19.23 1584 | Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.32dc 1585 | Theorem 19.32 of [Margaris] p. 90, where is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.) |
DECID | ||
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | 19.44 1588 | Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.45 1589 | Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.34 1590 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | 19.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.) |
Theorem | 19.42 1594 | Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
Theorem | excom13 1595 | Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
Theorem | exrot3 1596 | Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
Theorem | exrot4 1597 | Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.) |
Theorem | nexr 1598 | Inference from 19.8a 1498. (Contributed by Jeff Hankins, 26-Jul-2009.) |
Theorem | exan 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.) |
Theorem | hbexd 1600 | Deduction form of bound-variable hypothesis builder hbex 1543. (Contributed by NM, 2-Jan-2002.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |