Home | Intuitionistic Logic ExplorerTheorem List (p. 14 of 20)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

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

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

Statement | ||

Theorem | nic-ich 1301 | Chained inference. (Contributed by Jeff Hoffman, 17-Nov-2007.) |

Theorem | nic-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.) |

Theorem | nic-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.) |

Theorem | nic-bi1 1304 | Inference to extract one side of an implication from a definition. |

Theorem | nic-bi2 1305 | Inference to extract the other side of an implication from a 'biconditional' definition. |

Theorem | nic-stdmp 1306 | Derive the standard modus ponens from nic-mp 1287. (Contributed by Jeff Hoffman, 18-Nov-2007.) |

Theorem | nic-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.) |

Theorem | nic-luk2 1308 | Proof of luk-2 1266 from nic-ax 1289 and nic-mp 1287. (Contributed by Jeff Hoffman, 18-Nov-2007.) |

Theorem | nic-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 | ||

Syntax | wtru 1310 | is a wff. |

Syntax | wfal 1311 | is a wff. |

Theorem | trujust 1312 | Soundness justification theorem for df-tru 1313. |

Definition | df-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. |

Definition | df-fal 1314 | Definition of , a contradiction. is a constant false. |

Theorem | tru 1315 | is provable. (Contributed by Anthony Hart, 13-Oct-2010.) |

Theorem | notfal 1316 | is not provable. (Contributed by Anthony Hart, 22-Oct-2010.) (The proof was shortened by Mel L. O'Cat, 11-Mar-2012.) |

Theorem | trud 1317 | Eliminate as an antecedent. (Contributed by Mario Carneiro, 13-Mar-2014.) |

Theorem | dfneg 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 | ||

Theorem | ee22 1319 | Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 2-May-2011.) |

Theorem | ee12an 1320 | Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 28-Oct-2011.) |

Theorem | ee23 1321 | Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 17-Jul-2011.) |

Theorem | exbir 1322 | Exportation implication also converting head from biconditional to conditional. (Contributed by Alan Sare, 31-Dec-2011.) |

Theorem | 3impexp 1323 | impexp 249 with a 3-conjunct antecedent. (Contributed by Alan Sare, 31-Dec-2011.) |

Theorem | 3impexpbicom 1324 | 3impexp 1323 with biconditional consequent of antecedent that is commuted in consequent. (Contributed by Alan Sare, 31-Dec-2011.) |

Theorem | 3impexpbicomi 1325 | Deduction form of 3impexpbicom 1324. (Contributed by Alan Sare, 31-Dec-2011.) |

Theorem | ancomsimp 1326 | Closed form of ancoms 254. (Contributed by Alan Sare, 31-Dec-2011.) |

Theorem | exp3acom3r 1327 | Export and commute antecedents. (Contributed by Alan Sare, 18-Mar-2012.) |

Theorem | exp3acom23g 1328 | Implication form of exp3acom23 1329.(Contributed by Alan Sare, 22-Jul-2012.) |

Theorem | exp3acom23 1329 | The exportation deduction exp3a 244 with commutation of the conjoined wwfs. (Contributed by Alan Sare, 22-Jul-2012.) |

Theorem | simplbi2comg 1330 | Implication form of simplbi2com 1331. (Contributed by Alan Sare, 22-Jul-2012.) |

Theorem | simplbi2com 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.) |

Theorem | ee21 1332 | Special theorem needed for Alan Sare's virtual deduction translation tool. (Contributed by Alan Sare, 18-Mar-2012.) |

Theorem | ee10 1333 | Special theorem needed for Alan Sare's virtual deduction translation tool. |

Theorem | ee02 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 | ||

Syntax | wal 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. |

Axiom | ax-5 1336 | Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105. |

Axiom | ax-6 1337 | Axiom of Quantified Negation. Axiom C5-2 of [Monk2] p. 113. |

Axiom | ax-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. |

Axiom | ax-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. |

Theorem | gen2 1340 | Generalization applied twice. |

Theorem | mpg 1341 | Modus ponens combined with generalization. |

Theorem | mpgbi 1342 | Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.) |

Theorem | mpgbir 1343 | Modus ponens on biconditional combined with generalization. (The proof was shortened by Stefan Allan, 28-Oct-2008.) |

Theorem | a7s 1344 | Swap quantifiers in an antecedent. |

Theorem | alimi 1345 | Inference quantifying both antecedent and consequent. |

Theorem | 2alimi 1346 | Inference doubly quantifying both antecedent and consequent. |

Theorem | alim 1347 | Theorem 19.20 of [Margaris] p. 90. (The proof was shortened by O'Cat, 30-Mar-2008.) |

Theorem | al2imi 1348 | Inference quantifying antecedent, nested antecedent, and consequent. |

Theorem | alanimi 1349 | Variant of al2imi 1348 with conjunctive antecedent. (Contributed by Andrew Salmon, 8-Jun-2011.) |

Theorem | alimd 1350 | Deduction from Theorem 19.20 of [Margaris] p. 90. |

Theorem | albi 1351 | Theorem 19.15 of [Margaris] p. 90. |

Theorem | alrimi 1352 | Inference from Theorem 19.21 of [Margaris] p. 90. |

Theorem | albii 1353 | Inference adding universal quantifier to both sides of an equivalence. |

Theorem | 2albii 1354 | Inference adding 2 universal quantifiers to both sides of an equivalence. |

Theorem | hbth 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 ." |

Theorem | hbxfrbi 1356 | A utility lemma to transfer a bound-variable hypothesis builder into a definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |

Theorem | hbal 1357 | If is not free in , it is not free in . |

Theorem | alcom 1358 | Theorem 19.5 of [Margaris] p. 89. |

Theorem | alrimd 1359 | Deduction from Theorem 19.21 of [Margaris] p. 90. (The proof was shortened by Andrew Salmon, 13-May-2011.) |

Theorem | albid 1360 | Formula-building rule for universal quantifier (deduction rule). |

Theorem | 19.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.) |

Theorem | 19.26OLD 1362 | Obsolete proof of 19.26 1361 as of 4-Jul-2014. |

Theorem | 19.26-2 1363 | Theorem 19.26 of [Margaris] p. 90 with two quantifiers. |

Theorem | 19.26-3an 1364 | Theorem 19.26 of [Margaris] p. 90 with triple conjunction. |

Theorem | 19.33 1365 | Theorem 19.33 of [Margaris] p. 90. |

Theorem | alrot3 1366 | Theorem *11.21 in [WhiteheadRussell] p. 160. (Contributed by Andrew Salmon, 24-May-2011.) |

Theorem | alrot4 1367 | Rotate 4 universal quantifiers twice. (The proof was shortened by Wolf Lammen, 28-Jun-2014.) |

Theorem | alrot4OLD 1368 | Obsolete proof of alrot4 1367 as of 28-Jun-2014. |

Theorem | albiim 1369 | Split a biconditional and distribute quantifier. |

Theorem | 2albiim 1370 | Split a biconditional and distribute 2 quantifiers. |

Theorem | hband 1371 | Deduction form of bound-variable hypothesis builder hban 1441. |

Theorem | hb3and 1372 | Deduction form of bound-variable hypothesis builder hb3an 1444. |

Theorem | hbald 1373 | Deduction form of bound-variable hypothesis builder hbal 1357. |

Syntax | wex 1374 | Extend wff definition to include the existential quantifier ("there exists"). |

Axiom | ax-ie1 1375 | is bound in . Axiom 9 of 10 for intuitionistic logic. |

Axiom | ax-ie2 1376 | Define existential quantification. means "there exists at least one set such that is true." Axiom 10 of 10 for intuitionistic logic. |

Theorem | hbe1 1377 | is not free in . |

Theorem | 19.23t 1378 | Closed form of Theorem 19.23 of [Margaris] p. 90. (Revised by Mario Carneiro, 1-Feb-2015.) |

Theorem | 19.23 1379 | Theorem 19.23 of [Margaris] p. 90. (Revised by Mario Carneiro, 1-Feb-2015.) |

Theorem | alnex 1380 | Theorem 19.7 of [Margaris] p. 89. |

Theorem | df-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 | ||

Syntax | cv 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.) |

Syntax | wceq 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.) |

Theorem | weq 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.) |

Syntax | wcel 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.) |

Theorem | wel 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.) |

Axiom | ax-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. |

Axiom | ax-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. |

Axiom | ax-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 See also ax11v 1703 and ax11v2 1651 for other equivalents of this axiom that (unlike this axiom) have distinct variable restrictions. |

Axiom | ax-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. |

Axiom | ax-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. |

Axiom | ax-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.) |

Theorem | ax-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.) |

Theorem | ax12or 1394 | Derive the intuitionistic form of ax-12 1393 from the original form. |

Axiom | ax-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. |

Axiom | ax-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. |

Theorem | hbequid 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.) |

Theorem | hbequidOLD 1398 | Obsolete proof of hbequid 1397 as of 23-Mar-2014. |

Theorem | alequcom 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). |

Theorem | alequcoms 1400 | A commutation rule for identical variable specifiers. |

< Previous Next > |

Copyright terms: Public domain | < Previous Next > |