Home | Intuitionistic Logic Explorer Theorem List (p. 16 of 102) | < 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 | alrimd 1501 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | eximdh 1502 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
Theorem | eximd 1503 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nexd 1504 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |
Theorem | exbidh 1505 | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |
Theorem | albid 1506 | Formula-building rule for universal quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exbid 1507 | Formula-building rule for existential quantifier (deduction rule). (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exsimpl 1508 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | exsimpr 1509 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) |
Theorem | alexdc 1510 | Theorem 19.6 of [Margaris] p. 89, given a decidability condition. The forward direction holds for all propositions, as seen at alexim 1536. (Contributed by Jim Kingdon, 2-Jun-2018.) |
DECID | ||
Theorem | 19.29 1511 | Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | 19.29r 1512 | Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
Theorem | 19.29r2 1513 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.) |
Theorem | 19.29x 1514 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
Theorem | 19.35-1 1515 | 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 1516 | Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.25 1517 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.30dc 1518 | Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.) |
DECID | ||
Theorem | 19.43 1519 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33b2 1520 | The antecedent provides a condition implying the converse of 19.33 1373. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1521 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33bdc 1521 | Converse of 19.33 1373 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 1520 (Contributed by Jim Kingdon, 23-Apr-2018.) |
DECID | ||
Theorem | 19.40 1522 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.40-2 1523 | 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 1524 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
Theorem | exintr 1525 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |
Theorem | alsyl 1526 | Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
Theorem | hbex 1527 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfex 1528 | 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 1529 | Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.) |
Theorem | i19.24 1530 | Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1515, 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 1531 | Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1515, 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 1532 | A closed version of one direction of 19.9 1535. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.9t 1533 | A closed version of 19.9 1535. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.) |
Theorem | 19.9h 1534 | 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 1535 | 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 1536 | One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1510. (Contributed by Jim Kingdon, 2-Jul-2018.) |
Theorem | exnalim 1537 | 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 1538 | A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.) |
Theorem | alexnim 1539 | A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | ax6blem 1540 | If is not free in , it is not free in . This theorem doesn't use ax6b 1541 compared to hbnt 1543. (Contributed by GD, 27-Jan-2018.) |
Theorem | ax6b 1541 |
Quantified Negation. Axiom C5-2 of [Monk2] p.
113.
(Contributed by GD, 27-Jan-2018.) |
Theorem | hbn1 1542 | is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.) |
Theorem | hbnt 1543 | Closed theorem version of bound-variable hypothesis builder hbn 1544. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | hbn 1544 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hbnd 1545 | Deduction form of bound-variable hypothesis builder hbn 1544. (Contributed by NM, 3-Jan-2002.) |
Theorem | nfnt 1546 | 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 1547 | Deduction associated with nfnt 1546. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfn 1548 | Inference associated with nfnt 1546. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfdc 1549 | If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | modal-5 1550 | The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
Theorem | 19.9d 1551 | A deduction version of one direction of 19.9 1535. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.9hd 1552 | A deduction version of one direction of 19.9 1535. This is an older variation of this theorem; new proofs should use 19.9d 1551. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | excomim 1553 | One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | excom 1554 | Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.12 1555 | 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 1556 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21-2 1557 | Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.) |
Theorem | nf2 1558 | An alternative definition of df-nf 1350, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nf3 1559 | An alternative definition of df-nf 1350. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nf4dc 1560 | Variable is effectively not free in iff is always true or always false, given a decidability condition. The reverse direction, nf4r 1561, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.) |
DECID | ||
Theorem | nf4r 1561 | 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 1560. (Contributed by Jim Kingdon, 21-Jul-2018.) |
Theorem | 19.36i 1562 | 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 1563 | Closed form of 19.36i 1562. 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 1564 | 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 1565* | Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.38 1566 | Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.23t 1567 | 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 1568 | Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.32dc 1569 | Theorem 19.32 of [Margaris] p. 90, where is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.) |
DECID | ||
Theorem | 19.32r 1570 | One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if is decidable, as seen at 19.32dc 1569. (Contributed by Jim Kingdon, 28-Jul-2018.) |
Theorem | 19.31r 1571 | 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 1572 | Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.45 1573 | Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.34 1574 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.41h 1575 | Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1576 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) |
Theorem | 19.41 1576 | 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 1577 | Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1578 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.) |
Theorem | 19.42 1578 | Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
Theorem | excom13 1579 | Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
Theorem | exrot3 1580 | Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
Theorem | exrot4 1581 | Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.) |
Theorem | nexr 1582 | Inference from 19.8a 1482. (Contributed by Jeff Hankins, 26-Jul-2009.) |
Theorem | exan 1583 | 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 1584 | Deduction form of bound-variable hypothesis builder hbex 1527. (Contributed by NM, 2-Jan-2002.) |
Theorem | eeor 1585 | Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.) |
Theorem | a9e 1586 | At least one individual exists. This is not a theorem of free logic, which is sound in empty domains. For such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10). In the system consisting of ax-5 1336 through ax-14 1405 and ax-17 1419, all axioms other than ax-9 1424 are believed to be theorems of free logic, although the system without ax-9 1424 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
Theorem | a9ev 1587* | At least one individual exists. Weaker version of a9e 1586. (Contributed by NM, 3-Aug-2017.) |
Theorem | ax9o 1588 | An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
Theorem | equid 1589 |
Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68.
This is often an axiom of equality in textbook systems, but we don't
need it as an axiom since it can be proved from our other axioms.
This proof is similar to Tarski's and makes use of a dummy variable . It also works in intuitionistic logic, unlike some other possible ways of proving this theorem. (Contributed by NM, 1-Apr-2005.) |
Theorem | nfequid 1590 | Bound-variable hypothesis builder for . This theorem tells us that any variable, including , is effectively not free in , even though is technically free according to the traditional definition of free variable. (Contributed by NM, 13-Jan-2011.) (Revised by NM, 21-Aug-2017.) |
Theorem | stdpc6 1591 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1653.) Axiom 6 of [Mendelson] p. 95. Mendelson doesn't say why he prepended the redundant quantifier, but it was probably to be compatible with free logic (which is valid in the empty domain). (Contributed by NM, 16-Feb-2005.) |
Theorem | equcomi 1592 | Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) |
Theorem | equcom 1593 | Commutative law for equality. (Contributed by NM, 20-Aug-1993.) |
Theorem | equcoms 1594 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.) |
Theorem | equtr 1595 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
Theorem | equtrr 1596 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
Theorem | equtr2 1597 | A transitive law for equality. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | equequ1 1598 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Theorem | equequ2 1599 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Theorem | elequ1 1600 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |