User:Gregbard/Theorems of propositional logic

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

Propositional logic

• Modus ponens

$((P\to Q)\land P)\to Q$

• • Modus ponendo ponens

$P\to ((P\to Q)\to Q)$

• • Modus tollendo ponens
  • Modus non excipiens

• Modus tollens

$((P\to Q)\land \neg Q)\to \neg P$

• • Modus ponendo tollens
  • Modus tollendo tollens

• Law of identity

$(P\to P)$

• Law of the excluded middle, Tertium non datur

$(P\lor \neg P)$

• Law of noncontradiction

$\neg (P\land \neg P)$

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

$((P\to Q)\land (Q\to R))\to (P\to R)$

• Disjunctive syllogism

$((P\lor Q)\land \neg P)\to Q$

• Constructive dilemma

$(((P\to Q)\land (R\to S))\land (P\lor R))\to (Q\lor S)$

• Destructive dilemma

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

• Simplification

$(P\land Q)\to P$

• Addition (logic), Disjunction introduction

$P\to (P\lor Q)$

• Conjunction introduction, Conjunction (logic)

$P,Q\vdash (P\land Q)$

• De Morgan's laws
  • Negation of conjunction

$\neg (P\land Q)\to (\neg P\lor \neg Q)$

• • Negation of disjunction

$\neg (P\lor Q)\to (\neg P\land \neg Q)$

• Double negation

$(P\to \neg \neg P)$, $(\neg \neg P\to P)$

• • Law of triple negation

$\neg \neg \neg P\to \neg P$

• Transposition

$(P\to Q)\to (\neg Q\to \neg P)$

• Material implication (rule of inference)

$(P\to Q)\to (\neg P\lor Q)$

• Material equivalence
  • Biconditional

$((P\to Q)\land (Q\to P))\to (P\leftrightarrow Q)$

$((P\land Q)\lor (\neg P\land \neg Q))\to (P\leftrightarrow Q)$

• Exportation (logic)

$((P\to (Q\to R))\to ((P\land Q)\to R))$

• • Export-import law

$(P\to (Q\to R))\leftrightarrow ((P\land Q)\to R)$

• Importation (logic)

$((P\land Q)\to R)\to (P\to (Q\to R))$

• • Import-export law

$((P\land Q)\to R)\leftrightarrow (P\to (Q\to R))$

• Absorption (logic), Adjunction (logic)

$(P\to Q)\to (P\to (P\land Q))$

• Absorption law
• Peirce's law

$((P\to Q)\to P)\leftrightarrow P$

• Ex falso quodlibet, Principle of explosion

$(P\land \neg P)\to Q$

• Wolfram axiom

$((P\uparrow Q)\uparrow R)\uparrow (P\uparrow ((P\uparrow R)\uparrow P))\leftrightarrow R$

• Nicod's axiom

$((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

$(((P\to Q)\land (R\to Q))\land (P\lor R))\to Q$

• Golden rule (propositional logic)

$((P\land Q)\leftrightarrow P)\leftrightarrow (Q\leftrightarrow (P\lor Q))$

• Meridith's astonishing single axiom

$(((((P\to Q)\to (\neg R\to \neg S))\to R)\to T)\to ((T\to P)\to (S\to P)))$

• Frege's theorem

$((P\to (Q\to R))\to ((P\to Q)\to (P\to R)))$

• Praeclarum theorema

$(((P\to Q)\land (R\to S))\to ((P\land R)\to (Q\land S)))$

• Consensus theorem

$((((P\land Q)\lor (\neg P\land R))\lor (P\land R))\leftrightarrow ((P\land Q)\lor (\neg P\land R)))$

• Conditionalization

$Q\to (P\to Q)$

• Law of Duns Scotus, Law of denial of antecedent

$\neg P\to (P\to Q)$

• Contraposition
  • Principle of transposition

$(P\to Q)\to (\neg Q\to \neg P)$

• • Converse law of contraposition

$(\neg P\to \neg Q)\to (Q\to P)$

$(\neg P\to Q)\to (\neg Q\to P)$

$(P\to \neg Q)\to (Q\to \neg P)$

• Consequentia mirabilis, Law of Clavius

$(\neg P\to P)\to P$

• Proof by contradiction

$(\neg P\to (Q\land \neg Q))\leftrightarrow P$

• Resolution (logic)

$((P\land Q)\land (\neg P\land R))\to (Q\land R)$

• Reductio ad absurdum

$(\neg P\to (Q\land \neg Q))\to P$

• Composition (logic)

$(P\to Q)\to ((P\to R)\to (P\to (Q\land R)))$

• Laws of development

$P\leftrightarrow ((P\lor Q)\land (P\lor \neg Q))$

$P\leftrightarrow ((P\land Q)\lor (P\land \neg Q))$

• Replacement (logic)

$((P\leftrightarrow Q)\land (R\leftrightarrow P))\leftrightarrow ((P\leftrightarrow Q)\land (R\leftrightarrow Q))$

• Shunting (logic)

$((P\land Q)\to R)\leftrightarrow (P\to (Q\to R))$

• Goodman's theorem

$(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

$(P\lor (Q\lor R))\leftrightarrow ((P\lor Q)\lor R)$

$((P\lor Q)\lor R)\leftrightarrow (P\lor (Q\lor R))$

• Associativity of conjunction

$((P\land Q)\land R)\leftrightarrow (P\land (Q\land R))$

$(P\land (Q\land R))\leftrightarrow ((P\land Q)\land R)$

• Associativity of implication

$(P\to (Q\to R))\leftrightarrow ((P\to Q)\to R)$

• Associativity of equivalence

$((P\leftrightarrow Q)\leftrightarrow R)\leftrightarrow (P\leftrightarrow (Q\leftrightarrow R))$

$(P\leftrightarrow (Q\leftrightarrow R))\leftrightarrow ((P\leftrightarrow Q)\leftrightarrow R)$

• Commutative property, Commutativity
• Commutativity of conjunction

$(P\land Q)\leftrightarrow (Q\land P)$

• Commutativity of disjunction

$(P\lor Q)\leftrightarrow (Q\lor P)$

• Commutativity of implication, Law of permutation

$(P\to (Q\to R))\to (Q\to (P\to R))$

• Commutativity of equivalence, Complete commutative law of equivalence

$(P\leftrightarrow Q)\leftrightarrow (Q\leftrightarrow P)$

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

$(P\land (Q\land R))\leftrightarrow ((P\land Q)\land (P\land R))$

• Distribution of conjunction over disjunction

$(P\land (Q\lor R))\leftrightarrow ((P\land Q)\lor (P\land R))$

• Distribution of disjunction over conjunction

$(P\lor (Q\land R))\leftrightarrow ((P\lor Q)\land (P\lor R))$

• Distribution of disjunction over disjunction

$(P\lor (Q\lor R))\leftrightarrow ((P\lor Q)\land (P\lor R))$

• Distribution of implication

$(P\to (Q\to R))\to ((P\to Q)\to (P\to R))$

• Distribution of implication over equivalence

$P\to (Q\leftrightarrow R)\leftrightarrow ((P\to Q)\leftrightarrow (P\to R))$

• Distribution of disjunction over equivalence

$(P\lor (Q\leftrightarrow R))\leftrightarrow ((P\lor Q)\leftrightarrow (P\lor R))$

• Distribution of negation over equivalence

$\neg (P\leftrightarrow Q)\leftrightarrow (\neg P\leftrightarrow Q)$

• Double distribution

$((P\land Q)\lor (R\land S))\leftrightarrow (((P\lor R)\land (P\lor S))\land ((Q\lor R)\land (Q\land S)))$

$((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

$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

$(P\land P)\leftrightarrow P$

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

$(P\lor P)\leftrightarrow P$

• Idempotency of entailment

• Monotonic property, Monotonicity
• Monotonicity of conjunction

$(P\to Q)\to ((P\land R)\to (Q\land R))$

• Monotonicity of disjunction

$(P\to Q)\to ((P\lor R)\to (Q\lor R))$

• Monotonicity of entailment
• Law of conflation

$((P\to Q)\land (R\to S))\to (P\land R)\to (Q\land S))$

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

$P\to P$

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

$P\leftrightarrow P$

Other

• A recto ad obliquum