Home | Intuitionistic Logic Explorer Theorem List (p. 16 of 114) | < 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 | nf3an 1501 | If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nford 1502 | If in a context is not free in and , it is not free in . (Contributed by Jim Kingdon, 29-Oct-2019.) |
Theorem | nfand 1503 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nf3and 1504 | Deduction form of bound-variable hypothesis builder nf3an 1501. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
Theorem | hbim1 1505 | A closed form of hbim 1480. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfim1 1506 | A closed form of nfim 1507. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | nfim 1507 | If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | hbimd 1508 | Deduction form of bound-variable hypothesis builder hbim 1480. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfor 1509 | If is not free in and , it is not free in . (Contributed by Jim Kingdon, 11-Mar-2018.) |
Theorem | hbbid 1510 | Deduction form of bound-variable hypothesis builder hbbi 1483. (Contributed by NM, 1-Jan-2002.) |
Theorem | nfal 1511 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfnf 1512 | 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 | nfalt 1513 | Closed form of nfal 1511. (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | nfa2 1514 | Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfia1 1515 | Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.21ht 1516 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.) |
Theorem | 19.21t 1517 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |
Theorem | 19.21 1518 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | stdpc5 1519 | An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis can be thought of as emulating " is not free in ." With this definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example would not (for us) be free in by nfequid 1633. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
Theorem | nfimd 1520 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
Theorem | aaanh 1521 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | aaan 1522 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | nfbid 1523 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |
Theorem | nfbi 1524 | If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | 19.8a 1525 | If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.23bi 1526 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exlimih 1527 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | exlimi 1528 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exlimd2 1529 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1530 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |
Theorem | exlimdh 1530 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
Theorem | exlimd 1531 | 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 1532* |
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 1532 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 1533 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Theorem | eximi 1534 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2eximi 1535 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Theorem | eximii 1536 | Inference associated with eximi 1534. (Contributed by BJ, 3-Feb-2018.) |
Theorem | alinexa 1537 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
Theorem | exbi 1538 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exbii 1539 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Theorem | 2exbii 1540 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Theorem | 3exbii 1541 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Theorem | exancom 1542 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
Theorem | alrimdd 1543 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimd 1544 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | eximdh 1545 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
Theorem | eximd 1546 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nexd 1547 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
Theorem | exbidh 1548 | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Theorem | albid 1549 | Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exbid 1550 | Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exsimpl 1551 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | exsimpr 1552 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | alexdc 1553 | Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1579. (Contributed by Jim Kingdon, 2-Jun-2018.) |
DECID | ||
Theorem | 19.29 1554 | Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | 19.29r 1555 | Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
Theorem | 19.29r2 1556 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.) |
Theorem | 19.29x 1557 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
Theorem | 19.35-1 1558 | 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 1559 | Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.25 1560 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.30dc 1561 | Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.) |
DECID | ||
Theorem | 19.43 1562 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33b2 1563 | The antecedent provides a condition implying the converse of 19.33 1416. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1564 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33bdc 1564 | Converse of 19.33 1416 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 1563 (Contributed by Jim Kingdon, 23-Apr-2018.) |
DECID | ||
Theorem | 19.40 1565 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.40-2 1566 | 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 1567 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
Theorem | exintr 1568 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |
Theorem | alsyl 1569 | Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
Theorem | hbex 1570 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfex 1571 | 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 1572 | Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.) |
Theorem | i19.24 1573 | Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1558, 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 1574 | Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1558, 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 1575 | A closed version of one direction of 19.9 1578. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.9t 1576 | A closed version of 19.9 1578. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.) |
Theorem | 19.9h 1577 | 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 1578 | 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 1579 | One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1553. (Contributed by Jim Kingdon, 2-Jul-2018.) |
Theorem | exnalim 1580 | 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 1581 | A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.) |
Theorem | alexnim 1582 | A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | ax6blem 1583 | If is not free in , it is not free in . This theorem doesn't use ax6b 1584 compared to hbnt 1586. (Contributed by GD, 27-Jan-2018.) |
Theorem | ax6b 1584 |
Quantified Negation. Axiom C5-2 of [Monk2] p.
113.
(Contributed by GD, 27-Jan-2018.) |
Theorem | hbn1 1585 | is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.) |
Theorem | hbnt 1586 | Closed theorem version of bound-variable hypothesis builder hbn 1587. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | hbn 1587 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hbnd 1588 | Deduction form of bound-variable hypothesis builder hbn 1587. (Contributed by NM, 3-Jan-2002.) |
Theorem | nfnt 1589 | 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 1590 | Deduction associated with nfnt 1589. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfn 1591 | Inference associated with nfnt 1589. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfdc 1592 | If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | modal-5 1593 | The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
Theorem | 19.9d 1594 | A deduction version of one direction of 19.9 1578. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.9hd 1595 | A deduction version of one direction of 19.9 1578. This is an older variation of this theorem; new proofs should use 19.9d 1594. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | excomim 1596 | One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | excom 1597 | Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.12 1598 | 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 1599 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21-2 1600 | Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |