Home | Intuitionistic Logic Explorer Theorem List (p. 8 of 129) | < 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 | pm2.48 701 | Theorem *2.48 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.49 702 | Theorem *2.49 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.67 703 | Theorem *2.67 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 9-Dec-2012.) |
Theorem | biorf 704 | A wff is equivalent to its disjunction with falsehood. Theorem *4.74 of [WhiteheadRussell] p. 121. (Contributed by NM, 23-Mar-1995.) (Proof shortened by Wolf Lammen, 18-Nov-2012.) |
Theorem | biortn 705 | A wff is equivalent to its negated disjunction with falsehood. (Contributed by NM, 9-Jul-2012.) |
Theorem | biorfi 706 | A wff is equivalent to its disjunction with falsehood. (Contributed by NM, 23-Mar-1995.) |
Theorem | pm2.621 707 | Theorem *2.621 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 13-Dec-2013.) |
Theorem | pm2.62 708 | Theorem *2.62 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 13-Dec-2013.) |
Theorem | imorri 709 | Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | ioran 710 | Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 851, anordc 908, or ianordc 843. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm3.14 711 | Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 843. The converse holds for decidable propositions, as seen at pm3.13dc 911. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm3.1 712 | Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 908. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | jao 713 | 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 714 | Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 10-Mar-2013.) |
Theorem | oridm 715 | 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 716 | Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.) |
Theorem | orim12i 717 | Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
Theorem | orim1i 718 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Theorem | orim2i 719 | Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Theorem | orbi2i 720 | 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 721 | Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Theorem | orbi12i 722 | Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.) |
Theorem | pm1.5 723 | Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) |
Theorem | or12 724 | Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.) |
Theorem | orass 725 | 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 726 | Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.32 727 | Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.) |
Theorem | or32 728 | A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Theorem | or4 729 | Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.) |
Theorem | or42 730 | Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.) |
Theorem | orordi 731 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
Theorem | orordir 732 | Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.) |
Theorem | pm2.3 733 | Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.41 734 | Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.42 735 | Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.4 736 | Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.44 737 | Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
Theorem | mtord 738 | A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm4.45 739 | Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.48 740 | Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) (Revised by NM, 1-Dec-2012.) |
Theorem | orim12d 741 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.) |
Theorem | orim1d 742 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Theorem | orim2d 743 | Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.) |
Theorem | orim2 744 | Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.) |
Theorem | orbi2d 745 | 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 746 | Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) |
Theorem | orbi1 747 | Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
Theorem | orbi12d 748 | Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.) |
Theorem | pm5.61 749 | Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.) |
Theorem | jaoian 750 | Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.) |
Theorem | jao1i 751 | Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.) |
Theorem | jaodan 752 | Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.) |
Theorem | mpjaodan 753 | Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination). (Contributed by Mario Carneiro, 29-May-2016.) |
Theorem | pm4.77 754 | Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.63 755 | Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.64 756 | Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm5.53 757 | Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.38 758 | Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.36 759 | Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.37 760 | Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.) |
Theorem | pm2.73 761 | Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.74 762 | Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm2.76 763 | Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm2.75 764 | Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.) |
Theorem | pm2.8 765 | Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.) |
Theorem | pm2.81 766 | Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm2.82 767 | Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm3.2ni 768 | Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.) |
Theorem | orabs 769 | 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 770 | Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.) |
Theorem | ordi 771 | 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 772 | Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | andi 773 | 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 774 | Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | orddi 775 | Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | anddi 776 | Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.) |
Theorem | pm4.39 777 | Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.) |
Theorem | pm4.72 778 | 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 779 | Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Theorem | biort 780 | A wff is disjoined with truth is true. (Contributed by NM, 23-May-1999.) |
Syntax | wstab 781 | Extend wff definition to include stability. |
STAB | ||
Definition | df-stab 782 |
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 | stbid 783 | The equivalent of a stable proposition is stable. (Contributed by Jim Kingdon, 12-Aug-2022.) |
STAB STAB | ||
Theorem | stabnot 784 | Every formula of the form is stable. Uses notnotnot 669. (Contributed by David A. Wheeler, 13-Aug-2018.) |
STAB | ||
Theorem | imanst 785 | Express implication in terms of conjunction. Theorem 3.4(27) of [Stoll] p. 176. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Wolf Lammen, 30-Oct-2012.) |
STAB | ||
Syntax | wdc 786 | Extend wff definition to include decidability. |
DECID | ||
Definition | df-dc 787 |
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 793, exmiddc 788, peircedc 864, or notnotrdc 795, any of which would correspond to the assertion that all propositions are decidable. (Contributed by Jim Kingdon, 11-Mar-2018.) |
DECID | ||
Theorem | exmiddc 788 | 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 789 | 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 790 | A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.) |
DECID DECID | ||
Theorem | dcbii 791 | The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.) |
DECID DECID | ||
Theorem | dcbid 792 | 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 787), double negation elimination (notnotrdc 795), or contraposition (condc 793). 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 793 |
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 794 | 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 586 which does not. (Contributed by Jim Kingdon, 24-Mar-2018.) |
DECID | ||
Theorem | notnotrdc 795 | Double negation elimination for a decidable proposition. The converse, notnot 599, 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 796 | Decidability implies stability. The converse is not necessarily true. (Contributed by David A. Wheeler, 13-Aug-2018.) |
DECID STAB | ||
Theorem | con1dc 797 | Contraposition for a decidable proposition. Based on theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by Jim Kingdon, 29-Mar-2018.) |
DECID | ||
Theorem | con4biddc 798 | A contraposition deduction. (Contributed by Jim Kingdon, 18-May-2018.) |
DECID DECID DECID DECID | ||
Theorem | impidc 799 | An importation inference for a decidable consequent. (Contributed by Jim Kingdon, 30-Apr-2018.) |
DECID DECID | ||
Theorem | simprimdc 800 | Simplification given a decidable proposition. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by Jim Kingdon, 30-Apr-2018.) |
DECID |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |