Home | Intuitionistic Logic ExplorerTheorem List (p. 15 of 20)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | nalequcoms 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 | ||

Axiom | ax-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 |

Theorem | a17d 1403* | ax-17 1402 with antecedent. |

1.4.4 Derive ax-9 from a weaker
version | ||

Theorem | a9wa9lem1 1404* | Lemma for a9wa9 1415. Similar to equcomi 1564, without using ax-9 1418 or ax-4 1392. |

Theorem | a9wa9lem2 1405* | Lemma for a9wa9 1415. Similar to equequ2 1571, without using ax-9 1418 or ax-4 1392. |

Theorem | a9wa9lem2OLD 1406* | Obsolete proof of a9wa9lem2 1405 as of 3-Apr-2014. |

Theorem | a9wa9lem3 1407* | Lemma for a9wa9 1415. Similar to ax4 1423, without using ax-9 1418 or ax-4 1392. |

Theorem | a9wa9lem4 1408* | Lemma for a9wa9 1415. Similar to hba1 1436, without using ax-9 1418 or ax-4 1392. |

Theorem | a9wa9lem5 1409* | Lemma for a9wa9 1415. Similar to hbn 1438, without using ax-9 1418 or ax-4 1392. |

Theorem | a9wa9lem6 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.) |

Theorem | a9wa9lem6OLD 1411* | Obsolete proof of a9wa9lem6 1410 as of 3-Apr-2014. |

Theorem | a9wa9lem7 1412* | Lemma for a9wa9 1415. Similar to hban 1441, without using ax-9 1418 or ax-4 1392. |

Theorem | a9wa9lem8 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.) |

Theorem | a9wa9lem8OLD 1414* | Obsolete proof of a9wa9lem8 1413 as of 18-Jul-2014. |

Theorem | a9wa9 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.) |

Theorem | a9wa9OLD 1416* | Obsolete proof of a9wa9 1415 as of 28-Mar-2014. |

1.4.5 Introduce Axiom of Existence
ax-9 | ||

Axiom | ax-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. |

Theorem | ax-9 1418 | Derive ax-9 1418 from ax-i9 1417, the modified version for intuitionistic logic. |

Theorem | equidqe 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.) |

Theorem | equidqeOLD 1420 | Obsolete proof of equidqe 1419 as of 27-Feb-2014. |

Theorem | equidq 1421 | equid 1562 with universal quantifier without using ax-4 1392 or ax-17 1402. |

Theorem | ax4sp1 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 | ||

Theorem | ax4 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.) |

Theorem | ax5o 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. |

Axiom | ax-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. |

Theorem | ax5 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. |

Theorem | ax6o 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. |

Axiom | ax-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. |

Theorem | ax6 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. |

Axiom | ax-ial 1430 | is not free in . Axiom 7 of 10 for intuitionistic logic. |

Axiom | ax-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 | ||

Theorem | a4i 1432 | Inference rule reversing generalization. |

Theorem | a4s 1433 | Generalization of antecedent. |

Theorem | a4sd 1434 | Deduction generalizing antecedent. |

Theorem | hbnt 1435 | Closed theorem version of bound-variable hypothesis builder hbn 1438. |

Theorem | hba1 1436 | is not free in . Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. |

Theorem | a5i 1437 | Inference version of ax-5o 1425. |

Theorem | hbn 1438 | If is not free in , it is not free in . |

Theorem | hbim 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.) |

Theorem | hbor 1440 | If is not free in and , it is not free in . |

Theorem | hban 1441 | If is not free in and , it is not free in . (The proof was shortened by Mario Carneiro, 2-Feb-2015.) |

Theorem | hbbi 1442 | If is not free in and , it is not free in . |

Theorem | hb3or 1443 | If is not free in , , and , it is not free in . |

Theorem | hb3an 1444 | If is not free in , , and , it is not free in . |

Theorem | hba2 1445 | Lemma 24 of [Monk2] p. 114. |

Theorem | hbia1 1446 | Lemma 23 of [Monk2] p. 114. |

Theorem | hbn1OLD 1447 | Obsolete proof of hbn1 1448 as of 15-Aug-2014. |

Theorem | hbn1 1448 | is not free in . (The proof was shortened by Wolf Lammen, 18-Aug-2014.) |

Theorem | ax46 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.) |

Theorem | ax46to4 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.) |

Theorem | ax46to6 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.) |

Theorem | ax67 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. |

Theorem | ax67to6 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. |

Theorem | ax67to7 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. |

Theorem | ax467 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. |

Theorem | ax467to4 1456 | Re-derivation of ax-4 1392 from ax467 1455. Only propositional calculus is used by the re-derivation. |

Theorem | ax467to6 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. |

Theorem | ax467to7 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. |

Theorem | modal-5 1459 | The analog in our "pure" predicate calculus of axiom 5 of modal logic S5. |

Theorem | modal-b 1460 | The analog in our "pure" predicate calculus of the Brouwer axiom (B) of modal logic S5. |

Theorem | 19.3 1461 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. |

Theorem | 19.16 1462 | Theorem 19.16 of [Margaris] p. 90. |

Theorem | 19.17 1463 | Theorem 19.17 of [Margaris] p. 90. |

Theorem | 19.21 1464 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." |

Theorem | 19.21-2 1465 | Theorem 19.21 of [Margaris] p. 90 but with 2 quantifiers. |

Theorem | stdpc5 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. |

Theorem | 19.21bi 1467 | Inference from Theorem 19.21 of [Margaris] p. 90. |

Theorem | 19.21bbi 1468 | Inference removing double quantifier. |

Theorem | 19.27 1469 | Theorem 19.27 of [Margaris] p. 90. |

Theorem | 19.28 1470 | Theorem 19.28 of [Margaris] p. 90. |

Theorem | 19.32 1471 | Theorem 19.32 of [Margaris] p. 90. |

Theorem | 19.31 1472 | Theorem 19.31 of [Margaris] p. 90. |

Theorem | hbim1 1473 | A closed form of hbim 1439. |

Theorem | hbnd 1474 | Deduction form of bound-variable hypothesis builder hbn 1438. |

Theorem | hbimd 1475 | Deduction form of bound-variable hypothesis builder hbim 1439. |

Theorem | hbbid 1476 | Deduction form of bound-variable hypothesis builder hbbi 1442. |

Theorem | 19.21t 1477 | Closed form of Theorem 19.21 of [Margaris] p. 90. |

Theorem | aaan 1478 | Rearrange universal quantifiers. |

1.4.8 The existential quantifier | ||

Theorem | 19.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. |

Theorem | 19.23bi 1480 | Inference from Theorem 19.23 of [Margaris] p. 90. |

Theorem | exlimi 1481 | Inference from Theorem 19.23 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.) |

Theorem | exlimd 1482 | Deduction from Theorem 19.23 of [Margaris] p. 90. |

Theorem | exim 1483 | Theorem 19.22 of [Margaris] p. 90. (The proof was shortened by Wolf Lammen, 4-Jul-2014.) |

Theorem | eximOLD 1484 | Obsolete proof of exim 1483 as of 4-Jul-2014. |

Theorem | eximi 1485 | Inference adding existential quantifier to antecedent and consequent. |

Theorem | 2eximi 1486 | Inference adding 2 existential quantifiers to antecedent and consequent. |

Theorem | alinexa 1487 | A transformation of quantifiers and logical connectives. |

Theorem | exbi 1488 | Theorem 19.18 of [Margaris] p. 90. |

Theorem | exbii 1489 | Inference adding existential quantifier to both sides of an equivalence. |

Theorem | 2exbii 1490 | Inference adding 2 existential quantifiers to both sides of an equivalence. |

Theorem | 3exbii 1491 | Inference adding 3 existential quantifiers to both sides of an equivalence. |

Theorem | exancom 1492 | Commutation of conjunction inside an existential quantifier. |

Theorem | eximd 1493 | Deduction from Theorem 19.22 of [Margaris] p. 90. |

Theorem | nex 1494 | Generalization rule for negated wff. |

Theorem | nexd 1495 | Deduction for generalization rule for negated wff. |

Theorem | exbid 1496 | Formula-building rule for existential quantifier (deduction rule). |

Theorem | exsimpl 1497 | Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (The proof was shortened by Andrew Salmon, 29-Jun-2011.) |

Theorem | 19.29 1498 | Theorem 19.29 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.) |

Theorem | 19.29r 1499 | Variation of Theorem 19.29 of [Margaris] p. 90. |

Theorem | 19.29r2 1500 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |