Propositional logic
Prove disjunctions, reason from alternatives, treat negation as an implication to False, work with equivalences and derive one of De Morgan’s laws. Then meet excluded middle and proof by contradiction, and the statements that need them, and finish with a mixed review without step-by-step guidance.
Progress is kept in this browser until you sign in
- Prove an or-statementTo prove P ∨ Q, pick the side you can prove.12 min
- Reason from alternativescases h with | inl hp | inr hq handles both possibilities.16 min
- What ¬P really meansA negation is a function into False. Apply it like one.14 min
- From a contradiction, anythingexfalso and absurd let a contradiction prove any goal.14 min
- Prove an equivalenceP ↔ Q is two implications. constructor gives you both.13 min
- Use an equivalenceh.mp and h.mpr turn an iff into the direction you need.13 min
- Prove a contrapositiveFrom P → Q and ¬Q, build ¬P by introducing an assumed P.15 min
- A De Morgan lawShow ¬(P ∨ Q) gives ¬P ∧ ¬Q, combining everything so far.17 min
- Split on whether P holdsby_cases and the classical De Morgan law ¬(P ∧ Q) → ¬P ∨ ¬Q.17 min
- Proof by contradictionAssume the negation of the goal, derive False, and see why that step is classical.16 min
- Review: every connectiveMixed exercises on or, not, iff and classical reasoning, with no step checklist.18 min