Problems
Build natural deduction proofs in the Fitch system. Start easy and work up.
Solved
0/50
Easy0/18
Medium0/22
Hard0/10
| Status | Title | Sequent | Topic | Difficulty |
|---|---|---|---|---|
| 1. Conjunction Swap | P ∧ Q ⊢ Q ∧ P | Propositional | Easy | |
| 2. Chain of Conditionals | P → Q, Q → R, P ⊢ R | Propositional | Easy | |
| 3. Weakening | P ∧ Q ⊢ P ∨ R | Propositional | Easy | |
| 4. Double Negation Introduction | P ⊢ ¬¬P | Propositional | Easy | |
| 5. Modus Tollens | P → Q, ¬Q ⊢ ¬P | Propositional | Easy | |
| 6. Disjunction Swap | P ∨ Q ⊢ Q ∨ P | Propositional | Easy | |
| 7. Transitivity of Identity | a = b, b = c ⊢ a = c | Identity | Easy | |
| 8. Hypothetical Syllogism | P → Q, Q → R ⊢ P → R | Propositional | Medium | |
| 9. Contraposition | P → Q ⊢ ¬Q → ¬P | Propositional | Medium | |
| 10. Exportation | (P ∧ Q) → R ⊢ P → Q → R | Propositional | Medium | |
| 11. Disjunctive Syllogism | P ∨ Q, ¬P ⊢ Q | Propositional | Medium | |
| 12. Distribution | P ∧ (Q ∨ R) ⊢ (P ∧ Q) ∨ (P ∧ R) | Propositional | Medium | |
| 13. De Morgan (Disjunction) | ¬(P ∨ Q) ⊢ ¬P ∧ ¬Q | Propositional | Medium | |
| 14. Transitivity of ↔ | P ↔ Q, Q ↔ R ⊢ P ↔ R | Propositional | Medium | |
| 15. Universal Modus Ponens | ∀x (P(x) → Q(x)), ∀x P(x) ⊢ ∀x Q(x) | Quantifiers | Medium | |
| 16. Existential Transfer | ∀x (P(x) → Q(x)), ∃x P(x) ⊢ ∃x Q(x) | Quantifiers | Medium | |
| 17. Law of Excluded Middle | ⊢ P ∨ ¬P | Propositional | Hard | |
| 18. De Morgan (Conjunction) | ¬(P ∧ Q) ⊢ ¬P ∨ ¬Q | Propositional | Hard | |
| 19. Quantifier Negation | ¬∃x P(x) ⊢ ∀x ¬P(x) | Quantifiers | Hard | |
| 20. Quantifier Swap | ∃x ∀y L(x, y) ⊢ ∀y ∃x L(x, y) | Quantifiers | Hard | |
| 21. Conjunction Association | P ∧ Q ∧ R ⊢ P ∧ (Q ∧ R) | Propositional | Easy | |
| 22. Biconditional Backwards | P ↔ Q, Q ⊢ P | Propositional | Easy | |
| 23. Explosion | P, ¬P ⊢ Q | Propositional | Easy | |
| 24. Double Negation Elimination | ¬¬P ⊢ P | Propositional | Easy | |
| 25. Symmetry of Identity | a = b ⊢ b = a | Identity | Easy | |
| 26. Indiscernibility of Identicals | P(a), a = b ⊢ P(b) | Identity | Easy | |
| 27. Universal Instantiation | ∀x (P(x) → Q(x)), P(a) ⊢ Q(a) | Quantifiers | Easy | |
| 28. Existential Generalization | P(a) ∧ Q(a) ⊢ ∃x Q(x) | Quantifiers | Easy | |
| 29. Self-Implication | ⊢ P → P | Propositional | Easy | |
| 30. Conjunction to Conditional | P ∧ Q ⊢ P → Q | Propositional | Easy | |
| 31. Constructive Dilemma | P ∨ Q, P → R, Q → S ⊢ R ∨ S | Propositional | Medium | |
| 32. Importation | P → Q → R ⊢ (P ∧ Q) → R | Propositional | Medium | |
| 33. Composition | P → Q, P → R ⊢ P → (Q ∧ R) | Propositional | Medium | |
| 34. Proof by Cases | P → R, Q → R ⊢ (P ∨ Q) → R | Propositional | Medium | |
| 35. Negated Conditional | P ∧ ¬Q ⊢ ¬(P → Q) | Propositional | Medium | |
| 36. Biconditional Swap | P ↔ Q ⊢ Q ↔ P | Propositional | Medium | |
| 37. Absorption | P → Q ⊢ P → (P ∧ Q) | Propositional | Medium | |
| 38. Universal over Conjunction | ∀x (P(x) ∧ Q(x)) ⊢ ∀x P(x) ∧ ∀x Q(x) | Quantifiers | Medium | |
| 39. Existential Weakening | ∃x P(x) ⊢ ∃x (P(x) ∨ Q(x)) | Quantifiers | Medium | |
| 40. Universal to Existential | ∀x P(x) ⊢ ∃x P(x) | Quantifiers | Easy | |
| 41. Universal Syllogism | ∀x (P(x) → Q(x)), ∀x (Q(x) → R(x)) ⊢ ∀x (P(x) → R(x)) | Quantifiers | Medium | |
| 42. Distinctness | P(a), ¬P(b) ⊢ a ≠ b | Identity | Medium | |
| 43. Existential over Conjunction | ∃x (P(x) ∧ Q(x)) ⊢ ∃x P(x) ∧ ∃x Q(x) | Quantifiers | Medium | |
| 44. Symmetric Relation | ∀x ∀y (R(x, y) → R(y, x)), R(a, b) ⊢ R(b, a) | Quantifiers | Medium | |
| 45. Peirce's Law | ⊢ ((P → Q) → P) → P | Propositional | Hard | |
| 46. Contraposition Reversed | ¬Q → ¬P ⊢ P → Q | Propositional | Hard | |
| 47. Material Implication | P → Q ⊢ ¬P ∨ Q | Propositional | Hard | |
| 48. Negated Universal | ¬∀x P(x) ⊢ ∃x ¬P(x) | Quantifiers | Hard | |
| 49. Existential Antecedent | ∃x P(x) → Q ⊢ ∀x (P(x) → Q) | Quantifiers | Hard | |
| 50. There Is Only One | ∃x (P(x) ∧ ∀y (P(y) → (y = x))), P(a), P(b) ⊢ a = b | Identity | Hard |