Home | Intuitionistic Logic Explorer Theorem List (p. 16 of 20) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | 19.29x 1501 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. |
Theorem | alex 1502 | Theorem 19.6 of [Margaris] p. 89. |
Theorem | 2nalexn 1503 | Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) |
Theorem | exnal 1504 | Theorem 19.14 of [Margaris] p. 90. |
Theorem | alexn 1505 | A relationship between two quantifiers and negation. |
Theorem | 2exnexn 1506 | Theorem *11.51 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.) (The proof was shortened by Wolf Lammen, 25-Sep-2014.) |
Theorem | 2exnexnOLD 1507 | Obsolete proof of 2exnexn 1506 as of 25-Sep-2014. |
Theorem | exanali 1508 | A transformation of quantifiers and logical connectives. (The proof was shortened by Wolf Lammen, 4-Sep-2014.) |
Theorem | exanaliOLD 1509 | Obsolete proof of exanali 1508 as of 4-Sep-2014. |
Theorem | 19.35-1 1510 | Forward direction of Theorem 19.35 of [Margaris] p. 90. (Contributed by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.35 1511 | Theorem 19.35 of [Margaris] p. 90. This theorem is useful for moving an implication (in the form of the right-hand side) into the scope of a single existential quantifier. (The proof was shortened by Wolf Lammen, 27-Jun-2014.) |
Theorem | 19.35OLD 1512 | Obsolete proof of 19.35 1511 as of 27-Jun-2014. |
Theorem | 19.35i 1513 | Inference from Theorem 19.35 of [Margaris] p. 90. |
Theorem | 19.35ri 1514 | Inference from Theorem 19.35 of [Margaris] p. 90. |
Theorem | 19.25 1515 | Theorem 19.25 of [Margaris] p. 90. |
Theorem | 19.30 1516 | Theorem 19.30 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | 19.43 1517 | Theorem 19.43 of [Margaris] p. 90. (The proof was shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.43OLD 1518 | Obsolete proof of 19.43 1517 as of 27-Jun-2014. |
Theorem | 19.33b2 1519 | The antecedent provides a condition implying the converse of 19.33 1365. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33b 1520 is intuitionistically valid with a slight modification of the antecedent. (Contributed by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33b 1520 | The antecedent provides a condition implying the converse of 19.33 1365. Compare Theorem 19.33 of [Margaris] p. 90. (The proof was shortened by Wolf Lammen, 5-Jul-2014.) (The proof was shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | 19.33bOLD 1521 | Obsolete proof of 19.33b 1520 as of 22-Mar-2014. |
Theorem | 19.40 1522 | Theorem 19.40 of [Margaris] p. 90. |
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. |
Theorem | equs3 1526 | Lemma used in proofs of substitution properties. |
Theorem | a6e 1527 | Abbreviated version of ax-6o 1428. |
Theorem | hbex 1528 | If is not free in , it is not free in . |
Theorem | 19.2 1529 | Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.) |
Theorem | 19.9t 1530 | A closed version of one direction of 19.9 1531. |
Theorem | 19.9 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.9d 1532 | A deduction version of one direction of 19.9 1531. |
Theorem | excomim 1533 | One direction of Theorem 19.11 of [Margaris] p. 89. |
Theorem | excom 1534 | Theorem 19.11 of [Margaris] p. 89. |
Theorem | 19.12 1535 | Theorem 19.12 of [Margaris] p. 89. Assuming the converse is a mistake sometimes made by beginners! But sometimes the converse does hold, as in 19.12vv 1741. |
Theorem | 19.19 1536 | Theorem 19.19 of [Margaris] p. 90. |
Theorem | 19.36 1537 | Theorem 19.36 of [Margaris] p. 90. |
Theorem | 19.36i 1538 | Inference from Theorem 19.36 of [Margaris] p. 90. |
Theorem | 19.37 1539 | Theorem 19.37 of [Margaris] p. 90. |
Theorem | 19.38 1540 | Theorem 19.38 of [Margaris] p. 90. |
Theorem | 19.39 1541 | Theorem 19.39 of [Margaris] p. 90. |
Theorem | 19.24 1542 | Theorem 19.24 of [Margaris] p. 90. |
Theorem | 19.44 1543 | Theorem 19.44 of [Margaris] p. 90. |
Theorem | 19.45 1544 | Theorem 19.45 of [Margaris] p. 90. |
Theorem | 19.34 1545 | Theorem 19.34 of [Margaris] p. 90. |
Theorem | 19.41 1546 | Theorem 19.41 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | 19.42 1547 | Theorem 19.42 of [Margaris] p. 90. |
Theorem | excom13 1548 | Swap 1st and 3rd existential quantifiers. |
Theorem | exrot3 1549 | Rotate existential quantifiers. |
Theorem | exrot4 1550 | Rotate existential quantifiers twice. |
Theorem | nexr 1551 | Inference from 19.8a 1479. (Contributed by Jeff Hankins, 26-Jul-2009.) |
Theorem | exan 1552 | Place a conjunct in the scope of an existential quantifier. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | hbexd 1553 | Deduction form of bound-variable hypothesis builder hbex 1528. |
Theorem | eeor 1554 | Rearrange existential quantifiers. |
Theorem | qexmid 1555 | Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic. |
Theorem | a9e 1556 | 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 1396 and ax-17 1402, all axioms other than ax-9 1418 are believed to be theorems of free logic, although the system without ax-9 1418 is probably not complete in free logic. |
Theorem | ax9o 1557 |
Show that the original axiom ax-9o 1558 can be derived from ax-9 1418
and
others. See ax9 1559 for the rederivation of ax-9 1418
from ax-9o 1558.
Normally, ax9o 1557 should be used rather than ax-9o 1558, except by theorems specifically studying the latter's properties. |
Axiom | ax-9o 1558 |
A variant of ax-9 1418. Axiom scheme C10' in [Megill] p. 448 (p. 16 of the
preprint).
This axiom is redundant, as shown by theorem ax9o 1557. Normally, ax9o 1557 should be used rather than ax-9o 1558, except by theorems specifically studying the latter's properties. |
Theorem | ax9 1559 |
Rederivation of axiom ax-9 1418 from the orginal version, ax-9o 1558. See
ax9o 1557 for the derivation of ax-9o 1558 from ax-9 1418. Lemma L18 in [Megill]
p. 446 (p. 14 of the preprint).
This theorem should not be referenced in any proof. Instead, use ax-9 1418 above so that uses of ax-9 1418 can be more easily identified. |
Theorem | equidALT 1560 | Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. Alternate proof of equid 1562 from older axioms ax-6o 1428 and ax-9o 1558. |
Theorem | equid1 1561 | Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. This proof is similar to Tarski's and makes use of a dummy variable . See equid 1562 for a proof that avoids dummy variables (but is less intuitive). |
Theorem | equid 1562 | 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. (The proof has been modified to use equid1 1561 for compatibility with intuitionistic logic.) |
Theorem | stdpc6 1563 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1614.) 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). |
Theorem | equcomi 1564 | Commutative law for equality. Lemma 7 of [Tarski] p. 69. |
Theorem | equcom 1565 | Commutative law for equality. |
Theorem | equcoms 1566 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. |
Theorem | equtr 1567 | A transitive law for equality. |
Theorem | equtrr 1568 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). |
Theorem | equtr2 1569 | A transitive law for equality. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | equequ1 1570 | An equivalence law for equality. |
Theorem | equequ2 1571 | An equivalence law for equality. |
Theorem | elequ1 1572 | An identity law for the non-logical predicate. |
Theorem | elequ2 1573 | An identity law for the non-logical predicate. |
Theorem | ax11i 1574 | Inference that has ax-11 1389 (without ) as its conclusion and doesn't require ax-10 1388, ax-11 1389, or ax-12 1393 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. |
Theorem | ax10o 1575 |
Show that ax-10o 1576 can be derived from ax-10 1388. An open problem is
whether this theorem can be derived from ax-10 1388 and the others when
ax-11 1389 is replaced with ax-11o 1654. See theorem ax10 1577
for the
rederivation of ax-10 1388 from ax10o 1575.
Normally, ax10o 1575 should be used rather than ax-10o 1576, except by theorems specifically studying the latter's properties. |
Axiom | ax-10o 1576 |
Axiom ax-10o 1576 ("o" for "old") was the
original version of ax-10 1388,
before it was discovered (in May 2008) that the shorter ax-10 1388 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 1575. Normally, ax10o 1575 should be used rather than ax-10o 1576, except by theorems specifically studying the latter's properties. |
Theorem | ax10 1577 |
Rederivation of ax-10 1388 from original version ax-10o 1576. See theorem
ax10o 1575 for the derivation of ax-10o 1576 from ax-10 1388.
This theorem should not be referenced in any proof. Instead, use ax-10 1388 above so that uses of ax-10 1388 can be more easily identified. |
Theorem | hbae 1578 | All variables are effectively bound in an identical variable specifier. |
Theorem | hbaes 1579 | Rule that applies hbae 1578 to antecedent. |
Theorem | hbnae 1580 | All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint). |
Theorem | hbnaes 1581 | Rule that applies hbnae 1580 to antecedent. |
Theorem | equs4 1582 | Lemma used in proofs of substitution properties. (The proof was shortened by Mario Carneiro, 20-May-2014.) |
Theorem | equsal 1583 | A useful equivalence related to substitution. (The proof was shortened by Andrew Salmon, 12-Aug-2011.) |
Theorem | equsex 1584 | A useful equivalence related to substitution. |
Theorem | dvelimfALT 1585 | Proof of dvelimf 1688 that uses ax-10o 1576 (in the form of ax10o 1575) but not ax-11o 1654, ax-10 1388, or ax-11 1389 (if we replace uses of ax10o 1575 by ax-10o 1576 in the proofs of referenced theorems). See dvelimALT 1800 for a proof (of the distinct variable version dvelim 1799) that doesn't require ax-10 1388. It is not clear whether a proof is possible that uses ax-10 1388 but avoids ax-11 1389, ax-11o 1654, and ax-10o 1576. |
Theorem | dral1 1586 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). |
Theorem | dral2 1587 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). |
Theorem | drex1 1588 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). |
Theorem | drex2 1589 | Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint). |
Theorem | exdistrf 1590 | Distribution of existential quantifiers, with a bound-variable hypothesis saying that is not free in , but can be free in (and there is no distinct variable condition on and ). (Contributed by Mario Carneiro, 20-Mar-2013.) |
Theorem | a4imt 1591 | Closed theorem form of a4im 1592. |
Theorem | a4im 1592 | Specialization, using implicit substitition. Compare Lemma 14 of [Tarski] p. 70. The a4im 1592 series of theorems requires that only one direction of the substitution hypothesis hold. |
Theorem | a4ime 1593 | Existential introduction, using implicit substitition. Compare Lemma 14 of [Tarski] p. 70. |
Theorem | a4imed 1594 | Deduction version of a4ime 1593. |
Theorem | cbv1 1595 | Rule used to change bound variables, using implicit substitition. |
Theorem | cbv2 1596 | Rule used to change bound variables, using implicit substitition. |
Theorem | cbv3 1597 | Rule used to change bound variables, using implicit substitition, that does not use ax-12 1393. |
Theorem | cbv3ALT 1598 | Rule used to change bound variables, using implicit substitition. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | cbval 1599 | Rule used to change bound variables, using implicit substitition. (The proof was shortened by Andrew Salmon, 25-May-2011.) |
Theorem | cbvex 1600 | Rule used to change bound variables, using implicit substitition. (Revised by Mario Carneiro, 3-Feb-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |