Home | Intuitionistic Logic Explorer Theorem List (p. 15 of 94) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Axiom | ax-13 1401 | Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the left-hand side of the binary predicate. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. "Non-logical" means that the predicate is not a primitive of predicate calculus proper but instead is an extension to it. "Binary" means that the predicate has two arguments. In a system of predicate calculus with equality, like ours, equality is not usually considered to be a non-logical predicate. In systems of predicate calculus without equality, it typically would be. (Contributed by NM, 5-Aug-1993.) |
Axiom | ax-14 1402 | Axiom of Equality. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. It substitutes equal variables into the right-hand side of the binary predicate. Axiom scheme C13' in [Megill] p. 448 (p. 16 of the preprint). It is a special case of Axiom B8 (p. 75) of system S2 of [Tarski] p. 77. (Contributed by NM, 5-Aug-1993.) |
Theorem | hbequid 1403 | Bound-variable hypothesis builder for . This theorem tells us that any variable, including , is effectively not free in , even though is technically free according to the traditional definition of free variable. (The proof uses only ax-5 1333, ax-8 1392, ax-12 1399, and ax-gen 1335. This shows that this can be proved without ax-9 1421, even though the theorem equid 1586 cannot be. A shorter proof using ax-9 1421 is obtainable from equid 1586 and hbth 1349.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) |
Theorem | axi12 1404 | Proof that ax-i12 1395 follows from ax-bnd 1396. So that we can track which theorems rely on ax-bnd 1396, proofs should reference ax-i12 1395 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.) |
Theorem | alequcom 1405 | Commutation law for identical variable specifiers. The antecedent and consequent are true when and are substituted with the same variable. Lemma L12 in [Megill] p. 445 (p. 12 of the preprint). (Contributed by NM, 5-Aug-1993.) |
Theorem | alequcoms 1406 | A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.) |
Theorem | nalequcoms 1407 | A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 2-Feb-2015.) |
Theorem | nfr 1408 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) |
Theorem | nfri 1409 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfrd 1410 | Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | alimd 1411 | Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimi 1412 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfd 1413 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfdh 1414 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfrimi 1415 | Moving an antecedent outside . (Contributed by Jim Kingdon, 23-Mar-2018.) |
Axiom | ax-17 1416* |
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.
(Contributed by NM, 5-Aug-1993.) |
Theorem | a17d 1417* | ax-17 1416 with antecedent. (Contributed by NM, 1-Mar-2013.) |
Theorem | nfv 1418* | If is not present in , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfvd 1419* | nfv 1418 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1474. (Contributed by Mario Carneiro, 6-Oct-2016.) |
Axiom | ax-i9 1420 | 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 1397 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.) Another name for this theorem is a9e 1583, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | ax-9 1421 | Derive ax-9 1421 from ax-i9 1420, the modified version for intuitionistic logic. Although ax-9 1421 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1420. (Contributed by NM, 3-Feb-2015.) |
Theorem | equidqe 1422 | equid 1586 with some quantification and negation without using ax-4 1397 or ax-17 1416. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) |
Theorem | ax4sp1 1423 | A special case of ax-4 1397 without using ax-4 1397 or ax-17 1416. (Contributed by NM, 13-Jan-2011.) |
Axiom | ax-ial 1424 | is not free in . Axiom 7 of 10 for intuitionistic logic. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Axiom | ax-i5r 1425 | Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | spi 1426 | Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.) |
Theorem | sps 1427 | Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | spsd 1428 | Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.) |
Theorem | nfbidf 1429 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) |
Theorem | hba1 1430 | is not free in . Example in Appendix in [Megill] p. 450 (p. 19 of the preprint). Also Lemma 22 of [Monk2] p. 114. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfa1 1431 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | a5i 1432 | Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfnf1 1433 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbim 1434 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by O'Cat, 3-Mar-2008.) (Revised by Mario Carneiro, 2-Feb-2015.) |
Theorem | hbor 1435 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.) |
Theorem | hban 1436 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.) |
Theorem | hbbi 1437 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hb3or 1438 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hb3an 1439 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hba2 1440 | Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | hbia1 1441 | Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | 19.3h 1442 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 21-May-2007.) |
Theorem | 19.3 1443 | A wff may be quantified with a variable not free in it. Theorem 19.3 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.16 1444 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.17 1445 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21h 1446 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." New proofs should use 19.21 1472 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | 19.21bi 1447 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.21bbi 1448 | Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.) |
Theorem | 19.27h 1449 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.27 1450 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28h 1451 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28 1452 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfan1 1453 | A closed form of nfan 1454. (Contributed by Mario Carneiro, 3-Oct-2016.) |
Theorem | nfan 1454 | If is not free in and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) (Proof shortened by Wolf Lammen, 13-Jan-2018.) |
Theorem | nf3an 1455 | If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nford 1456 | If in a context is not free in and , it is not free in . (Contributed by Jim Kingdon, 29-Oct-2019.) |
Theorem | nfand 1457 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nf3and 1458 | Deduction form of bound-variable hypothesis builder nf3an 1455. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
Theorem | hbim1 1459 | A closed form of hbim 1434. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfim1 1460 | A closed form of nfim 1461. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | nfim 1461 | 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.) |
Theorem | hbimd 1462 | Deduction form of bound-variable hypothesis builder hbim 1434. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfor 1463 | If is not free in and , it is not free in . (Contributed by Jim Kingdon, 11-Mar-2018.) |
Theorem | hbbid 1464 | Deduction form of bound-variable hypothesis builder hbbi 1437. (Contributed by NM, 1-Jan-2002.) |
Theorem | nfal 1465 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfnf 1466 | 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 | nfalt 1467 | Closed form of nfal 1465. (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | nfa2 1468 | Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfia1 1469 | Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.21ht 1470 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.) |
Theorem | 19.21t 1471 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |
Theorem | 19.21 1472 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) |
Theorem | stdpc5 1473 | 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 definition, the meaning of "not free" is less restrictive than the usual textbook definition; for example would not (for us) be free in by nfequid 1587. This theorem scheme can be proved as a metatheorem of Mendelson's axiom system, even though it is slightly stronger than his Axiom 5. (Contributed by NM, 22-Sep-1993.) (Revised by Mario Carneiro, 12-Oct-2016.) (Proof shortened by Wolf Lammen, 1-Jan-2018.) |
Theorem | nfimd 1474 | 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 | aaanh 1475 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | aaan 1476 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | nfbid 1477 | 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 1478 | 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.) |
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. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.23bi 1480 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exlimih 1481 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.) |
Theorem | exlimi 1482 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exlimd2 1483 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1484 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |
Theorem | exlimdh 1484 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
Theorem | exlimd 1485 | Deduction from Theorem 19.9 of [Margaris] p. 89. (Contributed by Mario Carneiro, 24-Sep-2016.) (Proof rewritten by Jim Kingdon, 18-Jun-2018.) |
Theorem | exlimiv 1486* |
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 A Primer for Logic and Proof p. 59 (PDF p. 65) at http://www.mathsci.appstate.edu/~jlh/primer/hirst.pdf. 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 1486 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 1487 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Theorem | eximi 1488 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2eximi 1489 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Theorem | eximii 1490 | Inference associated with eximi 1488. (Contributed by BJ, 3-Feb-2018.) |
Theorem | alinexa 1491 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
Theorem | exbi 1492 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exbii 1493 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Theorem | 2exbii 1494 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Theorem | 3exbii 1495 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Theorem | exancom 1496 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
Theorem | alrimdd 1497 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimd 1498 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | eximdh 1499 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.) |
Theorem | eximd 1500 | Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |