User:Gregbard/Theorems of propositional logic

This is a list of truth-functional tautologies which are theorems of propositional logic.

Propositional logic

• Modus ponens

${\displaystyle ((P\to Q)\land P)\to Q}$

• • Modus ponendo ponens

${\displaystyle P\to ((P\to Q)\to Q)}$

• • Modus tollendo ponens
  • Modus non excipiens

• Modus tollens

${\displaystyle ((P\to Q)\land \neg Q)\to \neg P}$

• • Modus ponendo tollens
  • Modus tollendo tollens

• Law of identity

${\displaystyle (P\to P)}$

• Law of the excluded middle, Tertium non datur

${\displaystyle (P\lor \neg P)}$

• Law of noncontradiction

${\displaystyle \neg (P\land \neg P)}$

• Hypothetical syllogism, Transitivity of implication, Chain argument, Chain rule

${\displaystyle ((P\to Q)\land (Q\to R))\to (P\to R)}$

• Disjunctive syllogism

${\displaystyle ((P\lor Q)\land \neg P)\to Q}$

• Constructive dilemma

${\displaystyle (((P\to Q)\land (R\to S))\land (P\lor R))\to (Q\lor S)}$

• Destructive dilemma

${\displaystyle ((P\to Q)\land (R\to S))\to ((\neg Q\lor \neg S)\to (\neg P\lor \neg R))}$

• Simplification

${\displaystyle (P\land Q)\to P}$

• Addition (logic), Disjunction introduction

${\displaystyle P\to (P\lor Q)}$

• Conjunction introduction, Conjunction (logic)

${\displaystyle P,Q\vdash (P\land Q)}$

• De Morgan's laws
  • Negation of conjunction

${\displaystyle \neg (P\land Q)\to (\neg P\lor \neg Q)}$

• • Negation of disjunction

${\displaystyle \neg (P\lor Q)\to (\neg P\land \neg Q)}$

• Double negation

${\displaystyle (P\to \neg \neg P)}$, ${\displaystyle (\neg \neg P\to P)}$

• • Law of triple negation

${\displaystyle \neg \neg \neg P\to \neg P}$

• Transposition

${\displaystyle (P\to Q)\to (\neg Q\to \neg P)}$

• Material implication (rule of inference)

${\displaystyle (P\to Q)\to (\neg P\lor Q)}$

• Material equivalence
  • Biconditional

${\displaystyle ((P\to Q)\land (Q\to P))\to (P\leftrightarrow Q)}$

${\displaystyle ((P\land Q)\lor (\neg P\land \neg Q))\to (P\leftrightarrow Q)}$

• Exportation (logic)

${\displaystyle ((P\to (Q\to R))\to ((P\land Q)\to R))}$

• • Export-import law

${\displaystyle (P\to (Q\to R))\leftrightarrow ((P\land Q)\to R)}$

• Importation (logic)

${\displaystyle ((P\land Q)\to R)\to (P\to (Q\to R))}$

• • Import-export law

${\displaystyle ((P\land Q)\to R)\leftrightarrow (P\to (Q\to R))}$

• Absorption (logic), Adjunction (logic)

${\displaystyle (P\to Q)\to (P\to (P\land Q))}$

• Absorption law
• Peirce's law

${\displaystyle ((P\to Q)\to P)\leftrightarrow P}$

• Ex falso quodlibet, Principle of explosion

${\displaystyle (P\land \neg P)\to Q}$

• Wolfram axiom

${\displaystyle ((P\uparrow Q)\uparrow R)\uparrow (P\uparrow ((P\uparrow R)\uparrow P))\leftrightarrow R}$

• Nicod's axiom

${\displaystyle ((P\uparrow (Q\uparrow R))\uparrow ((M\uparrow (M\uparrow M))\uparrow ((N\uparrow Q)\uparrow ((P\uparrow N)\uparrow (P\uparrow N))))}$

• Case analysis

${\displaystyle (((P\to Q)\land (R\to Q))\land (P\lor R))\to Q}$

• Golden rule (propositional logic)

${\displaystyle ((P\land Q)\leftrightarrow P)\leftrightarrow (Q\leftrightarrow (P\lor Q))}$

• Meridith's astonishing single axiom

${\displaystyle (((((P\to Q)\to (\neg R\to \neg S))\to R)\to T)\to ((T\to P)\to (S\to P)))}$

• Frege's theorem

${\displaystyle ((P\to (Q\to R))\to ((P\to Q)\to (P\to R)))}$

• Praeclarum theorema

${\displaystyle (((P\to Q)\land (R\to S))\to ((P\land R)\to (Q\land S)))}$

• Consensus theorem

${\displaystyle ((((P\land Q)\lor (\neg P\land R))\lor (P\land R))\leftrightarrow ((P\land Q)\lor (\neg P\land R)))}$

• Conditionalization

${\displaystyle Q\to (P\to Q)}$

• Law of Duns Scotus, Law of denial of antecedent

${\displaystyle \neg P\to (P\to Q)}$

• Contraposition
  • Principle of transposition

${\displaystyle (P\to Q)\to (\neg Q\to \neg P)}$

• • Converse law of contraposition

${\displaystyle (\neg P\to \neg Q)\to (Q\to P)}$

${\displaystyle (\neg P\to Q)\to (\neg Q\to P)}$

${\displaystyle (P\to \neg Q)\to (Q\to \neg P)}$

• Consequentia mirabilis, Law of Clavius

${\displaystyle (\neg P\to P)\to P}$

• Proof by contradiction

${\displaystyle (\neg P\to (Q\land \neg Q))\leftrightarrow P}$

• Resolution (logic)

${\displaystyle ((P\land Q)\land (\neg P\land R))\to (Q\land R)}$

• Reductio ad absurdum

${\displaystyle (\neg P\to (Q\land \neg Q))\to P}$

• Composition (logic)

${\displaystyle (P\to Q)\to ((P\to R)\to (P\to (Q\land R)))}$

• Laws of development

${\displaystyle P\leftrightarrow ((P\lor Q)\land (P\lor \neg Q))}$

${\displaystyle P\leftrightarrow ((P\land Q)\lor (P\land \neg Q))}$

• Replacement (logic)

${\displaystyle ((P\leftrightarrow Q)\land (R\leftrightarrow P))\leftrightarrow ((P\leftrightarrow Q)\land (R\leftrightarrow Q))}$

• Shunting (logic)

${\displaystyle ((P\land Q)\to R)\leftrightarrow (P\to (Q\to R))}$

• Goodman's theorem

${\displaystyle (P\leftrightarrow (P\leftrightarrow Q))\to Q}$

• Merging of implication
• Strengthened implication
• Weakened implication
• Drop an always true factor
• Drop an always false term
• Indirect reduction of syllogism
• Weak law of excluded middle
• Identity of equivalence
• Equivalence of negations, Negation of equivalents

• Associative property, Associativity
• Associativity of disjunction

${\displaystyle (P\lor (Q\lor R))\leftrightarrow ((P\lor Q)\lor R)}$

${\displaystyle ((P\lor Q)\lor R)\leftrightarrow (P\lor (Q\lor R))}$

• Associativity of conjunction

${\displaystyle ((P\land Q)\land R)\leftrightarrow (P\land (Q\land R))}$

${\displaystyle (P\land (Q\land R))\leftrightarrow ((P\land Q)\land R)}$

• Associativity of implication

${\displaystyle (P\to (Q\to R))\leftrightarrow ((P\to Q)\to R)}$

• Associativity of equivalence

${\displaystyle ((P\leftrightarrow Q)\leftrightarrow R)\leftrightarrow (P\leftrightarrow (Q\leftrightarrow R))}$

${\displaystyle (P\leftrightarrow (Q\leftrightarrow R))\leftrightarrow ((P\leftrightarrow Q)\leftrightarrow R)}$

• Commutative property, Commutativity
• Commutativity of conjunction

${\displaystyle (P\land Q)\leftrightarrow (Q\land P)}$

• Commutativity of disjunction

${\displaystyle (P\lor Q)\leftrightarrow (Q\lor P)}$

• Commutativity of implication, Law of permutation

${\displaystyle (P\to (Q\to R))\to (Q\to (P\to R))}$

• Commutativity of equivalence, Complete commutative law of equivalence

${\displaystyle (P\leftrightarrow Q)\leftrightarrow (Q\leftrightarrow P)}$

• Distributive property, Distributivity, Principle of distributivity
• Distribution of conjunction over conjunction

${\displaystyle (P\land (Q\land R))\leftrightarrow ((P\land Q)\land (P\land R))}$

• Distribution of conjunction over disjunction

${\displaystyle (P\land (Q\lor R))\leftrightarrow ((P\land Q)\lor (P\land R))}$

• Distribution of disjunction over conjunction

${\displaystyle (P\lor (Q\land R))\leftrightarrow ((P\lor Q)\land (P\lor R))}$

• Distribution of disjunction over disjunction

${\displaystyle (P\lor (Q\lor R))\leftrightarrow ((P\lor Q)\land (P\lor R))}$

• Distribution of implication

${\displaystyle (P\to (Q\to R))\to ((P\to Q)\to (P\to R))}$

• Distribution of implication over equivalence

${\displaystyle P\to (Q\leftrightarrow R)\leftrightarrow ((P\to Q)\leftrightarrow (P\to R))}$

• Distribution of disjunction over equivalence

${\displaystyle (P\lor (Q\leftrightarrow R))\leftrightarrow ((P\lor Q)\leftrightarrow (P\lor R))}$

• Distribution of negation over equivalence

${\displaystyle \neg (P\leftrightarrow Q)\leftrightarrow (\neg P\leftrightarrow Q)}$

• Double distribution

${\displaystyle ((P\land Q)\lor (R\land S))\leftrightarrow (((P\lor R)\land (P\lor S))\land ((Q\lor R)\land (Q\land S)))}$

${\displaystyle ((P\lor Q)\land (R\lor S))\leftrightarrow (((P\land R)\lor (P\land S))\lor ((Q\land R)\lor (Q\lor S)))}$

• Self distributive law of implication

${\displaystyle S\to (P\to Q)\to ((S\to P)\to (S\to Q))}$

• Idempotency, Tautologousness
• Tautology (rule of inference)
• Idempotency of conjunction, Idempotency of conjunction of identity, Principle of tautology for conjunction

${\displaystyle (P\land P)\leftrightarrow P}$

• Idempotency of disjunction, Idempotency of disjunction of identity, Principle of tautology for disjunction

${\displaystyle (P\lor P)\leftrightarrow P}$

• Idempotency of entailment

• Monotonic property, Monotonicity
• Monotonicity of conjunction

${\displaystyle (P\to Q)\to ((P\land R)\to (Q\land R))}$

• Monotonicity of disjunction

${\displaystyle (P\to Q)\to ((P\lor R)\to (Q\lor R))}$

• Monotonicity of entailment
• Law of conflation

${\displaystyle ((P\to Q)\land (R\to S))\to (P\land R)\to (Q\land S))}$

• Reflexive property, Reflexivity
• Reflexivity of implication, Law of identity,

${\displaystyle P\to P}$

• Reflexivity of equivalance, Idempotency of identity, Identity of equivalance

${\displaystyle P\leftrightarrow P}$

Other

• A recto ad obliquum