Propositional logic, step by step
Every later proof is built from these moves. You will prove disjunctions, reason from alternatives, treat negation as an implication to False, work with equivalences, and derive one of De Morgan’s laws yourself.
Sign in to track your progress
- Prove an or-statementTo prove P ∨ Q, pick the side you can prove.7 min
- Reason from alternativescases h with | inl hp | inr hq handles both possibilities.11 min
- What ¬P really meansA negation is a function into False. Apply it like one.9 min
- From a contradiction, anythingexfalso and absurd let a contradiction prove any goal.9 min
- Prove an equivalenceP ↔ Q is two implications. constructor gives you both.8 min
- Use an equivalenceh.mp and h.mpr turn an iff into the direction you need.8 min
- Prove a contrapositiveFrom P → Q and ¬Q, build ¬P by introducing an assumed P.10 min
- A De Morgan lawShow ¬(P ∨ Q) gives ¬P ∧ ¬Q, combining everything so far.12 min