HomeHome Intuitionistic Logic Explorer
Theorem List (p. 16 of 20)
< Previous  Next >
Browser slow? Try the
Unicode version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 1501-1600   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorem19.29x 1501 Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification.
 
Theoremalex 1502 Theorem 19.6 of [Margaris] p. 89.
 
Theorem2nalexn 1503 Part of theorem *11.5 in [WhiteheadRussell] p. 164. (Contributed by Andrew Salmon, 24-May-2011.)
 
Theoremexnal 1504 Theorem 19.14 of [Margaris] p. 90.
 
Theoremalexn 1505 A relationship between two quantifiers and negation.
 
Theorem2exnexn 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.)
 
Theorem2exnexnOLD 1507 Obsolete proof of 2exnexn 1506 as of 25-Sep-2014.
 
Theoremexanali 1508 A transformation of quantifiers and logical connectives. (The proof was shortened by Wolf Lammen, 4-Sep-2014.)
 
TheoremexanaliOLD 1509 Obsolete proof of exanali 1508 as of 4-Sep-2014.
 
Theorem19.35-1 1510 Forward direction of Theorem 19.35 of [Margaris] p. 90. (Contributed by Mario Carneiro, 2-Feb-2015.)
 
Theorem19.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.)
 
Theorem19.35OLD 1512 Obsolete proof of 19.35 1511 as of 27-Jun-2014.
 
Theorem19.35i 1513 Inference from Theorem 19.35 of [Margaris] p. 90.
   =>   
 
Theorem19.35ri 1514 Inference from Theorem 19.35 of [Margaris] p. 90.
   =>   
 
Theorem19.25 1515 Theorem 19.25 of [Margaris] p. 90.
 
Theorem19.30 1516 Theorem 19.30 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)
 
Theorem19.43 1517 Theorem 19.43 of [Margaris] p. 90. (The proof was shortened by Mario Carneiro, 2-Feb-2015.)
 
Theorem19.43OLD 1518 Obsolete proof of 19.43 1517 as of 27-Jun-2014.
 
Theorem19.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.)
 
Theorem19.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.)
 
Theorem19.33bOLD 1521 Obsolete proof of 19.33b 1520 as of 22-Mar-2014.
 
Theorem19.40 1522 Theorem 19.40 of [Margaris] p. 90.
 
Theorem19.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.)
 
Theoremexintrbi 1524 Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
 
Theoremexintr 1525 Introduce a conjunct in the scope of an existential quantifier.
 
Theoremequs3 1526 Lemma used in proofs of substitution properties.
 
Theorema6e 1527 Abbreviated version of ax-6o 1428.
 
Theoremhbex 1528 If is not free in , it is not free in .
   =>   
 
Theorem19.2 1529 Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.)
 
Theorem19.9t 1530 A closed version of one direction of 19.9 1531.
 
Theorem19.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.)
   =>   
 
Theorem19.9d 1532 A deduction version of one direction of 19.9 1531.
   &       =>   
 
Theoremexcomim 1533 One direction of Theorem 19.11 of [Margaris] p. 89.
 
Theoremexcom 1534 Theorem 19.11 of [Margaris] p. 89.
 
Theorem19.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.
 
Theorem19.19 1536 Theorem 19.19 of [Margaris] p. 90.
   =>   
 
Theorem19.36 1537 Theorem 19.36 of [Margaris] p. 90.
   =>   
 
Theorem19.36i 1538 Inference from Theorem 19.36 of [Margaris] p. 90.
   &       =>   
 
Theorem19.37 1539 Theorem 19.37 of [Margaris] p. 90.
   =>   
 
Theorem19.38 1540 Theorem 19.38 of [Margaris] p. 90.
 
Theorem19.39 1541 Theorem 19.39 of [Margaris] p. 90.
 
Theorem19.24 1542 Theorem 19.24 of [Margaris] p. 90.
 
Theorem19.44 1543 Theorem 19.44 of [Margaris] p. 90.
   =>   
 
Theorem19.45 1544 Theorem 19.45 of [Margaris] p. 90.
   =>   
 
Theorem19.34 1545 Theorem 19.34 of [Margaris] p. 90.
 
Theorem19.41 1546 Theorem 19.41 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 25-May-2011.)
   =>   
 
Theorem19.42 1547 Theorem 19.42 of [Margaris] p. 90.
   =>   
 
Theoremexcom13 1548 Swap 1st and 3rd existential quantifiers.
 
Theoremexrot3 1549 Rotate existential quantifiers.
 
Theoremexrot4 1550 Rotate existential quantifiers twice.
 
Theoremnexr 1551 Inference from 19.8a 1479. (Contributed by Jeff Hankins, 26-Jul-2009.)
   =>   
 
Theoremexan 1552 Place a conjunct in the scope of an existential quantifier. (The proof was shortened by Andrew Salmon, 25-May-2011.)
   =>   
 
Theoremhbexd 1553 Deduction form of bound-variable hypothesis builder hbex 1528.
   &       =>   
 
Theoremeeor 1554 Rearrange existential quantifiers.
   &       =>   
 
Theoremqexmid 1555 Quantified "excluded middle." Exercise 9.2a of Boolos, p. 111, Computability and Logic.
 
1.4.9  Equality theorems without distinct variables
 
Theorema9e 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.
 
Theoremax9o 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.

 
Axiomax-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.

 
Theoremax9 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.

 
TheoremequidALT 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.
 
Theoremequid1 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).
 
Theoremequid 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.)
 
Theoremstdpc6 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).
 
Theoremequcomi 1564 Commutative law for equality. Lemma 7 of [Tarski] p. 69.
 
Theoremequcom 1565 Commutative law for equality.
 
Theoremequcoms 1566 An inference commuting equality in antecedent. Used to eliminate the need for a syllogism.
   =>   
 
Theoremequtr 1567 A transitive law for equality.
 
Theoremequtrr 1568 A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint).
 
Theoremequtr2 1569 A transitive law for equality. (The proof was shortened by Andrew Salmon, 25-May-2011.)
 
Theoremequequ1 1570 An equivalence law for equality.
 
Theoremequequ2 1571 An equivalence law for equality.
 
Theoremelequ1 1572 An identity law for the non-logical predicate.
 
Theoremelequ2 1573 An identity law for the non-logical predicate.
 
Theoremax11i 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.
   &       =>   
 
1.4.10  Axioms ax-10 and ax-11
 
Theoremax10o 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.

 
Axiomax-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.

 
Theoremax10 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.

 
Theoremhbae 1578 All variables are effectively bound in an identical variable specifier.
 
Theoremhbaes 1579 Rule that applies hbae 1578 to antecedent.
   =>   
 
Theoremhbnae 1580 All variables are effectively bound in a distinct variable specifier. Lemma L19 in [Megill] p. 446 (p. 14 of the preprint).
 
Theoremhbnaes 1581 Rule that applies hbnae 1580 to antecedent.
   =>   
 
Theoremequs4 1582 Lemma used in proofs of substitution properties. (The proof was shortened by Mario Carneiro, 20-May-2014.)
 
Theoremequsal 1583 A useful equivalence related to substitution. (The proof was shortened by Andrew Salmon, 12-Aug-2011.)
   &       =>   
 
Theoremequsex 1584 A useful equivalence related to substitution.
   &       =>   
 
TheoremdvelimfALT 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.
   &       &       =>   
 
Theoremdral1 1586 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
   =>   
 
Theoremdral2 1587 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
   =>   
 
Theoremdrex1 1588 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
   =>   
 
Theoremdrex2 1589 Formula-building lemma for use with the Distinctor Reduction Theorem. Part of Theorem 9.4 of [Megill] p. 448 (p. 16 of preprint).
   =>   
 
Theoremexdistrf 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.)
   =>   
 
Theorema4imt 1591 Closed theorem form of a4im 1592.
 
Theorema4im 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.
   &       =>   
 
Theorema4ime 1593 Existential introduction, using implicit substitition. Compare Lemma 14 of [Tarski] p. 70.
   &       =>   
 
Theorema4imed 1594 Deduction version of a4ime 1593.
   &       &       =>   
 
Theoremcbv1 1595 Rule used to change bound variables, using implicit substitition.
   &       &       =>   
 
Theoremcbv2 1596 Rule used to change bound variables, using implicit substitition.
   &       &       =>   
 
Theoremcbv3 1597 Rule used to change bound variables, using implicit substitition, that does not use ax-12 1393.
   &       &       =>   
 
Theoremcbv3ALT 1598 Rule used to change bound variables, using implicit substitition. (The proof was shortened by Andrew Salmon, 25-May-2011.)
   &       &       =>   
 
Theoremcbval 1599 Rule used to change bound variables, using implicit substitition. (The proof was shortened by Andrew Salmon, 25-May-2011.)
   &       &       =>   
 
Theoremcbvex 1600 Rule used to change bound variables, using implicit substitition. (Revised by Mario Carneiro, 3-Feb-2015.)
   &       &       =>   
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-1914
  Copyright terms: Public domain < Previous  Next >