HomeHome Intuitionistic Logic Explorer
Theorem List (p. 8 of 21)
< 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
 
Theorempm2.82 701 Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
 
Theorempm3.2ni 702 Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
   &       =>   
 
Theoremorabs 703 Absorption of redundant internal disjunct. Compare Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 28-Feb-2014.)
 
TheoremorabsOLD 704 Obsolete proof of orabs 703 as of 28-Feb-2014. (Contributed by NM, 5-Aug-1993.)
 
Theoremoranabs 705 Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
 
Theoremordi 706 Distributive law for disjunction. Theorem *4.41 of [WhiteheadRussell] p. 119. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theoremordir 707 Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
 
Theoremandi 708 Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)
 
Theoremandir 709 Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
 
Theoremorddi 710 Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
 
Theoremanddi 711 Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
 
Theorempm4.39 712 Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
 
Theorempm4.72 713 Implication in terms of biconditional and disjunction. Theorem *4.72 of [WhiteheadRussell] p. 121. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 30-Jan-2013.)
 
Theorempm5.16 714 Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
 
Theorembiort 715 A wff is disjoined with truth is true. (Contributed by NM, 23-May-1999.)
 
1.2.7  Decidable propositions
 
Syntaxwdc 716 Extend wff definition to include decidability.
DECID
 
Definitiondf-dc 717 Propositions which are known to be true or false are called decidable. The (classical) Law of the Excluded Middle corresponds to the principle that all propositions are decidable, but even given intuitionistic logic, particular kinds of propositions may be decidable (for example, the proposition that two natural numbers are equal will be decidable under most sets of axioms).

Our notation for decidability is a connective DECID which we place before the formula in question. For example, DECID corresponds to "x = y is decidable". (Contributed by Jim Kingdon, 11-Mar-2018.)

DECID
 
Theoremexmiddc 718 Law of excluded middle, for a decidable proposition. The law of the excluded middle is 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. The key way in which intuitionistic logic differs from classical logic is that intuitionistic logic says that excluded middle only holds for some propositions, and classical logic says that it holds for all propositions. (Contributed by Jim Kingdon, 12-May-2018.)
DECID
 
Theorempm2.1dc 719 Commuted law of the excluded middle for a decidable proposition. Based on theorem *2.1 of [WhiteheadRussell] p. 101. (Contributed by Jim Kingdon, 25-Mar-2018.)
DECID
 
Theoremdcn 720 A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.)
DECID DECID
 
Theoremdcbii 721 The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.)
   =>    DECID DECID
 
1.2.8  Theorems of decidable propositions

Many theorems of logic hold in intuitionistic logic just as they do in classical (non-inuitionistic) logic, for all propositions. Other theorems only hold for decidable propositions, such as the law of the excluded middle (df-dc 717), double negation elimination (notnotdc 737), or contraposition (condc 722). Our goal is to prove all well-known or important classical theorems, but with suitable decidability conditions so that the proofs follow from intuitionistic axioms. This section is focused on such proofs, given decidability conditions.

 
Theoremcondc 722 Contraposition of a decidable proposition. (Contributed by Jim Kingdon, 13-Mar-2018.)
DECID
 
Theorempm2.18dc 723 Proof by contradiction for a decidable proposition. Based on Theorem *2.18 of [WhiteheadRussell] p. 103 (also called the Law of Clavius). Intuitionistically it requires a decidability assumption, but compare with pm2.01 529 which does not. (Contributed by Jim Kingdon, 24-Mar-2018.)
DECID
 
Theoremnotnot2dc 724 Double negation elimination for a decidable proposition. (Contributed by Jim Kingdon, 11-Mar-2018.)
DECID
 
Theoremcon1dc 725 Contraposition for a decidable proposition. Based on theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by Jim Kingdon, 29-Mar-2018.)
DECID
 
Theoremimpidc 726 An importation inference for a decidable consequent. (Contributed by Jim Kingdon, 30-Apr-2018.)
DECID    =>    DECID
 
Theoremsimprimdc 727 Simplification given a decidable proposition. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by Jim Kingdon, 30-Apr-2018.)
DECID
 
Theoremsimplimdc 728 Simplification for a decidable proposition. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by Jim Kingdon, 29-Mar-2018.)
DECID
 
Theorempm2.61ddc 729 Deduction eliminating a decidable antecedent. (Contributed by Jim Kingdon, 4-May-2018.)
   &       =>    DECID
 
Theorempm2.6dc 730 Case elimination for a decidable proposition. Based on theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by Jim Kingdon, 25-Mar-2018.)
DECID
 
Theoremjadc 731 Inference forming an implication from the antecedents of two premises, where a decidable antecedent is negated. (Contributed by Jim Kingdon, 25-Mar-2018.)
DECID    &       =>    DECID
 
Theoremjaddc 732 Deduction forming an implication from the antecedents of two premises, where a decidable antecedent is negated. (Contributed by Jim Kingdon, 26-Mar-2018.)
DECID    &       =>    DECID
 
Theorempm2.61dc 733 Case elimination for a decidable proposition. Based on theorem *2.61 of [WhiteheadRussell] p. 107. (Contributed by Jim Kingdon, 29-Mar-2018.)
DECID
 
Theorempm2.5dc 734 Negating an implication for a decidable antecedent. Based on theorem *2.5 of [WhiteheadRussell] p. 107. (Contributed by Jim Kingdon, 29-Mar-2018.)
DECID
 
Theorempm2.521dc 735 Theorem *2.521 of [WhiteheadRussell] p. 107, but with an additional decidability condition. (Contributed by Jim Kingdon, 5-May-2018.)
DECID
 
Theoremcon34bdc 736 Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116, but for a decidable proposition. (Contributed by Jim Kingdon, 24-Apr-2018.)
DECID
 
Theoremnotnotdc 737 Double negation equivalence for a decidable proposition. Like theorem *4.13 of [WhiteheadRussell] p. 117, but with a decidability antecendent. (Contributed by Jim Kingdon, 13-Mar-2018.)
DECID
 
Theoremcon1biimdc 738 Contraposition. (Contributed by Jim Kingdon, 4-Apr-2018.)
DECID
 
Theoremcon1bidc 739 Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.)
DECID DECID
 
Theoremcon2bidc 740 Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.)
DECID DECID
 
Theoremcon1biddc 741 A contraposition deduction. (Contributed by Jim Kingdon, 4-Apr-2018.)
DECID    =>    DECID
 
Theoremcon1biidc 742 A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.)
DECID    =>    DECID
 
Theoremcon1bdc 743 Contraposition. Bidirectional version of con1dc 725. (Contributed by NM, 5-Aug-1993.)
DECID DECID
 
Theoremcon2biidc 744 A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.)
DECID    =>    DECID
 
Theoremcon2biddc 745 A contraposition deduction. (Contributed by Jim Kingdon, 11-Apr-2018.)
DECID    =>    DECID
 
Theoremcondandc 746 Proof by contradiction. This only holds for decidable propositions, as it is part of the family of theorems which assume , derive a contradiction, and therefore conclude . By contrast, assuming , deriving a contradiction, and therefore concluding , as in pm2.65 565, is valid for all propositions. (Contributed by Jim Kingdon, 13-May-2018.)
   &       =>    DECID
 
Theorembijadc 747 Combine antecedents into a single bi-conditional. This inference is reminiscent of jadc 731. (Contributed by Jim Kingdon, 4-May-2018.)
   &       =>    DECID
 
Theorempm5.18dc 748 Relationship between an equivalence and an equivalence with some negation, for decidable propositions. Based on theorem *5.18 of [WhiteheadRussell] p. 124. Given decidability, we can consider to represent "negated exclusive-or". (Contributed by Jim Kingdon, 4-Apr-2018.)
DECID DECID
 
Theoremdfandc 749 Definition of 'and' in terms of negation and implication, for decidable propositions. The forward direction holds for all propositions, and can (basically) be found at pm3.2im 546. (Contributed by Jim Kingdon, 30-Apr-2018.)
DECID DECID
 
Theorempm2.13dc 750 A decidable proposition or its triple negation is true. Theorem *2.13 of [WhiteheadRussell] p. 101 with decidability condition added. (Contributed by Jim Kingdon, 13-May-2018.)
DECID
 
Theorempm4.63dc 751 Theorem *4.63 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.)
DECID DECID
 
Theorempm4.67dc 752 Theorem *4.67 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.)
DECID DECID
 
Theoremannimim 753 Express conjunction in terms of implication. The biconditionalized version of this theorem, annim 1971, is not valid intuitionistically. (Contributed by Jim Kingdon, 24-Dec-2017.)
 
Theoremdcim 754 An implication between two decidable propositions is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.)
DECID DECID DECID
 
Theoremimanim 755 Express implication in terms of conjunction. The converse only holds given a decidability condition; see imandc 756. (Contributed by Jim Kingdon, 24-Dec-2017.)
 
Theoremimandc 756 Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176, with an added decidability condition. The forward direction, imanim 755, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 25-Apr-2018.)
DECID
 
Theorempm4.14dc 757 Theorem *4.14 of [WhiteheadRussell] p. 117, given a decidability condition. (Contributed by Jim Kingdon, 24-Apr-2018.)
DECID
 
Theorempm3.37dc 758 Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112, given a decidability condition. (Contributed by Jim Kingdon, 24-Apr-2018.)
DECID
 
Theorempm4.15 759 Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.)
 
Theorempm2.54dc 760 Deriving disjunction from implication for a decidable proposition. Based on theorem *2.54 of [WhiteheadRussell] p. 107. The converse, pm2.53 618, holds whether the proposition is decidable or not. (Contributed by Jim Kingdon, 26-Mar-2018.)
DECID
 
Theoremdfordc 761 Definition of 'or' in terms of negation and implication for a decidable proposition. Based on definition of [Margaris] p. 49. (Contributed by Jim Kingdon, 26-Mar-2018.)
DECID
 
Theorempm2.25dc 762 Elimination of disjunction based on a disjunction, for a decidable proposition. Based on theorem *2.25 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
DECID
 
Theorempm2.68dc 763 Concluding disjunction from implication for a decidable proposition. Based on theorem *2.68 of [WhiteheadRussell] p. 108. Converse of pm2.62 644 and one half of dfor2dc 764. (Contributed by Jim Kingdon, 27-Mar-2018.)
DECID
 
Theoremdfor2dc 764 Logical 'or' expressed in terms of implication only, for a decidable proposition. Based on theorem *5.25 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 27-Mar-2018.)
DECID
 
Theoremimimorbdc 765 Simplify an implication between implications, for a decidable proposition. (Contributed by Jim Kingdon, 18-Mar-2018.)
DECID
 
Theoremimordc 766 Implication in terms of disjunction for a decidable proposition. Based on theorem *4.6 of [WhiteheadRussell] p. 120. (Contributed by Jim Kingdon, 20-Apr-2018.)
DECID
 
Theorempm4.62dc 767 Implication in terms of disjunction. Like Theorem *4.62 of [WhiteheadRussell] p. 120, but for a decidable antecedent. (Contributed by Jim Kingdon, 21-Apr-2018.)
DECID
 
Theoremianordc 768 Negated conjunction in terms of disjunction (DeMorgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120, but where one proposition is decidable. The reverse direction, pm3.14 647, holds for all propositions, but the equivalence only holds where one proposition is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
DECID
 
Theoremoibabs 769 Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.)
 
Theorempm4.64dc 770 Theorem *4.64 of [WhiteheadRussell] p. 120, given a decidability condition. The reverse direction, pm2.53 618, holds for all propositions. (Contributed by Jim Kingdon, 2-May-2018.)
DECID
 
Theorempm4.66dc 771 Theorem *4.66 of [WhiteheadRussell] p. 120, given a decidability condition. (Contributed by Jim Kingdon, 2-May-2018.)
DECID
 
Theorempm4.54dc 772 Theorem *4.54 of [WhiteheadRussell] p. 120, for decidable propositions. One form of DeMorgan's law. (Contributed by Jim Kingdon, 2-May-2018.)
DECID DECID
 
Theorempm4.56 773 Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.)
 
Theorempm4.78i 774 Implication distributes over disjunction. We do not have an intuitionistic proof of the converse, but both directions hold classically as can be seen at pm4.78 2081. (Contributed by Jim Kingdon, 15-Jan-2018.)
 
Theorempm4.79dc 775 Equivalence between a disjunction of two implications, and a conjunction and an implication. Based on theorem *4.79 of [WhiteheadRussell] p. 121 but with additional decidability antecedents. (Contributed by Jim Kingdon, 28-Mar-2018.)
DECID DECID
 
Theorempm5.17dc 776 Two ways of stating exclusive-or which are equivalent for a decidable proposition. Based on theorem *5.17 of [WhiteheadRussell] p. 124. (Contributed by Jim Kingdon, 16-Apr-2018.)
DECID
 
Theorempm2.85dc 777 Reverse distribution of disjunction over implication, given decidability. Based on theorem *2.85 of [WhiteheadRussell] p. 108. (Contributed by Jim Kingdon, 1-Apr-2018.)
DECID
 
Theoremorimdidc 778 Disjunction distributes over implication. The forward direction, pm2.76 697, is valid intuitionistically. The reverse direction holds if is decidable, as can be seen at pm2.85dc 777. (Contributed by Jim Kingdon, 1-Apr-2018.)
DECID
 
Theorempm2.26dc 779 Decidable proposition version of theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.)
DECID
 
Theorempm5.11dc 780 A decidable proposition or its negation implies a second proposition. Based on theorem *5.11 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 29-Mar-2018.)
DECID DECID
 
Theorempm5.12dc 781 Excluded middle with antecedents for a decidable consequent. Based on theorem *5.12 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
DECID
 
Theorempm5.14dc 782 A decidable proposition is implied by or implies other propositions. Based on theorem *5.14 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
DECID
 
Theorempm5.13dc 783 An implication holds in at least one direction, where one proposition is decidable. Based on theorem *5.13 of [WhiteheadRussell] p. 123. (Contributed by Jim Kingdon, 30-Mar-2018.)
DECID
 
Theorempm5.55dc 784 A disjunction is equivalent to one of its disjuncts, given a decidable disjunct. Based on theorem *5.55 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
DECID
 
1.2.9  Miscellaneous theorems of propositional calculus
 
Theorempm5.21nd 785 Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 20-Nov-2005.) (Proof shortened by Wolf Lammen, 4-Nov-2013.)
   &       &       =>   
 
Theorempm5.35 786 Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theorempm5.54dc 787 A conjunction is equivalent to one of its conjuncts, given a decidable conjunct. Based on theorem *5.54 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 30-Mar-2018.)
DECID
 
Theorembaib 788 Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.)
   =>   
 
Theorembaibr 789 Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.)
   =>   
 
Theorempm5.44 790 Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
 
Theorempm5.6dc 791 Conjunction in antecedent versus disjunction in consequent, for a decidable proposition. Based on theorem *5.6 of [WhiteheadRussell] p. 125. (Contributed by Jim Kingdon, 2-Apr-2018.)
DECID
 
Theoremorcanai 792 Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)
   =>   
 
Theoremintnan 793 Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.)
   =>   
 
Theoremintnanr 794 Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.)
   =>   
 
Theoremintnand 795 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
   =>   
 
Theoremintnanrd 796 Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.)
   =>   
 
Theoremdcan 797 A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
DECID DECID DECID
 
Theoremdcor 798 A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.)
DECID DECID DECID
 
Theoremdcbi 799 An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.)
DECID DECID DECID
 
Theoremannimdc 800 Express conjunction in terms of implication. The forward direction, annimim 753, is valid for all propositions, but as an equivalence, it requires a decidability condition. (Contributed by Jim Kingdon, 25-Apr-2018.)
DECID DECID
    < 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-2000 21 2001-2099
  Copyright terms: Public domain < Previous  Next >