HomeHome Intuitionistic Logic Explorer
Theorem List (p. 8 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 - 701-800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theorempm3.2ni 701 Infer negated disjunction of negated premises.
   &       =>   
 
Theoremorabs 702 Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (The proof was shortened by Wolf Lammen, 28-Feb-2014.)
 
TheoremorabsOLD 703 Obsolete proof of orabs 702 as of 28-Feb-2014.
 
Theoremoranabs 704 Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton 23-Jun-2005.) (The proof was shortened by Wolf Lammen, 10-Nov-2013.)
 
Theoremordi 705 Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theoremordir 706 Distributive law for disjunction.
 
Theoremandi 707 Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (The proof was shortened by Wolf Lammen, 5-Jan-2013.)
 
Theoremandir 708 Distributive law for conjunction.
 
Theoremorddi 709 Double distributive law for disjunction.
 
Theoremanddi 710 Double distributive law for conjunction.
 
Theorempm4.39 711 Theorem *4.39 of [WhiteheadRussell] p. 118.
 
Theorempm4.72 712 Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (The proof was shortened by Wolf Lammen, 30-Jan-2013.)
 
Theorempm5.16 713 Theorem *5.16 of [WhiteheadRussell] p. 124. (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorembiort 714 A wff is disjoined with truth is true.
 
1.2.7  Classical logic
 
Theoremcon4d 715 Deduction derived from axiom ax-3 7.
   =>   
 
Theorempm2.18 716 Proof by contradiction. Theorem *2.18 of [WhiteheadRussell] p. 103. Also called the Law of Clavius.
 
Theorempm2.18d 717 Deduction based on reductio ad absurdum. (Contributed by FL, 12-Jul-2009.) (The proof was shortened by Andrew Salmon, 7-May-2011.)
   =>   
 
Theoremnotnot2 718 Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. (The proof was shortened by David Harvey, 5-Sep-1999. An even shorter proof found by Josh Purinton, 29-Dec-2000.)
 
Theoremnotnotri 719 Inference from double negation.
   =>   
 
Theoremcon1d 720 A contraposition deduction.
   =>   
 
Theoremcon1 721 Contraposition. Theorem *2.15 of [WhiteheadRussell] p. 102. (The proof was shortened by Wolf Lammen, 12-Feb-2013.)
 
Theoremmt3d 722 Modus tollens deduction.
   &       =>   
 
Theoremmt3i 723 Modus tollens inference. (The proof was shortened by Wolf Lammen, 15-Sep-2012.)
   &       =>   
 
Theoremmt3 724 A rule similar to modus tollens. (The proof was shortened by Wolf Lammen, 11-Sep-2013.)
   &       =>   
 
Theoremnsyl2 725 A negated syllogism inference.
   &       =>   
 
Theoremcon1i 726 A contraposition inference. (The proof was shortened by O'Cat, 28-Nov-2008.) (The proof was shortened by Wolf Lammen, 19-Jun-2013.)
   =>   
 
Theoremnsyl4 727 A negated syllogism inference.
   &       =>   
 
Theoremcon4i 728 Inference rule derived from axiom ax-3 7. (The proof was shortened by Wolf Lammen, 21-Jun-2013.)
   =>   
 
Theoremimpi 729 An importation inference. (The proof was shortened by Wolf Lammen, 20-Jul-2013.)
   =>   
 
Theoremsimprim 730 Simplification. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (The proof was shortened by Wolf Lammen, 13-Nov-2012.)
 
Theoremsimplim 731 Simplification. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (The proof was shortened by Wolf Lammen, 21-Jul-2012.)
 
Theoremmt4 732 The rule of modus tollens. (Contributed by Wolf Lammen, 12-May-2013.)
   &       =>   
 
Theoremmt4d 733 Modus tollens deduction.
   &       =>   
 
Theoremmt4i 734 Modus tollens inference. (Contributed by Wolf Lammen, 12-May-2013.)
   &       =>   
 
Theorempm2.61d 735 Deduction eliminating an antecedent. (The proof was shortened by Wolf Lammen, 12-Sep-2013.)
   &       =>   
 
Theorempm2.61d1 736 Inference eliminating an antecedent.
   &       =>   
 
Theorempm2.61d2 737 Inference eliminating an antecedent.
   &       =>   
 
Theoremja 738 Inference joining the antecedents of two premises. (The proof was shortened by O'Cat, 19-Feb-2008.)
   &       =>   
 
Theoremjad 739 Deduction form of ja 738. (Contributed by Scott Fenton, 13-Dec-2010.) (The proof was shortened by Andrew Salmon, 17-Sep-2011.)
   &       =>   
 
Theorempeirce 740 Peirce's axiom. This odd-looking theorem is the "difference" between an intuitionistic system of propositional calculus and a classical system and is not accepted by intuitionists. When Peirce's axiom is added to an intuitionistic system, the system becomes equivalent to our classical system ax-1 5 through ax-3 7. A curious fact about this theorem is that it requires ax-3 7 for its proof even though the result has no negation connectives in it. (The proof was shortened by Wolf Lammen, 9-Oct-2012.)
 
Theorempm2.6 741 Theorem *2.6 of [WhiteheadRussell] p. 107.
 
Theorempm2.61 742 Theorem *2.61 of [WhiteheadRussell] p. 107. Useful for eliminating an antecedent. (The proof was shortened by Wolf Lammen, 22-Sep-2013.)
 
Theorempm2.61i 743 Inference eliminating an antecedent. (The proof was shortened by Wolf Lammen, 12-Sep-2013.)
   &       =>   
 
Theorempm2.61ii 744 Inference eliminating two antecedents. (The proof was shortened by Josh Purinton, 29-Dec-2000.)
   &       &       =>   
 
Theorempm2.61ian 745 Elimination of an antecedent.
   &       =>   
 
Theorempm2.61dan 746 Elimination of an antecedent.
   &       =>   
 
Theorempm2.61ddan 747 Elimination of two antecedents.
   &       &       =>   
 
Theorempm2.61dda 748 Elimination of two antecedents.
   &       &       =>   
 
Theorempm2.61nii 749 Inference eliminating two antecedents. (The proof was shortened by Andrew Salmon, 25-May-2011.) (The proof was shortened by Wolf Lammen, 13-Nov-2012.)
   &       &       =>   
 
Theorempm2.61iii 750 Inference eliminating three antecedents. (The proof was shortened by Wolf Lammen, 22-Sep-2013.)
   &       &       &       =>   
 
Theoremimpt 751 Importation theorem expressed with primitive connectives. (The proof was shortened by Wolf Lammen, 20-Jul-2013.)
 
Theoremimpcon4bid 752 A variation on impbid 119 with contraposition. (Contributed by Jeff Hankins, 3-Jul-2009.)
   &       =>   
 
Theorempm2.5 753 Theorem *2.5 of [WhiteheadRussell] p. 107. (The proof was shortened by Wolf Lammen, 9-Oct-2012.)
 
Theorempm2.521 754 Theorem *2.521 of [WhiteheadRussell] p. 107. (The proof was shortened by Wolf Lammen, 8-Oct-2012.)
 
Theoremloolin 755 The Linearity Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. For a version not using ax-3 7, see loolinALT 94. (Contributed by O'Cat, 12-Aug-2004.) (The proof was shortened by Wolf Lammen, 2-Nov-2012.)
 
Theoremlooinv 756 The Inversion Axiom of the infinite-valued sentential logic (L-infinity) of Lukasiewicz. Using dfor2 794, we can see that this essentially expresses "disjunction commutes." Theorem *2.69 of [WhiteheadRussell] p. 108.
 
Theoremcon34b 757 Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116.
 
Theoremnotnot 758 Double negation. Theorem *4.13 of [WhiteheadRussell] p. 117.
 
Theoremcon4bid 759 A contraposition deduction.
   =>   
 
Theoremnotbi 760 Contraposition. Theorem *4.11 of [WhiteheadRussell] p. 117. (The proof was shortened by Wolf Lammen, 12-Jun-2013.)
 
Theoremcon2bi 761 Contraposition. Theorem *4.12 of [WhiteheadRussell] p. 117. (The proof was shortened by Wolf Lammen, 3-Jan-2013.)
 
Theoremcon2bid 762 A contraposition deduction.
   =>   
 
Theoremcon1bid 763 A contraposition deduction.
   =>   
 
Theoremcon1bii 764 A contraposition inference. (The proof was shortened by Wolf Lammen, 13-Oct-2012.)
   =>   
 
Theoremcon1biiOLD 765 Obsolete proof of con1bii 764 as of 28-Sep-2014.
   =>   
 
Theoremcon1b 766 Contraposition. Bidirectional version of con1 721.
 
Theoremcon4bii 767 A contraposition inference.
   =>   
 
Theoremcon2bii 768 A contraposition inference.
   =>   
 
Theorembija 769 Combine antecedents into a single bi-conditional. This inference, reminiscent of ja 738, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im 161 and pm5.21im 591). (Contributed by Wolf Lammen, 13-May-2013.)
   &       =>   
 
Theorempm5.18 770 Theorem *5.18 of [WhiteheadRussell] p. 124. This theorem says that logical equivalence is the same as negated "exclusive-or." (The proof was shortened by Andrew Salmon, 20-Jun-2011.) (The proof was shortened by Wolf Lammen, 15-Oct-2013.)
 
Theoremxor3 771 Two ways to express "exclusive or."
 
Theoremnbbn 772 Move negation outside of biconditional. Compare Theorem *5.18 of [WhiteheadRussell] p. 124. (The proof was shortened by Wolf Lammen, 20-Sep-2013.)
 
Theorembiass 773 Associative law for the biconditional. An axiom of system DS in Vladimir Lifschitz, "On calculational proofs", Annals of Pure and Applied Logic, 113:207-224, 2002, http://www.cs.utexas.edu/users/ai-lab/pub-view.php?PubID=26805. Interestingly, this law was not included in Principia Mathematica but was apparently first noted by Jan Lukasiewicz circa 1923. (The proof was shortened by Juha Arpiainen, 19-Jan-2006.) (The proof was shortened by Wolf Lammen, 21-Sep-2013.)
 
Theorempm4.81 774 Theorem *4.81 of [WhiteheadRussell] p. 122.
 
Theoremdf-an 775 Definition of 'and' in terms of negation and implication (classical).
 
Theorempm4.63 776 Theorem *4.63 of [WhiteheadRussell] p. 120.
 
Theorempm4.67 777 Theorem *4.67 of [WhiteheadRussell] p. 120.
 
Theoremdfbi1 778 Relate the biconditional connective to primitive connectives.
 
Theoremiman 779 Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (The proof was shortened by Wolf Lammen, 30-Oct-2012.)
 
Theoremannim 780 Express conjunction in terms of implication.
 
Theorempm4.61 781 Theorem *4.61 of [WhiteheadRussell] p. 120.
 
Theorempm4.65 782 Theorem *4.65 of [WhiteheadRussell] p. 120.
 
Theorempm4.14 783 Theorem *4.14 of [WhiteheadRussell] p. 117. (The proof was shortened by Wolf Lammen, 23-Oct-2012.)
 
Theorempm3.37 784 Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112. (The proof was shortened by Wolf Lammen, 23-Oct-2012.)
 
Theorempm4.15 785 Theorem *4.15 of [WhiteheadRussell] p. 117. (The proof was shortened by Wolf Lammen, 18-Nov-2012.)
 
Theoremcondan 786 Proof by contradiction. (The proof was shortened by Wolf Lammen, 19-Jun-2014.)
   &       =>   
 
Theoremxordi 787 Conjunction distributes over exclusive-or, using to express exclusive-or. This is one way to interpret the distributive law of multiplication over addition in modulo 2 arithmetic.
 
Theorempm2.54 788 Theorem *2.54 of [WhiteheadRussell] p. 107.
 
Theoremdf-or 789 Define disjunction (logical 'or'). Definition of [Margaris] p. 49.
 
Theoremorrd 790 Deduce implication from disjunction.
   =>   
 
Theoremorri 791 Infer implication from disjunction.
   =>   
 
Theorempm2.25 792 Theorem *2.25 of [WhiteheadRussell] p. 104.
 
Theorempm2.68 793 Theorem *2.68 of [WhiteheadRussell] p. 108.
 
Theoremdfor2 794 Logical 'or' expressed in terms of implication only. Theorem *5.25 of [WhiteheadRussell] p. 124. (The proof was shortened by Wolf Lammen, 20-Oct-2012.)
 
Theorempm4.64 795 Theorem *4.64 of [WhiteheadRussell] p. 120.
 
Theoremimor 796 Implication in terms of disjunction. Theorem *4.6 of [WhiteheadRussell] p. 120.
 
Theoremimori 797 Infer disjunction from implication.
   =>   
 
Theoremexmid 798 Law of excluded middle, also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. This is an essential distinction of our classical logic and is not a theorem of intuitionistic logic.
 
Theorempm2.1 799 Theorem *2.1 of [WhiteheadRussell] p. 101. (The proof was shortened by Wolf Lammen, 23-Nov-2012.)
 
Theorempm2.13 800 Theorem *2.13 of [WhiteheadRussell] p. 101.
    < 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-700701-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 >