HomeHome Intuitionistic Logic Explorer
Theorem List (p. 14 of 20)
< 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 - 1301-1400   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremnic-ich 1301 Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   &       =>   
 
Theoremnic-idbl 1302 Double the terms. Since doubling is the same as negation, this can be viewed as a contraposition inference. (Contributed by Jeff Hoffman, 17-Nov-2007.)
   =>   
 
Theoremnic-bijust 1303 For nic-* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nic-bi1 1304 and nic-bi2 1305 are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18-Nov-2007.)
 
Theoremnic-bi1 1304 Inference to extract one side of an implication from a definition.
   =>   
 
Theoremnic-bi2 1305 Inference to extract the other side of an implication from a 'biconditional' definition.
   =>   
 
Theoremnic-stdmp 1306 Derive the standard modus ponens from nic-mp 1287. (Contributed by Jeff Hoffman, 18-Nov-2007.)
   &       =>   
 
Theoremnic-luk1 1307 Proof of luk-1 1265 from nic-ax 1289 and nic-mp 1287 (and definitions nic-dfim 1285 and nic-dfneg 1286). Note that the standard axioms ax-1 5, ax-2 6, and ax-3 7 are proved from the Lukasiewicz axioms by theorems ax1 1276, ax2 1277, and ax3 1278. (Contributed by Jeff Hoffman, 18-Nov-2007.)
 
Theoremnic-luk2 1308 Proof of luk-2 1266 from nic-ax 1289 and nic-mp 1287. (Contributed by Jeff Hoffman, 18-Nov-2007.)
 
Theoremnic-luk3 1309 Proof of luk-3 1267 from nic-ax 1289 and nic-mp 1287. (Contributed by Jeff Hoffman, 18-Nov-2007.)
 
1.3.6  True and false constants
 
Syntaxwtru 1310 is a wff.
 
Syntaxwfal 1311 is a wff.
 
Theoremtrujust 1312 Soundness justification theorem for df-tru 1313.
 
Definitiondf-tru 1313 Definition of , a tautology. is a constant true. In this definition biid 159 is used as an antecedent, however, any true wff, such as an axiom, can be used in its place.
 
Definitiondf-fal 1314 Definition of , a contradiction. is a constant false.
 
Theoremtru 1315 is provable. (Contributed by Anthony Hart, 13-Oct-2010.)
 
Theoremnotfal 1316 is not provable. (Contributed by Anthony Hart, 22-Oct-2010.) (The proof was shortened by Mel L. O'Cat, 11-Mar-2012.)
 
Theoremtrud 1317 Eliminate as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.)
   =>   
 
Theoremdfneg 1318 One definition of negation in logics that take as axiomatic is via "implies contradition", i.e. . (Contributed by Mario Carneiro, 2-Feb-2015.)
 
1.3.7  Auxiliary theorems for Alan Sare's virtual deduction tool, part 1
 
Theoremee22 1319 Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 2-May-2011.)
   &       &       =>   
 
Theoremee12an 1320 Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.)
   &       &       =>   
 
Theoremee23 1321 Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 17-Jul-2011.)
   &       &       =>   
 
Theoremexbir 1322 Exportation implication also converting head from biconditional to conditional. (Contributed by Alan Sare, 31-Dec-2011.)
 
Theorem3impexp 1323 impexp 249 with a 3-conjunct antecedent. (Contributed by Alan Sare, 31-Dec-2011.)
 
Theorem3impexpbicom 1324 3impexp 1323 with biconditional consequent of antecedent that is commuted in consequent. (Contributed by Alan Sare, 31-Dec-2011.)
 
Theorem3impexpbicomi 1325 Deduction form of 3impexpbicom 1324. (Contributed by Alan Sare, 31-Dec-2011.)
   =>   
 
Theoremancomsimp 1326 Closed form of ancoms 254. (Contributed by Alan Sare, 31-Dec-2011.)
 
Theoremexp3acom3r 1327 Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.)
   =>   
 
Theoremexp3acom23g 1328 Implication form of exp3acom23 1329.(Contributed by Alan Sare, 22-Jul-2012.)
 
Theoremexp3acom23 1329 The exportation deduction exp3a 244 with commutation of the conjoined wwfs. (Contributed by Alan Sare, 22-Jul-2012.)
   =>   
 
Theoremsimplbi2comg 1330 Implication form of simplbi2com 1331. (Contributed by Alan Sare, 22-Jul-2012.)
 
Theoremsimplbi2com 1331 A deduction eliminating a conjunct, similar to simplbi2 365. (Contributed by Alan Sare, 22-Jul-2012.) (The proof was shortened by Wolf Lammen, 10-Nov-2012.)
   =>   
 
Theoremee21 1332 Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 18-Mar-2012.)
   &       &       =>   
 
Theoremee10 1333 Special theorem needed for Alan Sare's virtual deduction translation tool.
   &       &       =>   
 
Theoremee02 1334 Special theorem needed for Alan Sare's virtual deduction translation tool.
   &       &       =>   
 
1.4  Predicate calculus mostly without distinct variables
 
1.4.1  "Pure" (equality-free) predicate calculus axioms ax-5, ax-6, ax-7, ax-gen
 
Syntaxwal 1335 Extend wff definition to include the universal quantifier ('for all'). is read " (phi) is true for all ." Typically, in its final application would be replaced with a wff containing a (free) occurrence of the variable , for example . In a universe with a finite number of objects, "for all" is equivalent to a big conjunction (AND) with one wff for each possible case of . When the universe is infinite (as with set theory), such a propositional-calculus equivalent is not possible because an infinitely long formula has no meaning, but conceptually the idea is the same.
 
Axiomax-5 1336 Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.
 
Axiomax-6 1337 Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113.
 
Axiomax-7 1338 Axiom of Quantifier Commutation. This axiom says universal quantifiers can be swapped. One of the 4 axioms of pure predicate calculus. Axiom scheme C6' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Lemma 12 of [Monk2] p. 109 and Axiom C5-3 of [Monk2] p. 113. An alternate axiomatization could use ax467 1455 in place of ax-4 1392, ax-6o 1428, and ax-7 1338.
 
Axiomax-gen 1339 Rule of Generalization. The postulated inference rule of pure predicate calculus. See e.g. Rule 2 of [Hamilton] p. 74. This rule says that if something is unconditionally true, then it is true for all values of a variable. For example, if we have proved , we can conclude or even . Theorem a4i 1432 shows we can go the other way also: in other words we can add or remove universal quantifiers from the beginning of any theorem as required.
   =>   
 
Theoremgen2 1340 Generalization applied twice.
   =>   
 
Theoremmpg 1341 Modus ponens combined with generalization.
   &       =>   
 
Theoremmpgbi 1342 Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
   &       =>   
 
Theoremmpgbir 1343 Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.)
   &       =>   
 
Theorema7s 1344 Swap quantifiers in an antecedent.
   =>   
 
Theoremalimi 1345 Inference quantifying both antecedent and consequent.
   =>   
 
Theorem2alimi 1346 Inference doubly quantifying both antecedent and consequent.
   =>   
 
Theoremalim 1347 Theorem 19.20 of [Margaris] p. 90. (The proof was shortened by O'Cat, 30-Mar-2008.)
 
Theoremal2imi 1348 Inference quantifying antecedent, nested antecedent, and consequent.
   =>   
 
Theoremalanimi 1349 Variant of al2imi 1348 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.)
   =>   
 
Theoremalimd 1350 Deduction from Theorem 19.20 of [Margaris] p. 90.
   &       =>   
 
Theoremalbi 1351 Theorem 19.15 of [Margaris] p. 90.
 
Theoremalrimi 1352 Inference from Theorem 19.21 of [Margaris] p. 90.
   &       =>   
 
Theoremalbii 1353 Inference adding universal quantifier to both sides of an equivalence.
   =>   
 
Theorem2albii 1354 Inference adding 2 universal quantifiers to both sides of an equivalence.
   =>   
 
Theoremhbth 1355 No variable is (effectively) free in a theorem.

This and later "hypothesis-building" lemmas, with labels starting "hb...", allow us to construct proofs of formulas of the form from smaller formulas of this form. These are useful for constructing hypotheses that state " is (effectively) not free in ."

   =>   
 
Theoremhbxfrbi 1356 A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
   &       =>   
 
Theoremhbal 1357 If is not free in , it is not free in .
   =>   
 
Theoremalcom 1358 Theorem 19.5 of [Margaris] p. 89.
 
Theoremalrimd 1359 Deduction from Theorem 19.21 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.)
   &       &       =>   
 
Theoremalbid 1360 Formula-building rule for universal quantifier (deduction rule).
   &       =>   
 
Theorem19.26 1361 Theorem 19.26 of [Margaris] p. 90. Also Theorem *10.22 of [WhiteheadRussell] p. 119. (The proof was shortened by Wolf Lammen, 4-Jul-2014.)
 
Theorem19.26OLD 1362 Obsolete proof of 19.26 1361 as of 4-Jul-2014.
 
Theorem19.26-2 1363 Theorem 19.26 of [Margaris] p. 90 with two quantifiers.
 
Theorem19.26-3an 1364 Theorem 19.26 of [Margaris] p. 90 with triple conjunction.
 
Theorem19.33 1365 Theorem 19.33 of [Margaris] p. 90.
 
Theoremalrot3 1366 Theorem *11.21 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.)
 
Theoremalrot4 1367 Rotate 4 universal quantifiers twice. (The proof was shortened by Wolf Lammen, 28-Jun-2014.)
 
Theoremalrot4OLD 1368 Obsolete proof of alrot4 1367 as of 28-Jun-2014.
 
Theoremalbiim 1369 Split a biconditional and distribute quantifier.
 
Theorem2albiim 1370 Split a biconditional and distribute 2 quantifiers.
 
Theoremhband 1371 Deduction form of bound-variable hypothesis builder hban 1441.
   &       =>   
 
Theoremhb3and 1372 Deduction form of bound-variable hypothesis builder hb3an 1444.
   &       &       =>   
 
Theoremhbald 1373 Deduction form of bound-variable hypothesis builder hbal 1357.
   &       =>   
 
Syntaxwex 1374 Extend wff definition to include the existential quantifier ("there exists").
 
Axiomax-ie1 1375 is bound in . Axiom 9 of 10 for intuitionistic logic.
 
Axiomax-ie2 1376 Define existential quantification. means "there exists at least one set such that is true." Axiom 10 of 10 for intuitionistic logic.
 
Theoremhbe1 1377 is not free in .
 
Theorem19.23t 1378 Closed form of Theorem 19.23 of [Margaris] p. 90. (Revised by Mario Carneiro, 1-Feb-2015.)
 
Theorem19.23 1379 Theorem 19.23 of [Margaris] p. 90. (Revised by Mario Carneiro, 1-Feb-2015.)
   =>   
 
Theoremalnex 1380 Theorem 19.7 of [Margaris] p. 89.
 
Theoremdf-ex 1381 Define existential quantification. means "there exists at least one set such that is true." Definition of [Margaris] p. 49.
 
1.4.2  Introduce equality axioms ax-8 through ax-14 except ax-9
 
Syntaxcv 1382 This syntax construction states that a variable , which has been declared to be a set variable by $f statement vx, is also a class expression. See comments in set.mm for justification.

While it is tempting and perhaps occasionally useful to view cv 1382 as a "type conversion" from a set variable to a class variable, keep in mind that cv 1382 is intrinsically no different from any other class-building syntax.

(The description above applies to set theory, not predicate calculus. The purpose of introducing here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1384 of predicate calculus from the wceq 1383 of set theory, so that we don't "overload" the connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers.)

 
Syntaxwceq 1383 Extend wff definition to include class equality.

(The purpose of introducing here, and not in set theory where it belongs, is to allow us to express i.e. "prove" the weq 1384 of predicate calculus in terms of the wceq 1383 of set theory, so that we don't "overload" the connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. For example, some parsers - although not the Metamath program - stumble on the fact that the in could be the of either weq 1384 or wceq 1383, although mathematically it makes no difference. The class variables and are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus.)

 
Theoremweq 1384 Extend wff definition to include atomic formulas using the equality predicate.

(Instead of introducing weq 1384 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wceq 1383. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically weq 1384 is considered to be a primitive syntax, even though here it is artificially "derived" from wceq 1383. Note: To see the proof steps of this syntax proof, type "show proof weq /all" in the Metamath program.)

 
Syntaxwcel 1385 Extend wff definition to include the membership connective between classes.

(The purpose of introducing here is to allow us to express i.e. "prove" the wel 1386 of predicate calculus in terms of the wceq 1383 of set theory, so that we don't "overload" the connective with two syntax definitions. This is done to prevent ambiguity that would complicate some Metamath parsers. The class variables and are introduced temporarily for the purpose of this definition but otherwise not used in predicate calculus.)

 
Theoremwel 1386 Extend wff definition to include atomic formulas with the epsilon (membership) predicate. This is read " is an element of ," " is a member of ," " belongs to ," or " contains ." Note: The phrase " includes " means " is a subset of ;" to use it also for , as some authors occasionally do, is poor form and causes confusion, according to George Boolos (1992 lecture at MIT).

This syntactical construction introduces a binary non-logical predicate symbol (epsilon) into our predicate calculus. We will eventually use it for the membership predicate of set theory, but that is irrelevant at this point: the predicate calculus axioms for apply to any arbitrary binary predicate symbol. "Non-logical" means that the predicate is presumed to have additional properties beyond the realm of predicate calculus, although these additional properties are not specified by predicate calculus itself but rather by the axioms of a theory (in our case set theory) added to predicate calculus. "Binary" means that the predicate has two arguments.

(Instead of introducing wel 1386 as an axiomatic statement, as was done in an older version of this database, we introduce it by "proving" a special case of set theory's more general wcel 1385. This lets us avoid overloading the connective, thus preventing ambiguity that would complicate certain Metamath parsers. However, logically wel 1386 is considered to be a primitive syntax, even though here it is artificially "derived" from wcel 1385. Note: To see the proof steps of this syntax proof, type "show proof wel /all" in the Metamath program.)

 
Axiomax-8 1387 Axiom of Equality. One of the equality and substitution axioms of predicate calculus with equality. This is similar to, but not quite, a transitive law for equality (proved later as equtr 1567). Axiom scheme C8' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom C7 of [Monk2] p. 105.

Axioms ax-8 1387 through ax-16 1644 are the axioms having to do with equality, substitution, and logical properties of our binary predicate (which later in set theory will mean "is a member of"). Note that all axioms except ax-16 1644 and ax-17 1402 are still valid even when , , and are replaced with the same variable because they do not have any distinct variable (Metamath's $d) restrictions. Distinct variable restrictions are required for ax-16 1644 and ax-17 1402 only.

 
Axiomax-10 1388 Axiom of Quantifier Substitution. One of the equality and substitution axioms of predicate calculus with equality. Appears as Lemma L12 in [Megill] p. 445 (p. 12 of the preprint).

The original version of this axiom was ax-10o 1576 ("o" for "old") and was replaced with this shorter ax-10 1388 in May 2008. The old axiom is proved from this one as theorem ax10o 1575. Conversely, this axiom is proved from ax-10o 1576 as theorem ax10 1577.

 
Axiomax-11 1389 Axiom of Variable Substitution. One of the 5 equality axioms of predicate calculus. The final consequent is a way of expressing " substituted for in wff " (cf. sb6 1705). It is based on Lemma 16 of [Tarski] p. 70 and Axiom C8 of [Monk2] p. 105, from which it can be proved by cases.

The original version of this axiom was ax-11o 1654 ("o" for "old") and was replaced with this shorter ax-11 1389 in Jan. 2007. The old axiom is proved from this one as theorem ax11o 1653. Conversely, this axiom is proved from ax-11o 1654 as theorem ax11 1655.

Juha Arpiainen proved the independence of this axiom (in the form of the older axiom ax-11o 1654) from the others on 19-Jan-2006. See item 9a at http://us.metamath.org/award2003.html.

Interestingly, if the wff expression substituted for contains no wff variables, the resulting statement can be proved without invoking this axiom. This means that even though this axiom is metalogically independent from the others, it is not logically independent. Specifically, we can prove any wff-variable-free instance of axiom ax-11o 1654 (from which the ax-11 1389 instance follows by theorem ax11 1655.) The proof is by induction on formula length, using ax11eq 1810 and ax11el 1811 for the basis steps and ax11indn 1813, ax11indi 1814, and ax11inda 1818 for the induction steps.

See also ax11v 1703 and ax11v2 1651 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions.

 
Axiomax-i11e 1390 Axiom of Variable Substitution for Existence. This can be derived from ax-11 1389 in a classical context but a separate axiom is needed for intuitionistic predicate calculus.
 
Axiomax-i12 1391 Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever is distinct from and , and is true, then quantified with is also true. In other words, is irrelevant to the truth of . Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases.

An open problem is whether this axiom is redundant. Note that the analogous axiom for the membership connective, ax-15 1807, has been shown to be redundant. It is also unknown whether this axiom can be replaced by a shorter formula. However, it can be derived from two slightly shorter formulas, as shown by a12study 1825.

This axiom has been modified from the original ax-12 1393 for compatibility with intuitionistic logic.

 
Axiomax-4 1392 Axiom of Specialization. A quantified wff implies the wff without a quantifier (i.e. an instance, or special case, of the generalized wff). In other words if something is true for all , it is true for any specific (that would typically occur as a free variable in the wff substituted for ). (A free variable is one that does not occur in the scope of a quantifier: and are both free in , but only is free in .) This is one of the axioms of what we call "pure" predicate calculus (ax-4 1392 through ax-7 1338 plus rule ax-gen 1339). Axiom scheme C5' in [Megill] p. 448 (p. 16 of the preprint). Also appears as Axiom B5 of [Tarski] p. 67 (under his system S2, defined in the last paragraph on p. 77).

Note that the converse of this axiom does not hold in general, but a weaker inference form of the converse holds and is expressed as rule ax-gen 1339. Conditional forms of the converse are given by ax-12 1393, ax-15 1807, ax-16 1644, and ax-17 1402.

Unlike the more general textbook Axiom of Specialization, we cannot choose a variable different from for the special case. For use, that requires the assistance of equality axioms, and we deal with it later after we introduce the definition of proper substitution - see stdpc4 1619.

An nice alternate axiomatization uses ax467 1455 and ax-5o 1425 in place of ax-4 1392, ax-5 1336, ax-6 1337, and ax-7 1338.

This axiom is redundant in the presence of certain other axioms, as shown by theorem ax4 1423. (We replaced the older ax-5o 1425 and ax-6o 1428 with newer versions ax-5 1336 and ax-6 1337 in order to prove this redundancy.)

 
Theoremax-12 1393 Rederive the original version of the axiom from ax-i12 1391. Note that we need ax-4 1392 for the derivation, but the proof of ax4 1423 is nontheless non-circular since it does not use ax-12. (Contributed by Mario Carneiro, 3-Feb-2015.)
 
Theoremax12or 1394 Derive the intuitionistic form of ax-12 1393 from the original form.
 
Axiomax-13 1395 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.
 
Axiomax-14 1396 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.
 
Theoremhbequid 1397 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 1387, ax-12 1393, and ax-gen 1339. This shows that this can be proved without ax-9 1418, even though the theorem equid 1562 cannot be. A shorter proof using ax-9 1418 is obtainable from equid 1562 and hbth 1355.) (The proof was shortened by Wolf Lammen, 23-Mar-2014.)
 
TheoremhbequidOLD 1398 Obsolete proof of hbequid 1397 as of 23-Mar-2014.
 
Theoremalequcom 1399 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).
 
Theoremalequcoms 1400 A commutation rule for identical variable specifiers.
   =>   
    < 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-1914
  Copyright terms: Public domain < Previous  Next >