HomeHome Intuitionistic Logic Explorer
Theorem List (p. 15 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 - 1401-1500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremnalequcoms 1401 A commutation rule for distinct variable specifiers. (Revised by Mario Carneiro, 2-Feb-2015.)
   =>   
 
1.4.3  Axiom ax-17 - first use of the $d distinct variable statement
 
Axiomax-17 1402* Axiom to quantify a variable over a formula in which it does not occur. Axiom C5 in [Megill] p. 444 (p. 11 of the preprint). Also appears as Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C5-1 of [Monk2] p. 113.

This axiom is logically redundant in the (logically complete) predicate calculus axiom system consisting of ax-gen 1339, ax-4 1392 through ax-9 1418, ax-10o 1576, and ax-12 1393 through ax-16 1644: in that system, we can derive any instance of ax-17 1402 not containing wff variables by induction on formula length, using ax17eq 1645 and ax17el 1808 for the basis together hbn 1438, hbal 1357, and hbim 1439. However, if we omit this axiom, our development would be quite inconvenient since we could work only with specific instances of wffs containing no wff variables - this axiom introduces the concept of a set variable not occurring in a wff (as opposed to just two set variables being distinct).

 
Theorema17d 1403* ax-17 1402 with antecedent.
 
1.4.4  Derive ax-9 from a weaker version
 
Theorema9wa9lem1 1404* Lemma for a9wa9 1415. Similar to equcomi 1564, without using ax-9 1418 or ax-4 1392.
   =>   
 
Theorema9wa9lem2 1405* Lemma for a9wa9 1415. Similar to equequ2 1571, without using ax-9 1418 or ax-4 1392.
   &       =>   
 
Theorema9wa9lem2OLD 1406* Obsolete proof of a9wa9lem2 1405 as of 3-Apr-2014.
   &       =>   
 
Theorema9wa9lem3 1407* Lemma for a9wa9 1415. Similar to ax4 1423, without using ax-9 1418 or ax-4 1392.
   &       =>   
 
Theorema9wa9lem4 1408* Lemma for a9wa9 1415. Similar to hba1 1436, without using ax-9 1418 or ax-4 1392.
   &       =>   
 
Theorema9wa9lem5 1409* Lemma for a9wa9 1415. Similar to hbn 1438, without using ax-9 1418 or ax-4 1392.
   &       &       =>   
 
Theorema9wa9lem6 1410* Lemma for a9wa9 1415. Similar to hbimd 1475, without using ax-9 1418 or ax-4 1392. (The proof was shortened by Wolf Lammen, 3-Apr-2014.)
   &       &       &       &       =>   
 
Theorema9wa9lem6OLD 1411* Obsolete proof of a9wa9lem6 1410 as of 3-Apr-2014.
   &       &       &       &       =>   
 
Theorema9wa9lem7 1412* Lemma for a9wa9 1415. Similar to hban 1441, without using ax-9 1418 or ax-4 1392.
   &       &       &       =>   
 
Theorema9wa9lem8 1413* Lemma for a9wa9 1415. Similar to dvelimfALT 1585, without using ax-9 1418 or ax-4 1392. (The proof was shortened by Wolf Lammen, 18-Jul-2014.)
   &       &       &       &       &       =>   
 
Theorema9wa9lem8OLD 1414* Obsolete proof of a9wa9lem8 1413 as of 18-Jul-2014.
   &       &       &       &       &       =>   
 
Theorema9wa9 1415* Derive ax-9 1418 (which has no distinct variable requirement) from a weaker version that requires that its two variables be distinct. The hypotheses are the instances of the weaker version that we need. Neither ax-9 1418 nor ax-4 1392 (which can be derived from ax-9 1418) is used by the proof. Note that every other predicate calculus axiom (except ax-13 1395 and ax-14 1396) is used by the proof. (The proof was shortened by Wolf Lammen, 28-Mar-2014.)
   &       &       &       &       &       &       &       =>   
 
Theorema9wa9OLD 1416* Obsolete proof of a9wa9 1415 as of 28-Mar-2014.
   &       &       &       &       &       &       &       =>   
 
1.4.5  Introduce Axiom of Existence ax-9
 
Axiomax-i9 1417 Axiom of Existence. One of the equality and substitution axioms of predicate calculus with equality. One thing this axiom tells us is that at least one thing exists (although ax-4 1392 and possibly others also tell us that, i.e. they are not valid in the empty domain of a "free logic"). In this form (not requiring that and be distinct) it was used in an axiom system of Tarski (see Axiom B7' in footnote 1 of [KalishMontague] p. 81.) It is equivalent to axiom scheme C10' in [Megill] p. 448 (p. 16 of the preprint); the equivalence is established by ax9o 1557 and ax9 1559. A more convenient form of this axiom is a9e 1556, which has additional remarks.

Raph Levien proved the independence of this axiom from the other logical axioms on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html.

ax-9 1418 can be proved from a weaker version requiring that the variables be distinct; see theorem a9wa9 1415.

 
Theoremax-9 1418 Derive ax-9 1418 from ax-i9 1417, the modified version for intuitionistic logic.
 
Theoremequidqe 1419 equid 1562 with existential quantifier without using ax-4 1392 or ax-17 1402. (The proof was shortened by Wolf Lammen, 27-Feb-2014.)
 
TheoremequidqeOLD 1420 Obsolete proof of equidqe 1419 as of 27-Feb-2014.
 
Theoremequidq 1421 equid 1562 with universal quantifier without using ax-4 1392 or ax-17 1402.
 
Theoremax4sp1 1422 A special case of ax-4 1392 without using ax-4 1392 or ax-17 1402.
 
1.4.6  Derive ax-4, ax-5o, and ax-6o
 
Theoremax4 1423 Theorem showing that ax-4 1392 can be derived from ax-5 1336, ax-gen 1339, ax-8 1387, ax-9 1418, ax-11 1389, and ax-17 1402 and is therefore redundant in a system including these axioms. The proof uses ideas from the proof of Lemma 21 of [Monk2] p. 114.

This theorem should not be referenced in any proof. Instead, we will use ax-4 1392 below so that explicit uses of ax-4 1392 can be more easily identified. In particular, this will more cleanly separate out the theorems of "pure" predicate calculus that don't involve equality or distinct variables. A beginner may wish to accept ax-4 1392 a priori, so that the proof of this theorem (ax4 1423), which involves equality as well as the distinct variable requirements of ax-17 1402, can be put off until those axioms are studied.

Note: All predicate calculus axioms introduced from this point forward are redundant. Immediately before their introduction, we prove them from earlier axioms to demonstrate their redundancy. Specifically, redundant axioms ax-4 1392, ax-5o 1425, ax-6o 1428, ax-9o 1558, ax-10o 1576, ax-11o 1654, ax-15 1807, and ax-16 1644 are proved by theorems ax4 1423, ax5o 1424, ax6o 1427, ax9o 1557, ax10o 1575, ax11o 1653, ax15 1806, and ax16 1643. Except for the ones suffixed with o (ax-5o 1425 etc.), we never reference those theorems directly. Instead, we use the axiom version that immediately follows it. This allow us to better isolate the uses of the redundant axioms for easier study of subsystems containing them.

(The proof was shortened by Scott Fenton, 24-Jan-2011.)

 
Theoremax5o 1424 Show that the original axiom ax-5o 1425 can be derived from ax-5 1336 and others. See ax5 1426 for the rederivation of ax-5 1336 from ax-5o 1425.

Part of the proof is based on the proof of Lemma 22 of [Monk2] p. 114.

Normally, ax5o 1424 should be used rather than ax-5o 1425, except by theorems specifically studying the latter's properties.

 
Axiomax-5o 1425 Axiom of Quantified Implication. This axiom moves a quantifier from outside to inside an implication, quantifying . Notice that must not be a free variable in the antecedent of the quantified implication, and we express this by binding to "protect" the axiom from a containing a free . One of the 4 axioms of "pure" predicate calculus. Axiom scheme C4' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Lemma 5 of [Monk2] p. 108 and Axiom 5 of [Mendelson] p. 69.

This axiom is redundant, as shown by theorem ax5o 1424.

Normally, ax5o 1424 should be used rather than ax-5o 1425, except by theorems specifically studying the latter's properties.

 
Theoremax5 1426 Rederivation of axiom ax-5 1336 from the orginal version, ax-5o 1425. See ax5o 1424 for the derivation of ax-5o 1425 from ax-5 1336.

This theorem should not be referenced in any proof. Instead, use ax-5 1336 above so that uses of ax-5 1336 can be more easily identified.

Note: This is the same as theorem alim 1347 below. It is proved separately here so that it won't be dependent on the axioms used for alim 1347.

 
Theoremax6o 1427 Show that the original axiom ax-6o 1428 can be derived from ax-6 1337 and others. See ax6 1429 for the rederivation of ax-6 1337 from ax-6o 1428.

Normally, ax6o 1427 should be used rather than ax-6o 1428, except by theorems specifically studying the latter's properties.

 
Axiomax-6o 1428 Axiom of Quantified Negation. This axiom is used to manipulate negated quantifiers. One of the 4 axioms of pure predicate calculus. Equivalent to axiom scheme C7' in [Megill] p. 448 (p. 16 of the preprint). An alternate axiomatization could use ax467 1455 in place of ax-4 1392, ax-6o 1428, and ax-7 1338.

This axiom is redundant, as shown by theorem ax6o 1427.

Normally, ax6o 1427 should be used rather than ax-6o 1428, except by theorems specifically studying the latter's properties.

 
Theoremax6 1429 Rederivation of axiom ax-6 1337 from the orginal version, ax-6o 1428. See ax6o 1427 for the derivation of ax-6o 1428 from ax-6 1337.

This theorem should not be referenced in any proof. Instead, use ax-6 1337 above so that uses of ax-6 1337 can be more easily identified.

 
Axiomax-ial 1430 is not free in . Axiom 7 of 10 for intuitionistic logic.
 
Axiomax-i5r 1431 The converse of ax-5o 1425. Axiom 8 of 10 for intuitionistic logic.
 
1.4.7  "Pure" predicate calculus including ax-4, without distinct variables
 
Theorema4i 1432 Inference rule reversing generalization.
   =>   
 
Theorema4s 1433 Generalization of antecedent.
   =>   
 
Theorema4sd 1434 Deduction generalizing antecedent.
   =>   
 
Theoremhbnt 1435 Closed theorem version of bound-variable hypothesis builder hbn 1438.
 
Theoremhba1 1436 is not free in . Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114.
 
Theorema5i 1437 Inference version of ax-5o 1425.
   =>   
 
Theoremhbn 1438 If is not free in , it is not free in .
   =>   
 
Theoremhbim 1439 If is not free in and , it is not free in . (The proof was shortened by O'Cat, 3-Mar-2008.) (Revised by Mario Carneiro, 2-Feb-2015.)
   &       =>   
 
Theoremhbor 1440 If is not free in and , it is not free in .
   &       =>   
 
Theoremhban 1441 If is not free in and , it is not free in . (The proof was shortened by Mario Carneiro, 2-Feb-2015.)
   &       =>   
 
Theoremhbbi 1442 If is not free in and , it is not free in .
   &       =>   
 
Theoremhb3or 1443 If is not free in , , and , it is not free in .
   &       &       =>   
 
Theoremhb3an 1444 If is not free in , , and , it is not free in .
   &       &       =>   
 
Theoremhba2 1445 Lemma 24 of [Monk2] p. 114.
 
Theoremhbia1 1446 Lemma 23 of [Monk2] p. 114.
 
Theoremhbn1OLD 1447 Obsolete proof of hbn1 1448 as of 15-Aug-2014.
 
Theoremhbn1 1448 is not free in . (The proof was shortened by Wolf Lammen, 18-Aug-2014.)
 
Theoremax46 1449 Proof of a single axiom that can replace ax-4 1392 and ax-6o 1428. See ax46to4 1450 and ax46to6 1451 for the re-derivation of those axioms. (Contributed by Scott Fenton, 12-Sep-2005.)
 
Theoremax46to4 1450 Re-derivation of ax-4 1392 from ax46 1449. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
 
Theoremax46to6 1451 Re-derivation of ax-6o 1428 from ax46 1449. Only propositional calculus is used for the re-derivation. (Contributed by Scott Fenton, 12-Sep-2005.)
 
Theoremax67 1452 Proof of a single axiom that can replace both ax-6o 1428 and ax-7 1338. See ax67to6 1453 and ax67to7 1454 for the re-derivation of those axioms.
 
Theoremax67to6 1453 Re-derivation of ax-6o 1428 from ax67 1452. Note that ax-6o 1428 and ax-7 1338 are not used by the re-derivation.
 
Theoremax67to7 1454 Re-derivation of ax-7 1338 from ax67 1452. Note that ax-6o 1428 and ax-7 1338 are not used by the re-derivation.
 
Theoremax467 1455 Proof of a single axiom that can replace ax-4 1392, ax-6o 1428, and ax-7 1338 in a subsystem that includes these axioms plus ax-5o 1425 and ax-gen 1339 (and propositional calculus). See ax467to4 1456, ax467to6 1457, and ax467to7 1458 for the re-derivation of those axioms. This theorem extends the idea in Scott Fenton's ax46 1449.
 
Theoremax467to4 1456 Re-derivation of ax-4 1392 from ax467 1455. Only propositional calculus is used by the re-derivation.
 
Theoremax467to6 1457 Re-derivation of ax-6o 1428 from ax467 1455. Note that ax-6o 1428 and ax-7 1338 are not used by the re-derivation. The use of alimi 1345 (which uses ax-4 1392) is allowed since we have already proved ax467to4 1456.
 
Theoremax467to7 1458 Re-derivation of ax-7 1338 from ax467 1455. Note that ax-6o 1428 and ax-7 1338 are not used by the re-derivation. The use of alimi 1345 (which uses ax-4 1392) is allowed since we have already proved ax467to4 1456.
 
Theoremmodal-5 1459 The analog in our "pure" predicate calculus of axiom 5 of modal logic S5.
 
Theoremmodal-b 1460 The analog in our "pure" predicate calculus of the Brouwer axiom (B) of modal logic S5.
 
Theorem19.3 1461 A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89.
   =>   
 
Theorem19.16 1462 Theorem 19.16 of [Margaris] p. 90.
   =>   
 
Theorem19.17 1463 Theorem 19.17 of [Margaris] p. 90.
   =>   
 
Theorem19.21 1464 Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ."
   =>   
 
Theorem19.21-2 1465 Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers.
   &       =>   
 
Theoremstdpc5 1466 An axiom scheme of standard predicate calculus that emulates Axiom 5 of [Mendelson] p. 69. The hypothesis can be thought of as emulating " is not free in ." With this convention, the meaning of "not free" is less restrictive than the usual textbook definition; for example would not (for us) be free in by hbequid 1397. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5.
   =>   
 
Theorem19.21bi 1467 Inference from Theorem 19.21 of [Margaris] p. 90.
   =>   
 
Theorem19.21bbi 1468 Inference removing double quantifier.
   =>   
 
Theorem19.27 1469 Theorem 19.27 of [Margaris] p. 90.
   =>   
 
Theorem19.28 1470 Theorem 19.28 of [Margaris] p. 90.
   =>   
 
Theorem19.32 1471 Theorem 19.32 of [Margaris] p. 90.
   =>   
 
Theorem19.31 1472 Theorem 19.31 of [Margaris] p. 90.
   =>   
 
Theoremhbim1 1473 A closed form of hbim 1439.
   &       =>   
 
Theoremhbnd 1474 Deduction form of bound-variable hypothesis builder hbn 1438.
   &       =>   
 
Theoremhbimd 1475 Deduction form of bound-variable hypothesis builder hbim 1439.
   &       &       =>   
 
Theoremhbbid 1476 Deduction form of bound-variable hypothesis builder hbbi 1442.
   &       &       =>   
 
Theorem19.21t 1477 Closed form of Theorem 19.21 of [Margaris] p. 90.
 
Theoremaaan 1478 Rearrange universal quantifiers.
   &       =>   
 
1.4.8  The existential quantifier
 
Theorem19.8a 1479 If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89.
 
Theorem19.23bi 1480 Inference from Theorem 19.23 of [Margaris] p. 90.
   =>   
 
Theoremexlimi 1481 Inference from Theorem 19.23 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)
   &       =>   
 
Theoremexlimd 1482 Deduction from Theorem 19.23 of [Margaris] p. 90.
   &       &       =>   
 
Theoremexim 1483 Theorem 19.22 of [Margaris] p. 90. (The proof was shortened by Wolf Lammen, 4-Jul-2014.)
 
TheoremeximOLD 1484 Obsolete proof of exim 1483 as of 4-Jul-2014.
 
Theoremeximi 1485 Inference adding existential quantifier to antecedent and consequent.
   =>   
 
Theorem2eximi 1486 Inference adding 2 existential quantifiers to antecedent and consequent.
   =>   
 
Theoremalinexa 1487 A transformation of quantifiers and logical connectives.
 
Theoremexbi 1488 Theorem 19.18 of [Margaris] p. 90.
 
Theoremexbii 1489 Inference adding existential quantifier to both sides of an equivalence.
   =>   
 
Theorem2exbii 1490 Inference adding 2 existential quantifiers to both sides of an equivalence.
   =>   
 
Theorem3exbii 1491 Inference adding 3 existential quantifiers to both sides of an equivalence.
   =>   
 
Theoremexancom 1492 Commutation of conjunction inside an existential quantifier.
 
Theoremeximd 1493 Deduction from Theorem 19.22 of [Margaris] p. 90.
   &       =>   
 
Theoremnex 1494 Generalization rule for negated wff.
   =>   
 
Theoremnexd 1495 Deduction for generalization rule for negated wff.
   &       =>   
 
Theoremexbid 1496 Formula-building rule for existential quantifier (deduction rule).
   &       =>   
 
Theoremexsimpl 1497 Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (The proof was shortened by Andrew Salmon, 29-Jun-2011.)
 
Theorem19.29 1498 Theorem 19.29 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)
 
Theorem19.29r 1499 Variation of Theorem 19.29 of [Margaris] p. 90.
 
Theorem19.29r2 1500 Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification.
    < 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 >