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

Browser slow? Try the
Unicode version. |

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

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

Statement | ||

Theorem | 19.21ht 1401 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |

Theorem | 19.21t 1402 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |

Theorem | nfimd 1403 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 30-Dec-2017.) |

Theorem | aaan 1404 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |

Theorem | nfbid 1405 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 29-Dec-2017.) |

Theorem | nfbi 1406 | If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |

1.3.7 The existential quantifier | ||

Theorem | 19.8a 1407 | If a wff is true, it is true for at least one instance. Special case of Theorem 19.8 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.23bi 1408 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | exlimi 1409 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |

Theorem | exlimd2 1410 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimd 1411 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |

Theorem | exlimd 1411 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |

Theorem | exlimiv 1412* |
Inference from Theorem 19.23 of [Margaris] p.
90.
This inference, along with our many variants is used to implement a
metatheorem called "Rule C" that is given in many logic
textbooks. See,
for example, Rule C in [Mendelson] p.
81, Rule C in [Margaris] p. 40, or
Rule C in Hirst and Hirst's In informal proofs, the statement "Let C be an element such that..." almost always means an implicit application of Rule C. In essence, Rule C states that if we can prove that some element exists satisfying a wff, i.e. where has free, then we can use C as a hypothesis for the proof where C is a new (ficticious) constant not appearing previously in the proof, nor in any axioms used, nor in the theorem to be proved. The purpose of Rule C is to get rid of the existential quantifier. We cannot do this in Metamath directly. Instead, we use the original (containing ) as an antecedent for the main part of the proof. We eventually arrive at where is the theorem to be proved and does not contain . Then we apply exlimiv 1412 to arrive at . Finally, we separately prove and detach it with modus ponens ax-mp 7 to arrive at the final theorem . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 25-Jul-2012.) |

Theorem | exim 1413 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |

Theorem | eximi 1414 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |

Theorem | 2eximi 1415 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |

Theorem | alinexa 1416 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |

Theorem | exbi 1417 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | exbii 1418 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |

Theorem | 2exbii 1419 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |

Theorem | 3exbii 1420 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |

Theorem | exancom 1421 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |

Theorem | eximd 1422 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |

Theorem | nexd 1423 | Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.) |

Theorem | exbid 1424 | Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.) |

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

Theorem | 19.29 1426 | Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |

Theorem | 19.29r 1427 | Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |

Theorem | 19.29r2 1428 | Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.) |

Theorem | 19.29x 1429 | Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.) |

Theorem | 19.35-1 1430 | Forward direction of Theorem 19.35 of [Margaris] p. 90. (Contributed by Mario Carneiro, 2-Feb-2015.) |

Theorem | 19.35i 1431 | Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |

Theorem | 19.25 1432 | Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |

Theorem | 19.43 1433 | Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |

Theorem | 19.33b2 1434 | The antecedent provides a condition implying the converse of 19.33 1304. Compare Theorem 19.33 of [Margaris] p. 90. This variation of 19.33bdc 1435 is intuitionistically valid without a decidability condition. (Contributed by Mario Carneiro, 2-Feb-2015.) |

Theorem | 19.33bdc 1435 | Converse of 19.33 1304 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 1434 (Contributed by Jim Kingdon, 23-Apr-2018.) |

DECID | ||

Theorem | 19.40 1436 | Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.40-2 1437 | 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 1438 | Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.) |

Theorem | exintr 1439 | Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.) |

Theorem | hbex 1440 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |

Theorem | nfex 1441 | 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 1442 | Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.) |

Theorem | 19.9ht 1443 | A closed version of one direction of 19.9 1445. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.9t 1444 | A closed version of 19.9 1445. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortended by Wolf Lammen, 30-Dec-2017.) |

Theorem | 19.9 1445 | 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 | ax6blem 1446 | If is not free in , it is not free in . This theorem doesn't use ax6b 1447 compared to hbnt 1449. (Contributed by GD, 27-Jan-2018.) |

Theorem | ax6b 1447 |
Quantified Negation. Axiom C5-2 of [Monk2] p.
113.
(Contributed by GD, 27-Jan-2018.) |

Theorem | hbn1 1448 | is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.) |

Theorem | hbnt 1449 | Closed theorem version of bound-variable hypothesis builder hbn 1450. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |

Theorem | hbn 1450 | If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) |

Theorem | hbnd 1451 | Deduction form of bound-variable hypothesis builder hbn 1450. (Contributed by NM, 3-Jan-2002.) |

Theorem | nfnd 1452 | If in a context is not free in , it is not free in . (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 28-Dec-2017.) |

Theorem | nfn 1453 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | nfdc 1454 | If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.) |

DECID | ||

Theorem | modal-5 1455 | The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.) |

Theorem | 19.9d 1456 | A deduction version of one direction of 19.9 1445. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |

Theorem | 19.9hd 1457 | A deduction version of one direction of 19.9 1445. This is an older variation of this theorem; new proofs should use 19.9d 1456. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |

Theorem | excomim 1458 | One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |

Theorem | excom 1459 | Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.12 1460 | 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 1461 | Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | nf2 1462 | An alternative definition of df-nf 1281, which does not involve nested quantifiers on the same variable. (Contributed by Mario Carneiro, 24-Sep-2016.) |

Theorem | nf3 1463 | An alternative definition of df-nf 1281. (Contributed by Mario Carneiro, 24-Sep-2016.) |

Theorem | 19.36i 1464 | Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |

Theorem | 19.38 1465 | Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.44 1466 | Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.45 1467 | Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.34 1468 | Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |

Theorem | 19.41 1469 | Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | 19.42 1470 | Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.) |

Theorem | excom13 1471 | Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.) |

Theorem | exrot3 1472 | Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.) |

Theorem | exrot4 1473 | Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.) |

Theorem | nexr 1474 | Inference from 19.8a 1407. (Contributed by Jeff Hankins, 26-Jul-2009.) |

Theorem | exan 1475 | 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 1476 | Deduction form of bound-variable hypothesis builder hbex 1440. (Contributed by NM, 2-Jan-2002.) |

Theorem | eeor 1477 | Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.) |

1.3.8 Equality theorems without distinct
variables | ||

Theorem | a9e 1478 | 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 1267 through ax-14 1338 and ax-17 1350, all axioms other than ax-9 1355 are believed to be theorems of free logic, although the system without ax-9 1355 is probably not complete in free logic. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |

Theorem | ax9o 1479 | An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |

Theorem | equid 1480 |
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 | stdpc6 1481 | One of the two equality axioms of standard predicate calculus, called reflexivity of equality. (The other one is stdpc7 1540.) 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 1482 | Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) |

Theorem | equcom 1483 | Commutative law for equality. (Contributed by NM, 20-Aug-1993.) |

Theorem | equcoms 1484 | An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.) |

Theorem | equtr 1485 | A transitive law for equality. (Contributed by NM, 23-Aug-1993.) |

Theorem | equtrr 1486 | A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.) |

Theorem | equtr2 1487 | A transitive law for equality. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.) |

Theorem | equequ1 1488 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |

Theorem | equequ2 1489 | An equivalence law for equality. (Contributed by NM, 5-Aug-1993.) |

Theorem | elequ1 1490 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |

Theorem | elequ2 1491 | An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.) |

Theorem | ax11i 1492 | Inference that has ax-11 1330 (without ) as its conclusion and doesn't require ax-10 1329, ax-11 1330, or ax-12 1335 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.) |

1.3.9 Axioms ax-10 and ax-11 | ||

Theorem | ax10o 1493 |
Show that ax-10o 1494 can be derived from ax-10 1329. An open problem is
whether this theorem can be derived from ax-10 1329 and the others when
ax-11 1330 is replaced with ax-11o 1590. See theorem ax10 1495
for the
rederivation of ax-10 1329 from ax10o 1493.
Normally, ax10o 1493 should be used rather than ax-10o 1494, except by theorems specifically studying the latter's properties. (Contributed by NM, 16-May-2008.) |

Axiom | ax-10o 1494 |
Axiom ax-10o 1494 ("o" for "old") was the
original version of ax-10 1329,
before it was discovered (in May 2008) that the shorter ax-10 1329 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 1493. Normally, ax10o 1493 should be used rather than ax-10o 1494, except by theorems specifically studying the latter's properties. (Contributed by NM, 5-Aug-1993.) |

Theorem | ax10 1495 |
Rederivation of ax-10 1329 from original version ax-10o 1494. See theorem
ax10o 1493 for the derivation of ax-10o 1494 from ax-10 1329.
This theorem should not be referenced in any proof. Instead, use ax-10 1329 above so that uses of ax-10 1329 can be more easily identified. (Contributed by NM, 16-May-2008.) |

Theorem | hbae 1496 | All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.) |

Theorem | nfae 1497 | All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.) |

Theorem | hbaes 1498 | Rule that applies hbae 1496 to antecedent. (Contributed by NM, 5-Aug-1993.) |

Theorem | hbnae 1499 | 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 1500 | 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 > |