HomeHome Intuitionistic Logic Explorer
Theorem List (p. 15 of 22)
< 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
 
Theorem19.21ht 1401 Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
 
Theorem19.21t 1402 Closed form of Theorem 19.21 of [Margaris] p. 90. (Contributed by NM, 27-May-1997.)
 F/
 
Theoremnfimd 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.)
 F/   &     F/   =>     F/
 
Theoremaaan 1404 Rearrange universal quantifiers. (Contributed by NM, 12-Aug-1993.)
   &       =>   
 
Theoremnfbid 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.)
 F/   &     F/   =>     F/
 
Theoremnfbi 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.)

 F/   &     F/   =>     F/
 
1.3.7  The existential quantifier
 
Theorem19.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.)
 
Theorem19.23bi 1408 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremexlimi 1409 Inference from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
   &       =>   
 
Theoremexlimd2 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.)
   &       &       =>   
 
Theoremexlimd 1411 Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 28-Jan-1997.)
   &       &       =>   
 
Theoremexlimiv 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 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 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.)

   =>   
 
Theoremexim 1413 Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 4-Jul-2014.)
 
Theoremeximi 1414 Inference adding existential quantifier to antecedent and consequent. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theorem2eximi 1415 Inference adding 2 existential quantifiers to antecedent and consequent. (Contributed by NM, 3-Feb-2005.)
   =>   
 
Theoremalinexa 1416 A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993.)
 
Theoremexbi 1417 Theorem 19.18 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theoremexbii 1418 Inference adding existential quantifier to both sides of an equivalence. (Contributed by NM, 24-May-1994.)
   =>   
 
Theorem2exbii 1419 Inference adding 2 existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)
   =>   
 
Theorem3exbii 1420 Inference adding 3 existential quantifiers to both sides of an equivalence. (Contributed by NM, 2-May-1995.)
   =>   
 
Theoremexancom 1421 Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
 
Theoremeximd 1422 Deduction from Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 20-May-1996.)
   &       =>   
 
Theoremnexd 1423 Deduction for generalization rule for negated wff. (Contributed by NM, 2-Jan-2002.)
   &       =>   
 
Theoremexbid 1424 Formula-building rule for existential quantifier (deduction rule). (Contributed by NM, 5-Aug-1993.)
   &       =>   
 
Theoremexsimpl 1425 Simplification of an existentially quantified conjunction. (Contributed by Rodolfo Medina, 25-Sep-2010.) (Proof shortened by Andrew Salmon, 29-Jun-2011.)
 
Theorem19.29 1426 Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)
 
Theorem19.29r 1427 Variation of Theorem 19.29 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
 
Theorem19.29r2 1428 Variation of Theorem 19.29 of [Margaris] p. 90 with double quantification. (Contributed by NM, 3-Feb-2005.)
 
Theorem19.29x 1429 Variation of Theorem 19.29 of [Margaris] p. 90 with mixed quantification. (Contributed by NM, 11-Feb-2005.)
 
Theorem19.35-1 1430 Forward direction of Theorem 19.35 of [Margaris] p. 90. (Contributed by Mario Carneiro, 2-Feb-2015.)
 
Theorem19.35i 1431 Inference from Theorem 19.35 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
   =>   
 
Theorem19.25 1432 Theorem 19.25 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
 
Theorem19.43 1433 Theorem 19.43 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Mario Carneiro, 2-Feb-2015.)
 
Theorem19.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.)
 
Theorem19.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
 
Theorem19.40 1436 Theorem 19.40 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.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.)
 
Theoremexintrbi 1438 Add/remove a conjunct in the scope of an existential quantifier. (Contributed by Raph Levien, 3-Jul-2006.)
 
Theoremexintr 1439 Introduce a conjunct in the scope of an existential quantifier. (Contributed by NM, 11-Aug-1993.)
 
Theoremhbex 1440 If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
   =>   
 
Theoremnfex 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.)

 F/   =>    
 F/
 
Theorem19.2 1442 Theorem 19.2 of [Margaris] p. 89, generalized to use two set variables. (Contributed by O'Cat, 31-Mar-2008.)
 
Theorem19.9ht 1443 A closed version of one direction of 19.9 1445. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.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.)
 F/
 
Theorem19.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.)
   =>   
 
Theoremax6blem 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.)
   =>   
 
Theoremax6b 1447 Quantified Negation. Axiom C5-2 of [Monk2] p. 113.

(Contributed by GD, 27-Jan-2018.)

 
Theoremhbn1 1448 is not free in . (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 18-Aug-2014.)
 
Theoremhbnt 1449 Closed theorem version of bound-variable hypothesis builder hbn 1450. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
 
Theoremhbn 1450 If is not free in , it is not free in . (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremhbnd 1451 Deduction form of bound-variable hypothesis builder hbn 1450. (Contributed by NM, 3-Jan-2002.)
   &       =>   
 
Theoremnfnd 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.)
 F/   =>     F/
 
Theoremnfn 1453 If is not free in , it is not free in . (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/   =>    
 F/
 
Theoremnfdc 1454 If is not free in , it is not free in DECID . (Contributed by Jim Kingdon, 11-Mar-2018.)

 F/   =>    
 F/DECID
 
Theoremmodal-5 1455 The analog in our predicate calculus of axiom 5 of modal logic S5. (Contributed by NM, 5-Oct-2005.)
 
Theorem19.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.)
 F/   =>   
 
Theorem19.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.)
   &       =>   
 
Theoremexcomim 1458 One direction of Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
 
Theoremexcom 1459 Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.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.)
 
Theorem19.19 1461 Theorem 19.19 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremnf2 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.)
 F/
 
Theoremnf3 1463 An alternative definition of df-nf 1281. (Contributed by Mario Carneiro, 24-Sep-2016.)
 F/
 
Theorem19.36i 1464 Inference from Theorem 19.36 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 2-Feb-2015.)
   &       =>   
 
Theorem19.38 1465 Theorem 19.38 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.44 1466 Theorem 19.44 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theorem19.45 1467 Theorem 19.45 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theorem19.34 1468 Theorem 19.34 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
 
Theorem19.41 1469 Theorem 19.41 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
   =>   
 
Theorem19.42 1470 Theorem 19.42 of [Margaris] p. 90. (Contributed by NM, 18-Aug-1993.)
   =>   
 
Theoremexcom13 1471 Swap 1st and 3rd existential quantifiers. (Contributed by NM, 9-Mar-1995.)
 
Theoremexrot3 1472 Rotate existential quantifiers. (Contributed by NM, 17-Mar-1995.)
 
Theoremexrot4 1473 Rotate existential quantifiers twice. (Contributed by NM, 9-Mar-1995.)
 
Theoremnexr 1474 Inference from 19.8a 1407. (Contributed by Jeff Hankins, 26-Jul-2009.)
   =>   
 
Theoremexan 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.)
   =>   
 
Theoremhbexd 1476 Deduction form of bound-variable hypothesis builder hbex 1440. (Contributed by NM, 2-Jan-2002.)
   &       =>   
 
Theoremeeor 1477 Rearrange existential quantifiers. (Contributed by NM, 8-Aug-1994.)
   &       =>   
 
1.3.8  Equality theorems without distinct variables
 
Theorema9e 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.)
 
Theoremax9o 1479 An implication related to substitution. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
 
Theoremequid 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.)

 
Theoremstdpc6 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.)
 
Theoremequcomi 1482 Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.)
 
Theoremequcom 1483 Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
 
Theoremequcoms 1484 An inference commuting equality in antecedent. Used to eliminate the need for a syllogism. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremequtr 1485 A transitive law for equality. (Contributed by NM, 23-Aug-1993.)
 
Theoremequtrr 1486 A transitive law for equality. Lemma L17 in [Megill] p. 446 (p. 14 of the preprint). (Contributed by NM, 23-Aug-1993.)
 
Theoremequtr2 1487 A transitive law for equality. (Contributed by NM, 12-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)
 
Theoremequequ1 1488 An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
 
Theoremequequ2 1489 An equivalence law for equality. (Contributed by NM, 5-Aug-1993.)
 
Theoremelequ1 1490 An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)
 
Theoremelequ2 1491 An identity law for the non-logical predicate. (Contributed by NM, 5-Aug-1993.)
 
Theoremax11i 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
 
Theoremax10o 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.)

 
Axiomax-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.)

 
Theoremax10 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.)

 
Theoremhbae 1496 All variables are effectively bound in an identical variable specifier. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 3-Feb-2015.)
 
Theoremnfae 1497 All variables are effectively bound in an identical variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/
 
Theoremhbaes 1498 Rule that applies hbae 1496 to antecedent. (Contributed by NM, 5-Aug-1993.)
   =>   
 
Theoremhbnae 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.)
 
Theoremnfnae 1500 All variables are effectively bound in a distinct variable specifier. (Contributed by Mario Carneiro, 11-Aug-2016.)

 F/
    < 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-2000 21 2001-2100 22 2101-2186
  Copyright terms: Public domain < Previous  Next >