Logic methods
Logic Methods: Translation, Models and Proof Practice
Choose a concrete reasoning question: validity, conditions, quantified translation, witness order, variable scope, uniqueness or a natural-deduction rule.
The truth-table and proof tasks below use classical, two-valued truth-functional logic, inclusive disjunction and material implication. They include complete original valuations and proofs; the proof guides name their rule package and keep temporary assumptions visible.
Begin with the question you need to solve. The foundations distinguish truth from valid inference; the quantified guides add complete interpretations and annotated proofs.
The quantified examples use classical first-order logic with a nonempty domain. Their records and diagrams are constructed for learning, and the proof guides state the system whose rules they follow.
Check an argument before formalizing it
Identify premises and conclusions, distinguish deduction from induction, and read conditions in the correct direction.
Valid and Sound Arguments
Separate premise truth from inference validity with ten complete cases and explained answers.
Necessary and Sufficient Conditions
Read if, only if and the contrapositive through twelve complete cases.
Deductive and Inductive Reasoning Worksheet
Practise universal instances, closed-roster deduction and probabilistic inference through twelve cases.
Translate the claim and inspect its interpretation
Specify the domain, track variable occurrences, compare witnesses and find the exact counterexample to a quantified claim.
Every P Is Q vs Some P Is Q: Translate the Domain Correctly
Use a conditional for every P is Q and a conjunction for some P is Q. Complete domain models expose the common swaps and the empty-P case.
Free and Bound Variables: Read Scope Without Capturing a Variable
Identify each variable occurrence and its nearest binder. An assignment table, safe renaming and a capture counterexample make scope visible.
Quantifier Order: Every Object Has a Witness vs One Shared Witness
A different witness for each object is weaker than one witness shared by all. Complete two-object matrices show the distinction and the valid direction.
Negating Nested Quantifiers: Find a Whole Failed Row
Negating every object has some partner requires one object with no partner. Follow the conversion and compare a failed row with a single false cell.
Check identity, uniqueness and description scope
Separate a unique object from a mere name, and distinguish the two negation scopes in Russell’s analysis.
Exactly One in Predicate Logic: Existence Plus Uniqueness
Exactly one requires a P witness and identity-based uniqueness. Compare zero, one and two P objects, then check why two names need not mean two objects.
Negating a Definite Description: Russell’s Outer and Inner Readings
Russell’s outer denial can hold when no unique P exists; the inner denial still requires one. Compare four complete models and make the chosen analysis explicit.
Audit a complete natural-deduction proof
Check arbitrary-name generalization and keep temporary existential witnesses inside the right subproof.
Universal Introduction: Why One Named Case Is Not Enough
Universal introduction needs an arbitrary name with the right dependencies. Compare an invalid particular-premise inference with complete licensed proofs.
Existential Elimination: Keep the Witness Inside Its Subproof
An existential witness is temporary, not an identified named object. A complete seven-line proof shows how to discharge the witness and preserve only the name-free conclusion.
Build tables, find countervaluations and test premises
Calculate a complete main column, track a partial search or require one common valuation for several premises.
Complete Truth Tables: Distinct Letters, Subformulas and the Final Column
Build an eight-row table from distinct letters and subformulas, then audit the final conditional column and a parentheses counterexample.
Partial Truth Tables: Find a Countervaluation and Repair a Failed Choice
Find and verify a countervaluation, preserve forced values, repair a failed trial and distinguish a rejected branch from an exhaustive validity result.
Joint Satisfiability: Why Three Possible Premises Can Fail Together
Check one common valuation, compare all pairwise witnesses, and separate inconsistency-driven validity from the truth of a conclusion.
Discharge assumptions in truth-functional proofs
Match conditional, case, negation and biconditional rules to complete block ranges, exact endpoints and open assumptions.
Conditional Proof: Discharge the Right Assumption and Keep the Others Visible
Derive a nested conditional with exact block ranges, then diagnose an endpoint at the wrong level and an illegal closed-line export.
Disjunction Elimination: Make Both Branches Reach the Same Conclusion
Prove a shared conclusion in two sibling cases, check every range and reject one-case or mismatched-endpoint shortcuts.
Negation Introduction vs Indirect Proof: Choose the Assumption from the Goal
Choose assumptions from the goal, distinguish ¬I from classical IP, and audit two full proofs with exact contradiction and discharge steps.
Biconditional Introduction: Prove Both Directions with Two Audited Subproofs
Prove both directions of a compound equivalence, audit six nested block ranges and check the resulting biconditional on all four rows.
Use the examples to check your reasoning
Try an explained check before opening its answer. A finite countermodel can refute a proposed valid inference; many successful finite tests alone cannot establish validity in every interpretation.
Use the downloadable complete records and proofs to reconstruct a result. Keep your own domain, predicate meanings and open assumptions visible when moving beyond these constructed examples.