Home | Intuitionistic Logic Explorer Theorem List (p. 8 of 108) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ioran 701 | Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 840, anordc 897, or ianordc 832. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm3.14 702 | Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 832. The converse holds for decidable propositions, as seen at pm3.13dc 900. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm3.1 703 | Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 897. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | jao 704 | Disjunction of antecedents. Compare Theorem *3.44 of [WhiteheadRussell] p. 113. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 4-Apr-2013.) |
Theorem | pm1.2 705 | Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 10-Mar-2013.) |
Theorem | oridm 706 | Idempotent law for disjunction. Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 16-Apr-2011.) (Proof shortened by Wolf Lammen, 10-Mar-2013.) |
Theorem | pm4.25 707 | Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) |
Theorem | orim12i 708 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
Theorem | orim1i 709 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Theorem | orim2i 710 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Theorem | orbi2i 711 | Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
Theorem | orbi1i 712 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Theorem | orbi12i 713 | Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Theorem | pm1.5 714 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
Theorem | or12 715 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
Theorem | orass 716 | Associative law for disjunction. Theorem *4.33 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | pm2.31 717 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.32 718 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
Theorem | or32 719 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | or4 720 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
Theorem | or42 721 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
Theorem | orordi 722 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
Theorem | orordir 723 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
Theorem | pm2.3 724 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.41 725 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.42 726 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.4 727 | Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.44 728 | Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
Theorem | mtord 729 | A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm4.45 730 | Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.48 731 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) (Revised by NM, 1-Dec-2012.) |
Theorem | orim12d 732 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.) |
Theorem | orim1d 733 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Theorem | orim2d 734 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Theorem | orim2 735 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
Theorem | orbi2d 736 | Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | orbi1d 737 | Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Theorem | orbi1 738 | Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
Theorem | orbi12d 739 | Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.) |
Theorem | pm5.61 740 | Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.) |
Theorem | jaoian 741 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
Theorem | jao1i 742 | Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.) |
Theorem | jaodan 743 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
Theorem | mpjaodan 744 | Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | pm4.77 745 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.63 746 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.64 747 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm5.53 748 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.38 749 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.36 750 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.37 751 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.73 752 | Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.74 753 | Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm2.76 754 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm2.75 755 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
Theorem | pm2.8 756 | Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm2.81 757 | Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.82 758 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.2ni 759 | Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.) |
Theorem | orabs 760 | 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 | oranabs 761 | Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.) |
Theorem | ordi 762 | 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 763 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | andi 764 | 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 765 | Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | orddi 766 | Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | anddi 767 | Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | pm4.39 768 | Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.72 769 | 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 770 | Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | biort 771 | A wff is disjoined with truth is true. (Contributed by NM, 23-May-1999.) |
Syntax | wstab 772 | Extend wff definition to include stability. |
STAB | ||
Definition | df-stab 773 |
Propositions where a double-negative can be removed are called stable.
See Chapter 2 [Moschovakis] p. 2.
Our notation for stability is a connective STAB which we place before the formula in question. For example, STAB corresponds to "x = y is stable". (Contributed by David A. Wheeler, 13-Aug-2018.) |
STAB | ||
Theorem | stabnot 774 | Every formula of the form is stable. Uses notnotnot 660. (Contributed by David A. Wheeler, 13-Aug-2018.) |
STAB | ||
Syntax | wdc 775 | Extend wff definition to include decidability. |
DECID | ||
Definition | df-dc 776 |
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". We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 782, exmiddc 777, peircedc 853, or notnotrdc 784, any of which would correspond to the assertion that all propositions are decidable. (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | exmiddc 777 | 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 778 | 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 779 | A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.) |
DECID DECID | ||
Theorem | dcbii 780 | The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.) |
DECID DECID | ||
Theorem | dcbid 781 | The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.) |
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 776), double negation elimination (notnotrdc 784), or contraposition (condc 782). 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 782 |
Contraposition of a decidable proposition.
This theorem swaps or "transposes" the order of the consequents when negation is removed. An informal example is that the statement "if there are no clouds in the sky, it is not raining" implies the statement "if it is raining, there are clouds in the sky." This theorem (without the decidability condition, of course) is called Transp or "the principle of transposition" in Principia Mathematica (Theorem *2.17 of [WhiteheadRussell] p. 103) and is Axiom A3 of [Margaris] p. 49. We will also use the term "contraposition" for this principle, although the reader is advised that in the field of philosophical logic, "contraposition" has a different technical meaning. (Contributed by Jim Kingdon, 13-Mar-2018.) |
DECID | ||
Theorem | pm2.18dc 783 | 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 578 which does not. (Contributed by Jim Kingdon, 24-Mar-2018.) |
DECID | ||
Theorem | notnotrdc 784 | Double negation elimination for a decidable proposition. The converse, notnot 591, holds for all propositions, not just decidable ones. This is Theorem *2.14 of [WhiteheadRussell] p. 102, but with a decidability condition added. (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | dcimpstab 785 | Decidability implies stability. The converse is not necessarily true. (Contributed by David A. Wheeler, 13-Aug-2018.) |
DECID STAB | ||
Theorem | con1dc 786 | Contraposition for a decidable proposition. Based on theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by Jim Kingdon, 29-Mar-2018.) |
DECID | ||
Theorem | con4biddc 787 | A contraposition deduction. (Contributed by Jim Kingdon, 18-May-2018.) |
DECID DECID DECID DECID | ||
Theorem | impidc 788 | An importation inference for a decidable consequent. (Contributed by Jim Kingdon, 30-Apr-2018.) |
DECID DECID | ||
Theorem | simprimdc 789 | 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 790 | 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 791 | Deduction eliminating a decidable antecedent. (Contributed by Jim Kingdon, 4-May-2018.) |
DECID | ||
Theorem | pm2.6dc 792 | 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 793 | 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 794 | 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 795 | 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 796 | 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 797 | Theorem *2.521 of [WhiteheadRussell] p. 107, but with an additional decidability condition. (Contributed by Jim Kingdon, 5-May-2018.) |
DECID | ||
Theorem | con34bdc 798 | Contraposition. Theorem *4.1 of [WhiteheadRussell] p. 116, but for a decidable proposition. (Contributed by Jim Kingdon, 24-Apr-2018.) |
DECID | ||
Theorem | notnotbdc 799 | Double negation equivalence for a decidable proposition. Like Theorem *4.13 of [WhiteheadRussell] p. 117, but with a decidability antecendent. The forward direction, notnot 591, holds for all propositions, not just decidable ones. (Contributed by Jim Kingdon, 13-Mar-2018.) |
DECID | ||
Theorem | con1biimdc 800 | Contraposition. (Contributed by Jim Kingdon, 4-Apr-2018.) |
DECID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |