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