| name | expression | explanation | |
|---|---|---|---|
Self-Implication | P → P | If P then P - a proposition always implies itself | |
Non-Contradiction | ¬(P ∧ ¬P) | Not both P and not P - contradictions cannot be true | |
Self-Equivalence | P ↔ P | P if and only if P - a proposition is always equivalent to itself | |
Modus Ponens Form | ((P → Q) ∧ P) → Q | If P implies Q and P is true, then Q must be true | |
Hypothetical Syllogism | ((P → Q) ∧ (Q → R)) → (P → R) | If P implies Q and Q implies R, then P implies R | |
Weakening | P → (Q → P) | If P is true, then it remains true regardless of Q | |
Proof by Contradiction Form | (¬P → P) → P | If assuming not-P leads to P, then P must be true | |
Peirce's Law | ((P → Q) → P) → P | Classical logical principle not provable in intuitionistic logic | |
Disjunctive Weakening | P ∨ (P → Q) | Either P is true or if P then Q - always true | |
Implication Disjunction | (P → Q) ∨ (Q → P) | Either P implies Q or Q implies P - always true | |
Conjunction Implication | (P → Q) → ((P ∧ R) → Q) | If P implies Q, then P and R together also imply Q | |
Conjunction Introduction Form | P → (Q → (P ∧ Q)) | If P and Q are both true, their conjunction is true | |
Modus Ponens Alternative Form | (P ∧ (P → Q)) → Q | If P is true and P implies Q, then Q is true | |
Modus Tollens Form | (¬Q ∧ (P → Q)) → ¬P | If Q is false and P implies Q, then P must be false | |
Self-Contradiction Implication | (P → ¬P) → ¬P | If P implies its own negation, then P must be false | |
Implication Negation Equivalence | ¬(P → Q) ↔ (P ∧ ¬Q) | An implication is false only when its antecedent is true and consequent is false | |
Contradiction Implication | (P → (Q ∧ ¬Q)) → ¬P | If P implies a contradiction, then P must be false | |
Double Negation Implication | ((P → Q) ∧ (P → ¬Q)) → ¬P | If P implies both Q and not-Q, then P must be false | |
Triple Negation Implication | (P → Q) → ((P → ¬Q) → ¬P) | If P implies contradictory results, P must be false | |
Material Implication Alternative | (P → Q) → (¬P ∨ Q) | If P implies Q, then either P is false or Q is true | |
Disjunctive Implication | (P ∨ Q) → (¬P → Q) | If either P or Q is true, then not-P implies Q | |
Hypothetical Syllogism Disjunctive Form | ((P → Q) ∧ (R → S) ∧ (P ∨ R)) → (Q ∨ S) | Complex syllogism with disjunctive conclusion | |
Biconditional Expansion | (P ↔ Q) ↔ ((P → Q) ∧ (Q → P)) | P if and only if Q means P implies Q and Q implies P |