Proof Playground

Logic Mode:Mode:

Rule Library (Classical)

A – Assumption
Example:
Notes: Initial assumption to start a proof or subproof.
Case – Case Analysis
Example: Subproof structure
Notes: Used to create subproofs for proof by cases, assumptions, or modal reasoning.
MP – Modus Ponens
Example: A → B, A ⊢ B
Notes: From A → B and A, infer B.
MT – Modus Tollens
Example: A → B, ¬B ⊢ ¬A
Notes: From A → B and ¬B, infer ¬A.
HS – Hypothetical Syllogism
Example: A → B, B → C ⊢ A → C
Notes: From A → B and B → C, infer A → C.
DS – Disjunctive Syllogism
Example: A ∨ B, ¬A ⊢ B
Notes: From A ∨ B and ¬A, infer B.
Simp – Simplification
Example: A ∧ B ⊢ A
Notes: From A ∧ B, infer A.
Conj – Conjunction
Example: A, B ⊢ A ∧ B
Notes: From A and B, infer A ∧ B.
Add – Addition
Example: A ⊢ A ∨ B
Notes: From A, infer A ∨ B.
DN – Double Negation
Example: A ⊢ ¬¬A
Notes: From A, infer ¬¬A (or vice versa).
DM – De Morgan's Laws
Example: ¬(A ∧ B) ⊢ ¬A ∨ ¬B
Notes: From ¬(A ∧ B), infer ¬A ∨ ¬B (or similar transformations).
BE – Biconditional Elimination
Example: A ↔ B ⊢ (A → B) ∧ (B → A)
Notes: From A ↔ B, infer A → B and B → A.
BI – Biconditional Introduction
Example: A → B, B → A ⊢ A ↔ B
Notes: From A → B and B → A, infer A ↔ B.
Contrad – Contradiction
Example: A, ¬A ⊢ False
Notes: From A and ¬A, infer False.
RAA – Reductio ad Absurdum
Example: Assume P, derive False ⊢ ¬P
Notes: If assuming P leads to a contradiction, infer ¬P.
DE – Disjunction Elimination (Classical)
Example: P ∨ Q, P → R, Q → R ⊢ R
Notes: From P ∨ Q and subproofs showing P → R and Q → R, infer R (Classical variant).

Exercises (Classical)

Saved Proofs

No proofs saved.

Givens

No givens provided.

Proof Structure

No proof lines added yet.