Home | Intuitionistic Logic Explorer Theorem List (p. 16 of 139) | < 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 | axi12 1501 | Proof that ax-i12 1494 follows from ax-bndl 1496. So that we can track which theorems rely on ax-bndl 1496, proofs should reference ax12or 1495 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.) |
Theorem | alequcom 1502 | Commutation law for identical variable specifiers. The antecedent and consequent are true when and are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | alequcoms 1503 | A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.) |
Theorem | nalequcoms 1504 | A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 2-Feb-2015.) |
Theorem | nfr 1505 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) |
Theorem | nfri 1506 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfrd 1507 | Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | alimd 1508 | Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimi 1509 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfd 1510 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfdh 1511 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfrimi 1512 | Moving an antecedent outside . (Contributed by Jim Kingdon, 23-Mar-2018.) |
Axiom | ax-17 1513* |
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 1514* | ax-17 1513 with antecedent. (Contributed by NM, 1-Mar-2013.) |
Theorem | nfv 1515* | If is not present in , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfvd 1516* | nfv 1515 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1572. (Contributed by Mario Carneiro, 6-Oct-2016.) |
Axiom | ax-i9 1517 | 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 1497 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 1683, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | ax-9 1518 | Derive ax-9 1518 from ax-i9 1517, the modified version for intuitionistic logic. Although ax-9 1518 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1517. (Contributed by NM, 3-Feb-2015.) |
Theorem | equidqe 1519 | equid 1688 with some quantification and negation without using ax-4 1497 or ax-17 1513. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) |
Theorem | ax4sp1 1520 | A special case of ax-4 1497 without using ax-4 1497 or ax-17 1513. (Contributed by NM, 13-Jan-2011.) |
Axiom | ax-ial 1521 | is not free in . One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Axiom | ax-i5r 1522 | Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | spi 1523 | Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.) |
Theorem | sps 1524 | Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | spsd 1525 | Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.) |
Theorem | nfbidf 1526 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) |
Theorem | hba1 1527 | 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 1528 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | axc4i 1529 | Inference version of 19.21 1570. (Contributed by NM, 3-Jan-1993.) |
Theorem | a5i 1530 | Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfnf1 1531 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbim 1532 | 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 1533 | 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 1534 | 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 1535 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hb3or 1536 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hb3an 1537 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hba2 1538 | Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | hbia1 1539 | Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | 19.3h 1540 | 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 1541 | 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 1542 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.17 1543 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21h 1544 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ". New proofs should use 19.21 1570 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | 19.21bi 1545 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.21bbi 1546 | Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.) |
Theorem | 19.27h 1547 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.27 1548 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28h 1549 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28 1550 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfan1 1551 | A closed form of nfan 1552. (Contributed by Mario Carneiro, 3-Oct-2016.) |
Theorem | nfan 1552 | 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 1553 | If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nford 1554 | If in a context is not free in and , it is not free in . (Contributed by Jim Kingdon, 29-Oct-2019.) |
Theorem | nfand 1555 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nf3and 1556 | Deduction form of bound-variable hypothesis builder nf3an 1553. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
Theorem | hbim1 1557 | A closed form of hbim 1532. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfim1 1558 | A closed form of nfim 1559. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | nfim 1559 | 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 1560 | Deduction form of bound-variable hypothesis builder hbim 1532. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfor 1561 | If is not free in and , it is not free in . (Contributed by Jim Kingdon, 11-Mar-2018.) |
Theorem | hbbid 1562 | Deduction form of bound-variable hypothesis builder hbbi 1535. (Contributed by NM, 1-Jan-2002.) |
Theorem | nfal 1563 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) Remove dependency on ax-4 1497. (Revised by Gino Giotto, 25-Aug-2024.) |
Theorem | nfnf 1564 | 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 1565 | Closed form of nfal 1563. (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | nfa2 1566 | Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfia1 1567 | Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.21ht 1568 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.) |
Theorem | 19.21t 1569 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |
Theorem | 19.21 1570 | 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 1571 | 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 1689. 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 1572 | 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 1573 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | aaan 1574 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | nfbid 1575 | 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 1576 | 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 1577 | 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 1578 | If a wff is true, it is true for at least one instance. Deduction form of 19.8a 1577. (Contributed by DAW, 13-Feb-2017.) |
Theorem | 19.23bi 1579 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exlimih 1580 | 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 1581 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exlimd2 1582 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1583 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |
Theorem | exlimdh 1583 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
Theorem | exlimd 1584 | 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 1585* |
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 1585 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 1586 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Theorem | eximi 1587 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2eximi 1588 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Theorem | eximii 1589 | Inference associated with eximi 1587. (Contributed by BJ, 3-Feb-2018.) |
Theorem | alinexa 1590 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
Theorem | exbi 1591 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exbii 1592 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Theorem | 2exbii 1593 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Theorem | 3exbii 1594 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Theorem | exancom 1595 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
Theorem | alrimdd 1596 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimd 1597 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | eximdh 1598 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
Theorem | eximd 1599 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nexd 1600 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |