Home | Intuitionistic Logic Explorer Theorem List (p. 8 of 21) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pm2.82 701 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.2ni 702 | Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.) |
Theorem | orabs 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.) |
Theorem | orabsOLD 704 | Obsolete proof of orabs 703 as of 28-Feb-2014. (Contributed by NM, 5-Aug-1993.) |
Theorem | oranabs 705 | Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.) |
Theorem | ordi 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.) |
Theorem | ordir 707 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | andi 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.) |
Theorem | andir 709 | Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | orddi 710 | Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | anddi 711 | Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | pm4.39 712 | Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.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.) |
Theorem | pm5.16 714 | Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | biort 715 | A wff is disjoined with truth is true. (Contributed by NM, 23-May-1999.) |
Syntax | wdc 716 | Extend wff definition to include decidability. |
DECID | ||
Definition | df-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 | ||
Theorem | exmiddc 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 | ||
Theorem | pm2.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 | ||
Theorem | dcn 720 | A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.) |
DECID DECID | ||
Theorem | dcbii 721 | The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.) |
DECID DECID | ||
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. | ||
Theorem | condc 722 | Contraposition of a decidable proposition. (Contributed by Jim Kingdon, 13-Mar-2018.) |
DECID | ||
Theorem | pm2.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 | ||
Theorem | notnot2dc 724 | Double negation elimination for a decidable proposition. (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | con1dc 725 | Contraposition for a decidable proposition. Based on theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by Jim Kingdon, 29-Mar-2018.) |
DECID | ||
Theorem | impidc 726 | An importation inference for a decidable consequent. (Contributed by Jim Kingdon, 30-Apr-2018.) |
DECID DECID | ||
Theorem | simprimdc 727 | Simplification given a decidable proposition. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by Jim Kingdon, 30-Apr-2018.) |
DECID | ||
Theorem | simplimdc 728 | Simplification for a decidable proposition. Similar to Theorem *3.26 (Simp) of [WhiteheadRussell] p. 112. (Contributed by Jim Kingdon, 29-Mar-2018.) |
DECID | ||
Theorem | pm2.61ddc 729 | Deduction eliminating a decidable antecedent. (Contributed by Jim Kingdon, 4-May-2018.) |
DECID | ||
Theorem | pm2.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 | ||
Theorem | jadc 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 | ||
Theorem | jaddc 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 | ||
Theorem | pm2.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 | ||
Theorem | pm2.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 | ||
Theorem | pm2.521dc 735 | Theorem *2.521 of [WhiteheadRussell] p. 107, but with an additional decidability condition. (Contributed by Jim Kingdon, 5-May-2018.) |
DECID | ||
Theorem | con34bdc 736 | Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116, but for a decidable proposition. (Contributed by Jim Kingdon, 24-Apr-2018.) |
DECID | ||
Theorem | notnotdc 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 | ||
Theorem | con1biimdc 738 | Contraposition. (Contributed by Jim Kingdon, 4-Apr-2018.) |
DECID | ||
Theorem | con1bidc 739 | Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.) |
DECID DECID | ||
Theorem | con2bidc 740 | Contraposition. (Contributed by Jim Kingdon, 17-Apr-2018.) |
DECID DECID | ||
Theorem | con1biddc 741 | A contraposition deduction. (Contributed by Jim Kingdon, 4-Apr-2018.) |
DECID DECID | ||
Theorem | con1biidc 742 | A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.) |
DECID DECID | ||
Theorem | con1bdc 743 | Contraposition. Bidirectional version of con1dc 725. (Contributed by NM, 5-Aug-1993.) |
DECID DECID | ||
Theorem | con2biidc 744 | A contraposition inference. (Contributed by Jim Kingdon, 15-Mar-2018.) |
DECID DECID | ||
Theorem | con2biddc 745 | A contraposition deduction. (Contributed by Jim Kingdon, 11-Apr-2018.) |
DECID DECID | ||
Theorem | condandc 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 | ||
Theorem | bijadc 747 | Combine antecedents into a single bi-conditional. This inference is reminiscent of jadc 731. (Contributed by Jim Kingdon, 4-May-2018.) |
DECID | ||
Theorem | pm5.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 | ||
Theorem | dfandc 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 | ||
Theorem | pm2.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 | ||
Theorem | pm4.63dc 751 | Theorem *4.63 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.) |
DECID DECID | ||
Theorem | pm4.67dc 752 | Theorem *4.67 of [WhiteheadRussell] p. 120, for decidable propositions. (Contributed by Jim Kingdon, 1-May-2018.) |
DECID DECID | ||
Theorem | annimim 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.) |
Theorem | dcim 754 | An implication between two decidable propositions is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.) |
DECID DECID DECID | ||
Theorem | imanim 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.) |
Theorem | imandc 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 | ||
Theorem | pm4.14dc 757 | Theorem *4.14 of [WhiteheadRussell] p. 117, given a decidability condition. (Contributed by Jim Kingdon, 24-Apr-2018.) |
DECID | ||
Theorem | pm3.37dc 758 | Theorem *3.37 (Transp) of [WhiteheadRussell] p. 112, given a decidability condition. (Contributed by Jim Kingdon, 24-Apr-2018.) |
DECID | ||
Theorem | pm4.15 759 | Theorem *4.15 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
Theorem | pm2.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 | ||
Theorem | dfordc 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 | ||
Theorem | pm2.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 | ||
Theorem | pm2.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 | ||
Theorem | dfor2dc 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 | ||
Theorem | imimorbdc 765 | Simplify an implication between implications, for a decidable proposition. (Contributed by Jim Kingdon, 18-Mar-2018.) |
DECID | ||
Theorem | imordc 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 | ||
Theorem | pm4.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 | ||
Theorem | ianordc 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 | ||
Theorem | oibabs 769 | Absorption of disjunction into equivalence. (Contributed by NM, 6-Aug-1995.) (Proof shortened by Wolf Lammen, 3-Nov-2013.) |
Theorem | pm4.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 | ||
Theorem | pm4.66dc 771 | Theorem *4.66 of [WhiteheadRussell] p. 120, given a decidability condition. (Contributed by Jim Kingdon, 2-May-2018.) |
DECID | ||
Theorem | pm4.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 | ||
Theorem | pm4.56 773 | Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.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.) |
Theorem | pm4.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 | ||
Theorem | pm5.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 | ||
Theorem | pm2.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 | ||
Theorem | orimdidc 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 | ||
Theorem | pm2.26dc 779 | Decidable proposition version of theorem *2.26 of [WhiteheadRussell] p. 104. (Contributed by Jim Kingdon, 20-Apr-2018.) |
DECID | ||
Theorem | pm5.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 | ||
Theorem | pm5.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 | ||
Theorem | pm5.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 | ||
Theorem | pm5.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 | ||
Theorem | pm5.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 | ||
Theorem | pm5.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.) |
Theorem | pm5.35 786 | Theorem *5.35 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm5.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 | ||
Theorem | baib 788 | Move conjunction outside of biconditional. (Contributed by NM, 13-May-1999.) |
Theorem | baibr 789 | Move conjunction outside of biconditional. (Contributed by NM, 11-Jul-1994.) |
Theorem | pm5.44 790 | Theorem *5.44 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm5.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 | ||
Theorem | orcanai 792 | Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.) |
Theorem | intnan 793 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 16-Sep-1993.) |
Theorem | intnanr 794 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 3-Apr-1995.) |
Theorem | intnand 795 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
Theorem | intnanrd 796 | Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
Theorem | dcan 797 | A conjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) |
DECID DECID DECID | ||
Theorem | dcor 798 | A disjunction of two decidable propositions is decidable. (Contributed by Jim Kingdon, 21-Apr-2018.) |
DECID DECID DECID | ||
Theorem | dcbi 799 | An equivalence of two decidable propositions is decidable. (Contributed by Jim Kingdon, 12-Apr-2018.) |
DECID DECID DECID | ||
Theorem | annimdc 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 > |
Copyright terms: Public domain | < Previous Next > |