Home | Intuitionistic Logic Explorer Theorem List (p. 17 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 | 19.29r2 1601 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.) |
Theorem | 19.29x 1602 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |
Theorem | 19.35-1 1603 | 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 1604 | Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.25 1605 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | 19.30dc 1606 | Theorem 19.30 of [Margaris] p. 90, with an additional decidability condition. (Contributed by Jim Kingdon, 21-Jul-2018.) |
DECID | ||
Theorem | 19.43 1607 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33b2 1608 | The antecedent provides a condition implying the converse of 19.33 1460. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1609 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33bdc 1609 | Converse of 19.33 1460 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 1608 (Contributed by Jim Kingdon, 23-Apr-2018.) |
DECID | ||
Theorem | 19.40 1610 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.40-2 1611 | 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 1612 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |
Theorem | exintr 1613 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |
Theorem | alsyl 1614 | Theorem *10.3 in [WhiteheadRussell] p. 150. (Contributed by Andrew Salmon, 8-Jun-2011.) |
Theorem | hbex 1615 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfex 1616 | 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 1617 | Theorem 19.2 of [Margaris] p. 89, generalized to use two setvar variables. (Contributed by O'Cat, 31-Mar-2008.) |
Theorem | i19.24 1618 | Theorem 19.24 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1603, 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 1619 | Theorem 19.39 of [Margaris] p. 90, with an additional hypothesis. The hypothesis is the converse of 19.35-1 1603, 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 1620 | A closed version of one direction of 19.9 1623. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.9t 1621 | A closed version of 19.9 1623. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.) |
Theorem | 19.9h 1622 | 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 1623 | 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 1624 | One direction of theorem 19.6 of [Margaris] p. 89. The converse holds given a decidability condition, as seen at alexdc 1598. (Contributed by Jim Kingdon, 2-Jul-2018.) |
Theorem | exnalim 1625 | 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 1626 | A transformation of quantifiers and logical connectives. In classical logic the converse also holds. (Contributed by Jim Kingdon, 15-Jul-2018.) |
Theorem | alexnim 1627 | A relationship between two quantifiers and negation. (Contributed by Jim Kingdon, 27-Aug-2018.) |
Theorem | ax6blem 1628 | If is not free in , it is not free in . This theorem doesn't use ax6b 1629 compared to hbnt 1631. (Contributed by GD, 27-Jan-2018.) |
Theorem | ax6b 1629 |
Quantified Negation. Axiom C5-2 of [Monk2] p.
113.
(Contributed by GD, 27-Jan-2018.) |
Theorem | hbn1 1630 | is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.) |
Theorem | hbnt 1631 | Closed theorem version of bound-variable hypothesis builder hbn 1632. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | hbn 1632 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hbnd 1633 | Deduction form of bound-variable hypothesis builder hbn 1632. (Contributed by NM, 3-Jan-2002.) |
Theorem | nfnt 1634 | 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 1635 | Deduction associated with nfnt 1634. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfn 1636 | Inference associated with nfnt 1634. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfdc 1637 | If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | modal-5 1638 | The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.) |
Theorem | 19.9d 1639 | A deduction version of one direction of 19.9 1623. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.9hd 1640 | A deduction version of one direction of 19.9 1623. This is an older variation of this theorem; new proofs should use 19.9d 1639. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | excomim 1641 | One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | excom 1642 | Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.12 1643 | 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 1644 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21-2 1645 | Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. (Contributed by NM, 4-Feb-2005.) |
Theorem | nf2 1646 | An alternate definition of df-nf 1437, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nf3 1647 | An alternate definition of df-nf 1437. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nf4dc 1648 | Variable is effectively not free in iff is always true or always false, given a decidability condition. The reverse direction, nf4r 1649, holds for all propositions. (Contributed by Jim Kingdon, 21-Jul-2018.) |
DECID | ||
Theorem | nf4r 1649 | 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 1648. (Contributed by Jim Kingdon, 21-Jul-2018.) |
Theorem | 19.36i 1650 | 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 1651 | Closed form of 19.36i 1650. 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 1652 | 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 1653* | Inference from Theorem 19.37 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.38 1654 | Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.23t 1655 | 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 1656 | Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.32dc 1657 | Theorem 19.32 of [Margaris] p. 90, where is decidable. (Contributed by Jim Kingdon, 4-Jun-2018.) |
DECID | ||
Theorem | 19.32r 1658 | One direction of Theorem 19.32 of [Margaris] p. 90. The converse holds if is decidable, as seen at 19.32dc 1657. (Contributed by Jim Kingdon, 28-Jul-2018.) |
Theorem | 19.31r 1659 | 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 1660 | Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.45 1661 | Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.34 1662 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.41h 1663 | Theorem 19.41 of [Margaris] p. 90. New proofs should use 19.41 1664 instead. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) (New usage is discouraged.) |
Theorem | 19.41 1664 | 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 1665 | Theorem 19.42 of [Margaris] p. 90. New proofs should use 19.42 1666 instead. (Contributed by NM, 18-Aug-1993.) (New usage is discouraged.) |
Theorem | 19.42 1666 | Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |
Theorem | excom13 1667 | Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.) |
Theorem | exrot3 1668 | Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.) |
Theorem | exrot4 1669 | Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.) |
Theorem | nexr 1670 | Inference from 19.8a 1569. (Contributed by Jeff Hankins, 26-Jul-2009.) |
Theorem | exan 1671 | 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 1672 | Deduction form of bound-variable hypothesis builder hbex 1615. (Contributed by NM, 2-Jan-2002.) |
Theorem | eeor 1673 | Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.) |
Theorem | a9e 1674 | 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 1423 through ax-14 1492 and ax-17 1506, all axioms other than ax-9 1511 are believed to be theorems of free logic, although the system without ax-9 1511 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
Theorem | a9ev 1675* | At least one individual exists. Weaker version of a9e 1674. (Contributed by NM, 3-Aug-2017.) |
Theorem | ax9o 1676 | An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
Theorem | equid 1677 |
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 1678 | 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 1679 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1743.) 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 1680 | Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) |
Theorem | ax6evr 1681* | A commuted form of a9ev 1675. The naming reflects how axioms were numbered in the Metamath Proof Explorer as of 2020 (a numbering which we eventually plan to adopt here too, but until this happens everywhere only some theorems will have it). (Contributed by BJ, 7-Dec-2020.) |
Theorem | equcom 1682 | Commutative law for equality. (Contributed by NM, 20-Aug-1993.) |
Theorem | equcomd 1683 | Deduction form of equcom 1682, symmetry of equality. For the versions for classes, see eqcom 2141 and eqcomd 2145. (Contributed by BJ, 6-Oct-2019.) |
Theorem | equcoms 1684 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.) |
Theorem | equtr 1685 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |
Theorem | equtrr 1686 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |
Theorem | equtr2 1687 | A transitive law for equality. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Theorem | equequ1 1688 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Theorem | equequ2 1689 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |
Theorem | elequ1 1690 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
Theorem | elequ2 1691 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |
Theorem | ax11i 1692 | Inference that has ax-11 1484 (without ) as its conclusion and doesn't require ax-10 1483, ax-11 1484, or ax-12 1489 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 1693 |
Show that ax-10o 1694 can be derived from ax-10 1483. An open problem is
whether this theorem can be derived from ax-10 1483 and the others when
ax-11 1484 is replaced with ax-11o 1795. See theorem ax10 1695
for the
rederivation of ax-10 1483 from ax10o 1693.
Normally, ax10o 1693 should be used rather than ax-10o 1694, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) |
Axiom | ax-10o 1694 |
Axiom ax-10o 1694 ("o" for "old") was the
original version of ax-10 1483,
before it was discovered (in May 2008) that the shorter ax-10 1483 could
replace it. It appears as Axiom scheme C11' in [Megill] p. 448 (p. 16 of
the preprint).
This axiom is redundant, as shown by theorem ax10o 1693. Normally, ax10o 1693 should be used rather than ax-10o 1694, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | ax10 1695 |
Rederivation of ax-10 1483 from original version ax-10o 1694. See theorem
ax10o 1693 for the derivation of ax-10o 1694 from ax-10 1483.
This theorem should not be referenced in any proof. Instead, use ax-10 1483 above so that uses of ax-10 1483 can be more easily identified. (Contributed by NM, 16-May-2008.) (New usage is discouraged.) |
Theorem | hbae 1696 | All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |
Theorem | nfae 1697 | All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbaes 1698 | Rule that applies hbae 1696 to antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | hbnae 1699 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | nfnae 1700 | All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |