Home | Intuitionistic Logic Explorer Theorem List (p. 15 of 102) | < 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 | ||
Theorem | sp 1401 | Specialization. Another name for ax-4 1400. (Contributed by NM, 21-May-2008.) |
Theorem | ax-12 1402 | Rederive the original version of the axiom from ax-i12 1398. (Contributed by Mario Carneiro, 3-Feb-2015.) |
Theorem | ax12or 1403 | Another name for ax-i12 1398. (Contributed by NM, 3-Feb-2015.) |
Axiom | ax-13 1404 | 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 1405 | 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 1406 | 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 1336, ax-8 1395, ax-12 1402, and ax-gen 1338. This shows that this can be proved without ax-9 1424, even though the theorem equid 1589 cannot be. A shorter proof using ax-9 1424 is obtainable from equid 1589 and hbth 1352.) (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 23-Mar-2014.) |
Theorem | axi12 1407 | Proof that ax-i12 1398 follows from ax-bndl 1399. So that we can track which theorems rely on ax-bndl 1399, proofs should reference ax-i12 1398 rather than this theorem. (Contributed by Jim Kingdon, 17-Aug-2018.) (New usage is discouraged). (Proof modification is discouraged.) |
Theorem | alequcom 1408 | 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 1409 | A commutation rule for identical variable specifiers. (Contributed by NM, 5-Aug-1993.) |
Theorem | nalequcoms 1410 | A commutation rule for distinct variable specifiers. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 2-Feb-2015.) |
Theorem | nfr 1411 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 26-Sep-2016.) |
Theorem | nfri 1412 | Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfrd 1413 | Consequence of the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | alimd 1414 | Deduction from Theorem 19.20 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | alrimi 1415 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfd 1416 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfdh 1417 | Deduce that is not free in in a context. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfrimi 1418 | Moving an antecedent outside . (Contributed by Jim Kingdon, 23-Mar-2018.) |
Axiom | ax-17 1419* |
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 1420* | ax-17 1419 with antecedent. (Contributed by NM, 1-Mar-2013.) |
Theorem | nfv 1421* | If is not present in , then is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfvd 1422* | nfv 1421 with antecedent. Useful in proofs of deduction versions of bound-variable hypothesis builders such as nfimd 1477. (Contributed by Mario Carneiro, 6-Oct-2016.) |
Axiom | ax-i9 1423 | 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 1400 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 1586, which has additional remarks. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | ax-9 1424 | Derive ax-9 1424 from ax-i9 1423, the modified version for intuitionistic logic. Although ax-9 1424 does hold intuistionistically, in intuitionistic logic it is weaker than ax-i9 1423. (Contributed by NM, 3-Feb-2015.) |
Theorem | equidqe 1425 | equid 1589 with some quantification and negation without using ax-4 1400 or ax-17 1419. (Contributed by NM, 13-Jan-2011.) (Proof shortened by Wolf Lammen, 27-Feb-2014.) |
Theorem | ax4sp1 1426 | A special case of ax-4 1400 without using ax-4 1400 or ax-17 1419. (Contributed by NM, 13-Jan-2011.) |
Axiom | ax-ial 1427 | is not free in . One of the axioms of predicate logic. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Axiom | ax-i5r 1428 | Axiom of quantifier collection. (Contributed by Mario Carneiro, 31-Jan-2015.) |
Theorem | spi 1429 | Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.) |
Theorem | sps 1430 | Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) |
Theorem | spsd 1431 | Deduction generalizing antecedent. (Contributed by NM, 17-Aug-1994.) |
Theorem | nfbidf 1432 | An equality theorem for effectively not free. (Contributed by Mario Carneiro, 4-Oct-2016.) |
Theorem | hba1 1433 | 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 1434 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | a5i 1435 | Inference generalizing a consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfnf1 1436 | is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | hbim 1437 | 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 1438 | 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 1439 | 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 1440 | If is not free in and , it is not free in . (Contributed by NM, 5-Aug-1993.) |
Theorem | hb3or 1441 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hb3an 1442 | If is not free in , , and , it is not free in . (Contributed by NM, 14-Sep-2003.) |
Theorem | hba2 1443 | Lemma 24 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | hbia1 1444 | Lemma 23 of [Monk2] p. 114. (Contributed by NM, 29-May-2008.) |
Theorem | 19.3h 1445 | 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 1446 | 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 1447 | Theorem 19.16 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.17 1448 | Theorem 19.17 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.) |
Theorem | 19.21h 1449 | Theorem 19.21 of [Margaris] p. 90. The hypothesis can be thought of as " is not free in ." New proofs should use 19.21 1475 instead. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.) |
Theorem | 19.21bi 1450 | Inference from Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.21bbi 1451 | Inference removing double quantifier. (Contributed by NM, 20-Apr-1994.) |
Theorem | 19.27h 1452 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.27 1453 | Theorem 19.27 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28h 1454 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | 19.28 1455 | Theorem 19.28 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfan1 1456 | A closed form of nfan 1457. (Contributed by Mario Carneiro, 3-Oct-2016.) |
Theorem | nfan 1457 | 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 1458 | If is not free in , , and , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nford 1459 | If in a context is not free in and , it is not free in . (Contributed by Jim Kingdon, 29-Oct-2019.) |
Theorem | nfand 1460 | If in a context is not free in and , it is not free in . (Contributed by Mario Carneiro, 7-Oct-2016.) |
Theorem | nf3and 1461 | Deduction form of bound-variable hypothesis builder nf3an 1458. (Contributed by NM, 17-Feb-2013.) (Revised by Mario Carneiro, 16-Oct-2016.) |
Theorem | hbim1 1462 | A closed form of hbim 1437. (Contributed by NM, 5-Aug-1993.) |
Theorem | nfim1 1463 | A closed form of nfim 1464. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 24-Sep-2016.) (Proof shortened by Wolf Lammen, 2-Jan-2018.) |
Theorem | nfim 1464 | 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 1465 | Deduction form of bound-variable hypothesis builder hbim 1437. (Contributed by NM, 1-Jan-2002.) (Revised by NM, 2-Feb-2015.) |
Theorem | nfor 1466 | If is not free in and , it is not free in . (Contributed by Jim Kingdon, 11-Mar-2018.) |
Theorem | hbbid 1467 | Deduction form of bound-variable hypothesis builder hbbi 1440. (Contributed by NM, 1-Jan-2002.) |
Theorem | nfal 1468 | If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.) |
Theorem | nfnf 1469 | 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 1470 | Closed form of nfal 1468. (Contributed by Jim Kingdon, 11-May-2018.) |
Theorem | nfa2 1471 | Lemma 24 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | nfia1 1472 | Lemma 23 of [Monk2] p. 114. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | 19.21ht 1473 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) (New usage is discouraged.) |
Theorem | 19.21t 1474 | Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.) |
Theorem | 19.21 1475 | 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 1476 | 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 1590. 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 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, 30-Dec-2017.) |
Theorem | aaanh 1478 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | aaan 1479 | Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.) |
Theorem | nfbid 1480 | 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 1481 | 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 1482 | 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 1483 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exlimih 1484 | 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 1485 | Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
Theorem | exlimd2 1486 | Deduction from Theorem 19.23 of [Margaris] p. 90. Similar to exlimdh 1487 but with one slightly different hypothesis. (Contributed by Jim Kingdon, 30-Dec-2017.) |
Theorem | exlimdh 1487 | Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.) |
Theorem | exlimd 1488 | 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 1489* |
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 1489 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 1490 | Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.) |
Theorem | eximi 1491 | Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.) |
Theorem | 2eximi 1492 | Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.) |
Theorem | eximii 1493 | Inference associated with eximi 1491. (Contributed by BJ, 3-Feb-2018.) |
Theorem | alinexa 1494 | A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.) |
Theorem | exbi 1495 | Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) |
Theorem | exbii 1496 | Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.) |
Theorem | 2exbii 1497 | Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.) |
Theorem | 3exbii 1498 | Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.) |
Theorem | exancom 1499 | Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.) |
Theorem | alrimdd 1500 | Deduction from Theorem 19.21 of [Margaris] p. 90. (Contributed by Mario Carneiro, 24-Sep-2016.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |