HomeHome Intuitionistic Logic Explorer
Theorem List (p. 8 of 114)
< Previous  Next >
Bad symbols? Try the
GIF version.

Mirrors  >  Metamath Home Page  >  ILE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Intuitionistic Logic Explorer - 701-800   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremimorri 701 Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (Revised by Mario Carneiro, 31-Jan-2015.)
𝜑𝜓)       (𝜑𝜓)
 
Theoremioran 702 Negated disjunction in terms of conjunction. This version of DeMorgan's law is a biconditional for all propositions (not just decidable ones), unlike oranim 843, anordc 900, or ianordc 835. Compare Theorem *4.56 of [WhiteheadRussell] p. 120. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)
(¬ (𝜑𝜓) ↔ (¬ 𝜑 ∧ ¬ 𝜓))
 
Theorempm3.14 703 Theorem *3.14 of [WhiteheadRussell] p. 111. One direction of De Morgan's law). The biconditional holds for decidable propositions as seen at ianordc 835. The converse holds for decidable propositions, as seen at pm3.13dc 903. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
((¬ 𝜑 ∨ ¬ 𝜓) → ¬ (𝜑𝜓))
 
Theorempm3.1 704 Theorem *3.1 of [WhiteheadRussell] p. 111. The converse holds for decidable propositions, as seen at anordc 900. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
((𝜑𝜓) → ¬ (¬ 𝜑 ∨ ¬ 𝜓))
 
Theoremjao 705 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.)
((𝜑𝜓) → ((𝜒𝜓) → ((𝜑𝜒) → 𝜓)))
 
Theorempm1.2 706 Axiom *1.2 (Taut) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.) (Revised by NM, 10-Mar-2013.)
((𝜑𝜑) → 𝜑)
 
Theoremoridm 707 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.)
((𝜑𝜑) ↔ 𝜑)
 
Theorempm4.25 708 Theorem *4.25 of [WhiteheadRussell] p. 117. (Contributed by NM, 3-Jan-2005.)
(𝜑 ↔ (𝜑𝜑))
 
Theoremorim12i 709 Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)
(𝜑𝜓)    &   (𝜒𝜃)       ((𝜑𝜒) → (𝜓𝜃))
 
Theoremorim1i 710 Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
(𝜑𝜓)       ((𝜑𝜒) → (𝜓𝜒))
 
Theoremorim2i 711 Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
(𝜑𝜓)       ((𝜒𝜑) → (𝜒𝜓))
 
Theoremorbi2i 712 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.)
(𝜑𝜓)       ((𝜒𝜑) ↔ (𝜒𝜓))
 
Theoremorbi1i 713 Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
(𝜑𝜓)       ((𝜑𝜒) ↔ (𝜓𝜒))
 
Theoremorbi12i 714 Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)
(𝜑𝜓)    &   (𝜒𝜃)       ((𝜑𝜒) ↔ (𝜓𝜃))
 
Theorempm1.5 715 Axiom *1.5 (Assoc) of [WhiteheadRussell] p. 96. (Contributed by NM, 3-Jan-2005.)
((𝜑 ∨ (𝜓𝜒)) → (𝜓 ∨ (𝜑𝜒)))
 
Theoremor12 716 Swap two disjuncts. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Nov-2012.)
((𝜑 ∨ (𝜓𝜒)) ↔ (𝜓 ∨ (𝜑𝜒)))
 
Theoremorass 717 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.)
(((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
 
Theorempm2.31 718 Theorem *2.31 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
((𝜑 ∨ (𝜓𝜒)) → ((𝜑𝜓) ∨ 𝜒))
 
Theorempm2.32 719 Theorem *2.32 of [WhiteheadRussell] p. 105. (Contributed by NM, 3-Jan-2005.)
(((𝜑𝜓) ∨ 𝜒) → (𝜑 ∨ (𝜓𝜒)))
 
Theoremor32 720 A rearrangement of disjuncts. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)
(((𝜑𝜓) ∨ 𝜒) ↔ ((𝜑𝜒) ∨ 𝜓))
 
Theoremor4 721 Rearrangement of 4 disjuncts. (Contributed by NM, 12-Aug-1994.)
(((𝜑𝜓) ∨ (𝜒𝜃)) ↔ ((𝜑𝜒) ∨ (𝜓𝜃)))
 
Theoremor42 722 Rearrangement of 4 disjuncts. (Contributed by NM, 10-Jan-2005.)
(((𝜑𝜓) ∨ (𝜒𝜃)) ↔ ((𝜑𝜒) ∨ (𝜃𝜓)))
 
Theoremorordi 723 Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
((𝜑 ∨ (𝜓𝜒)) ↔ ((𝜑𝜓) ∨ (𝜑𝜒)))
 
Theoremorordir 724 Distribution of disjunction over disjunction. (Contributed by NM, 25-Feb-1995.)
(((𝜑𝜓) ∨ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
 
Theorempm2.3 725 Theorem *2.3 of [WhiteheadRussell] p. 104. (Contributed by NM, 3-Jan-2005.)
((𝜑 ∨ (𝜓𝜒)) → (𝜑 ∨ (𝜒𝜓)))
 
Theorempm2.41 726 Theorem *2.41 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
((𝜓 ∨ (𝜑𝜓)) → (𝜑𝜓))
 
Theorempm2.42 727 Theorem *2.42 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
((¬ 𝜑 ∨ (𝜑𝜓)) → (𝜑𝜓))
 
Theorempm2.4 728 Theorem *2.4 of [WhiteheadRussell] p. 106. (Contributed by NM, 3-Jan-2005.)
((𝜑 ∨ (𝜑𝜓)) → (𝜑𝜓))
 
Theorempm4.44 729 Theorem *4.44 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
(𝜑 ↔ (𝜑 ∨ (𝜑𝜓)))
 
Theoremmtord 730 A modus tollens deduction involving disjunction. (Contributed by Jeff Hankins, 15-Jul-2009.) (Revised by Mario Carneiro, 31-Jan-2015.)
(𝜑 → ¬ 𝜒)    &   (𝜑 → ¬ 𝜃)    &   (𝜑 → (𝜓 → (𝜒𝜃)))       (𝜑 → ¬ 𝜓)
 
Theorempm4.45 731 Theorem *4.45 of [WhiteheadRussell] p. 119. (Contributed by NM, 3-Jan-2005.)
(𝜑 ↔ (𝜑 ∧ (𝜑𝜓)))
 
Theorempm3.48 732 Theorem *3.48 of [WhiteheadRussell] p. 114. (Contributed by NM, 28-Jan-1997.) (Revised by NM, 1-Dec-2012.)
(((𝜑𝜓) ∧ (𝜒𝜃)) → ((𝜑𝜒) → (𝜓𝜃)))
 
Theoremorim12d 733 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 10-May-1994.)
(𝜑 → (𝜓𝜒))    &   (𝜑 → (𝜃𝜏))       (𝜑 → ((𝜓𝜃) → (𝜒𝜏)))
 
Theoremorim1d 734 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
(𝜑 → (𝜓𝜒))       (𝜑 → ((𝜓𝜃) → (𝜒𝜃)))
 
Theoremorim2d 735 Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)
(𝜑 → (𝜓𝜒))       (𝜑 → ((𝜃𝜓) → (𝜃𝜒)))
 
Theoremorim2 736 Axiom *1.6 (Sum) of [WhiteheadRussell] p. 97. (Contributed by NM, 3-Jan-2005.)
((𝜓𝜒) → ((𝜑𝜓) → (𝜑𝜒)))
 
Theoremorbi2d 737 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.)
(𝜑 → (𝜓𝜒))       (𝜑 → ((𝜃𝜓) ↔ (𝜃𝜒)))
 
Theoremorbi1d 738 Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)
(𝜑 → (𝜓𝜒))       (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜃)))
 
Theoremorbi1 739 Theorem *4.37 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
 
Theoremorbi12d 740 Deduction joining two equivalences to form equivalence of disjunctions. (Contributed by NM, 5-Aug-1993.)
(𝜑 → (𝜓𝜒))    &   (𝜑 → (𝜃𝜏))       (𝜑 → ((𝜓𝜃) ↔ (𝜒𝜏)))
 
Theorempm5.61 741 Theorem *5.61 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 30-Jun-2013.)
(((𝜑𝜓) ∧ ¬ 𝜓) ↔ (𝜑 ∧ ¬ 𝜓))
 
Theoremjaoian 742 Inference disjoining the antecedents of two implications. (Contributed by NM, 23-Oct-2005.)
((𝜑𝜓) → 𝜒)    &   ((𝜃𝜓) → 𝜒)       (((𝜑𝜃) ∧ 𝜓) → 𝜒)
 
Theoremjao1i 743 Add a disjunct in the antecedent of an implication. (Contributed by Rodolfo Medina, 24-Sep-2010.)
(𝜓 → (𝜒𝜑))       ((𝜑𝜓) → (𝜒𝜑))
 
Theoremjaodan 744 Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)
((𝜑𝜓) → 𝜒)    &   ((𝜑𝜃) → 𝜒)       ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
 
Theoremmpjaodan 745 Eliminate a disjunction in a deduction. A translation of natural deduction rule E ( elimination). (Contributed by Mario Carneiro, 29-May-2016.)
((𝜑𝜓) → 𝜒)    &   ((𝜑𝜃) → 𝜒)    &   (𝜑 → (𝜓𝜃))       (𝜑𝜒)
 
Theorempm4.77 746 Theorem *4.77 of [WhiteheadRussell] p. 121. (Contributed by NM, 3-Jan-2005.)
(((𝜓𝜑) ∧ (𝜒𝜑)) ↔ ((𝜓𝜒) → 𝜑))
 
Theorempm2.63 747 Theorem *2.63 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
((𝜑𝜓) → ((¬ 𝜑𝜓) → 𝜓))
 
Theorempm2.64 748 Theorem *2.64 of [WhiteheadRussell] p. 107. (Contributed by NM, 3-Jan-2005.)
((𝜑𝜓) → ((𝜑 ∨ ¬ 𝜓) → 𝜑))
 
Theorempm5.53 749 Theorem *5.53 of [WhiteheadRussell] p. 125. (Contributed by NM, 3-Jan-2005.)
((((𝜑𝜓) ∨ 𝜒) → 𝜃) ↔ (((𝜑𝜃) ∧ (𝜓𝜃)) ∧ (𝜒𝜃)))
 
Theorempm2.38 750 Theorem *2.38 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
((𝜓𝜒) → ((𝜓𝜑) → (𝜒𝜑)))
 
Theorempm2.36 751 Theorem *2.36 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
((𝜓𝜒) → ((𝜑𝜓) → (𝜒𝜑)))
 
Theorempm2.37 752 Theorem *2.37 of [WhiteheadRussell] p. 105. (Contributed by NM, 6-Mar-2008.)
((𝜓𝜒) → ((𝜓𝜑) → (𝜑𝜒)))
 
Theorempm2.73 753 Theorem *2.73 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
((𝜑𝜓) → (((𝜑𝜓) ∨ 𝜒) → (𝜓𝜒)))
 
Theorempm2.74 754 Theorem *2.74 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
((𝜓𝜑) → (((𝜑𝜓) ∨ 𝜒) → (𝜑𝜒)))
 
Theorempm2.76 755 Theorem *2.76 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
((𝜑 ∨ (𝜓𝜒)) → ((𝜑𝜓) → (𝜑𝜒)))
 
Theorempm2.75 756 Theorem *2.75 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 4-Jan-2013.)
((𝜑𝜓) → ((𝜑 ∨ (𝜓𝜒)) → (𝜑𝜒)))
 
Theorempm2.8 757 Theorem *2.8 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.) (Proof shortened by Mario Carneiro, 31-Jan-2015.)
((𝜑𝜓) → ((¬ 𝜓𝜒) → (𝜑𝜒)))
 
Theorempm2.81 758 Theorem *2.81 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
((𝜓 → (𝜒𝜃)) → ((𝜑𝜓) → ((𝜑𝜒) → (𝜑𝜃))))
 
Theorempm2.82 759 Theorem *2.82 of [WhiteheadRussell] p. 108. (Contributed by NM, 3-Jan-2005.)
(((𝜑𝜓) ∨ 𝜒) → (((𝜑 ∨ ¬ 𝜒) ∨ 𝜃) → ((𝜑𝜓) ∨ 𝜃)))
 
Theorempm3.2ni 760 Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
¬ 𝜑    &    ¬ 𝜓        ¬ (𝜑𝜓)
 
Theoremorabs 761 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.)
(𝜑 ↔ ((𝜑𝜓) ∧ 𝜑))
 
Theoremoranabs 762 Absorb a disjunct into a conjunct. (Contributed by Roy F. Longton, 23-Jun-2005.) (Proof shortened by Wolf Lammen, 10-Nov-2013.)
(((𝜑 ∨ ¬ 𝜓) ∧ 𝜓) ↔ (𝜑𝜓))
 
Theoremordi 763 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 764 Distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
(((𝜑𝜓) ∨ 𝜒) ↔ ((𝜑𝜒) ∧ (𝜓𝜒)))
 
Theoremandi 765 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 766 Distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
(((𝜑𝜓) ∧ 𝜒) ↔ ((𝜑𝜒) ∨ (𝜓𝜒)))
 
Theoremorddi 767 Double distributive law for disjunction. (Contributed by NM, 12-Aug-1994.)
(((𝜑𝜓) ∨ (𝜒𝜃)) ↔ (((𝜑𝜒) ∧ (𝜑𝜃)) ∧ ((𝜓𝜒) ∧ (𝜓𝜃))))
 
Theoremanddi 768 Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)
(((𝜑𝜓) ∧ (𝜒𝜃)) ↔ (((𝜑𝜒) ∨ (𝜑𝜃)) ∨ ((𝜓𝜒) ∨ (𝜓𝜃))))
 
Theorempm4.39 769 Theorem *4.39 of [WhiteheadRussell] p. 118. (Contributed by NM, 3-Jan-2005.)
(((𝜑𝜒) ∧ (𝜓𝜃)) → ((𝜑𝜓) ↔ (𝜒𝜃)))
 
Theorempm4.72 770 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 771 Theorem *5.16 of [WhiteheadRussell] p. 124. (Contributed by NM, 3-Jan-2005.) (Revised by Mario Carneiro, 31-Jan-2015.)
¬ ((𝜑𝜓) ∧ (𝜑 ↔ ¬ 𝜓))
 
Theorembiort 772 A wff is disjoined with truth is true. (Contributed by NM, 23-May-1999.)
(𝜑 → (𝜑 ↔ (𝜑𝜓)))
 
1.2.7  Stable propositions
 
Syntaxwstab 773 Extend wff definition to include stability.
wff STAB 𝜑
 
Definitiondf-stab 774 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 𝜑 ↔ (¬ ¬ 𝜑𝜑))
 
Theoremstbid 775 The equivalent of a stable proposition is stable. (Contributed by Jim Kingdon, 12-Aug-2022.)
(𝜑 → (𝜓𝜒))       (𝜑 → (STAB 𝜓STAB 𝜒))
 
Theoremstabnot 776 Every formula of the form ¬ 𝜑 is stable. Uses notnotnot 661. (Contributed by David A. Wheeler, 13-Aug-2018.)
STAB ¬ 𝜑
 
Theoremimanst 777 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 𝜓 → ((𝜑𝜓) ↔ ¬ (𝜑 ∧ ¬ 𝜓)))
 
1.2.8  Decidable propositions
 
Syntaxwdc 778 Extend wff definition to include decidability.
wff DECID 𝜑
 
Definitiondf-dc 779 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 785, exmiddc 780, peircedc 856, or notnotrdc 787, any of which would correspond to the assertion that all propositions are decidable.

(Contributed by Jim Kingdon, 11-Mar-2018.)

(DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
 
Theoremexmiddc 780 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 781 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 782 A decidable proposition is decidable when negated. (Contributed by Jim Kingdon, 25-Mar-2018.)
(DECID 𝜑DECID ¬ 𝜑)
 
Theoremdcbii 783 The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 28-Mar-2018.)
(𝜑𝜓)       (DECID 𝜑DECID 𝜓)
 
Theoremdcbid 784 The equivalent of a decidable proposition is decidable. (Contributed by Jim Kingdon, 7-Sep-2019.)
(𝜑 → (𝜓𝜒))       (𝜑 → (DECID 𝜓DECID 𝜒))
 
1.2.9  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 779), double negation elimination (notnotrdc 787), or contraposition (condc 785). 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 785 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 𝜑 → ((¬ 𝜑 → ¬ 𝜓) → (𝜓𝜑)))
 
Theorempm2.18dc 786 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 579 which does not. (Contributed by Jim Kingdon, 24-Mar-2018.)
(DECID 𝜑 → ((¬ 𝜑𝜑) → 𝜑))
 
Theoremnotnotrdc 787 Double negation elimination for a decidable proposition. The converse, notnot 592, 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 𝜑 → (¬ ¬ 𝜑𝜑))
 
Theoremdcimpstab 788 Decidability implies stability. The converse is not necessarily true. (Contributed by David A. Wheeler, 13-Aug-2018.)
(DECID 𝜑STAB 𝜑)
 
Theoremcon1dc 789 Contraposition for a decidable proposition. Based on theorem *2.15 of [WhiteheadRussell] p. 102. (Contributed by Jim Kingdon, 29-Mar-2018.)
(DECID 𝜑 → ((¬ 𝜑𝜓) → (¬ 𝜓𝜑)))
 
Theoremcon4biddc 790 A contraposition deduction. (Contributed by Jim Kingdon, 18-May-2018.)
(𝜑 → (DECID 𝜓 → (DECID 𝜒 → (¬ 𝜓 ↔ ¬ 𝜒))))       (𝜑 → (DECID 𝜓 → (DECID 𝜒 → (𝜓𝜒))))
 
Theoremimpidc 791 An importation inference for a decidable consequent. (Contributed by Jim Kingdon, 30-Apr-2018.)
(DECID 𝜒 → (𝜑 → (𝜓𝜒)))       (DECID 𝜒 → (¬ (𝜑 → ¬ 𝜓) → 𝜒))
 
Theoremsimprimdc 792 Simplification given a decidable proposition. Similar to Theorem *3.27 (Simp) of [WhiteheadRussell] p. 112. (Contributed by Jim Kingdon, 30-Apr-2018.)
(DECID 𝜓 → (¬ (𝜑 → ¬ 𝜓) → 𝜓))
 
Theoremsimplimdc 793 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 794 Deduction eliminating a decidable antecedent. (Contributed by Jim Kingdon, 4-May-2018.)
(𝜑 → (𝜓𝜒))    &   (𝜑 → (¬ 𝜓𝜒))       (DECID 𝜓 → (𝜑𝜒))
 
Theorempm2.6dc 795 Case elimination for a decidable proposition. Based on theorem *2.6 of [WhiteheadRussell] p. 107. (Contributed by Jim Kingdon, 25-Mar-2018.)
(DECID 𝜑 → ((¬ 𝜑𝜓) → ((𝜑𝜓) → 𝜓)))
 
Theoremjadc 796 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 797 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 798 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 799 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 800 Theorem *2.521 of [WhiteheadRussell] p. 107, but with an additional decidability condition. (Contributed by Jim Kingdon, 5-May-2018.)
(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-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11394
  Copyright terms: Public domain < Previous  Next >