Home | Intuitionistic Logic Explorer Theorem List (p. 16 of 133) | < 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 | alimd 1501 | Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimi 1502 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfd 1503 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfdh 1504 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfrimi 1505 | Moving an antecedent outside . (Contributed by Jim Kingdon, 23-Mar-2018.) |
Axiom | ax-17 1506* |
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of the
preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski]
p. 77 and Axiom C5-1 of
[Monk2] p. 113.
(Contributed by NM, 5-Aug-1993.) |
Theorem | a17d 1507* | ax-17 1506 with antecedent. (Contributed by NM, 1-Mar-2013.) |
Theorem | nfv 1508* | If is not present in , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfvd 1509* | nfv 1508 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1564. (Contributed by Mario Carneiro, 6-Oct-2016.) |
Axiom | ax-i9 1510 | Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. One thing this axiom tells us is that at least one thing exists (although ax-4 1487 and possibly others also tell us that, i.e. they are not valid in the empty domain of a "free logic"). In this form (not requiring that and be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) Another name for this theorem is a9e 1674, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | ax-9 1511 | Derive ax-9 1511 from ax-i9 1510, the modified version for intuitionistic logic. Although ax-9 1511 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1510. (Contributed by NM, 3-Feb-2015.) |
Theorem | equidqe 1512 | equid 1677 with some quantification and negation without using ax-4 1487 or ax-17 1506. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) |
Theorem | ax4sp1 1513 | A special case of ax-4 1487 without using ax-4 1487 or ax-17 1506. (Contributed by NM, 13-Jan-2011.) |
Axiom | ax-ial 1514 | is not free in . One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Axiom | ax-i5r 1515 | Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | spi 1516 | Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.) |
Theorem | sps 1517 | Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | spsd 1518 | Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.) |
Theorem | nfbidf 1519 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) |
Theorem | hba1 1520 | is not free in . Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfa1 1521 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | a5i 1522 | Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfnf1 1523 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbim 1524 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Revised by Mario Carneiro, 2-Feb-2015.) |
Theorem | hbor 1525 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | hban 1526 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | hbbi 1527 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hb3or 1528 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hb3an 1529 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hba2 1530 | Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | hbia1 1531 | Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | 19.3h 1532 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 21-May-2007.) |
Theorem | 19.3 1533 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.16 1534 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.17 1535 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21h 1536 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." New proofs should use 19.21 1562 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | 19.21bi 1537 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.21bbi 1538 | Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.) |
Theorem | 19.27h 1539 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.27 1540 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28h 1541 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28 1542 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfan1 1543 | A closed form of nfan 1544. (Contributed by Mario Carneiro, 3-Oct-2016.) |
Theorem | nfan 1544 | If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) |
Theorem | nf3an 1545 | If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nford 1546 | If in a context is not free in and , it is not free in . (Contributed by Jim Kingdon, 29-Oct-2019.) |
Theorem | nfand 1547 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nf3and 1548 | Deduction form of bound-variable hypothesis builder nf3an 1545. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
Theorem | hbim1 1549 | A closed form of hbim 1524. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfim1 1550 | A closed form of nfim 1551. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | nfim 1551 | 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 1552 | Deduction form of bound-variable hypothesis builder hbim 1524. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfor 1553 | If is not free in and , it is not free in . (Contributed by Jim Kingdon, 11-Mar-2018.) |
Theorem | hbbid 1554 | Deduction form of bound-variable hypothesis builder hbbi 1527. (Contributed by NM, 1-Jan-2002.) |
Theorem | nfal 1555 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfnf 1556 | 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 1557 | Closed form of nfal 1555. (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | nfa2 1558 | Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfia1 1559 | Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.21ht 1560 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.) |
Theorem | 19.21t 1561 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |
Theorem | 19.21 1562 | 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 1563 | 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 1678. 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 1564 | If in a context is not free in and , then it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |
Theorem | aaanh 1565 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | aaan 1566 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | nfbid 1567 | If in a context is not free in and , then it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |
Theorem | nfbi 1568 | If is not free in and , then it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | 19.8a 1569 | If a wff is true, then 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.8ad 1570 | If a wff is true, it is true for at least one instance. Deduction form of 19.8a 1569. (Contributed by DAW, 13-Feb-2017.) |
Theorem | 19.23bi 1571 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exlimih 1572 | 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 1573 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exlimd2 1574 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1575 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |
Theorem | exlimdh 1575 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
Theorem | exlimd 1576 | 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 1577* |
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 1577 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 5 to arrive at the final theorem . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.) |
Theorem | exim 1578 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Theorem | eximi 1579 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2eximi 1580 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Theorem | eximii 1581 | Inference associated with eximi 1579. (Contributed by BJ, 3-Feb-2018.) |
Theorem | alinexa 1582 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
Theorem | exbi 1583 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exbii 1584 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Theorem | 2exbii 1585 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Theorem | 3exbii 1586 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Theorem | exancom 1587 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
Theorem | alrimdd 1588 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimd 1589 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | eximdh 1590 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
Theorem | eximd 1591 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nexd 1592 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
Theorem | exbidh 1593 | Formula-building rule for existential quantifier (deduction form). (Contributed by NM, 5-Aug-1993.) |
Theorem | albid 1594 | Formula-building rule for universal quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exbid 1595 | Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exsimpl 1596 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | exsimpr 1597 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | alexdc 1598 | Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1624. (Contributed by Jim Kingdon, 2-Jun-2018.) |
DECID | ||
Theorem | 19.29 1599 | Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | 19.29r 1600 | Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |