Project 2: Logic, Sets, and Proof Lab

A self-contained deep-dive from the canonical Math from Foundations to Machine Learning curriculum.

  • Difficulty: Intermediate
  • Time: 8-16 hours
  • Language: Python (alternatives: JavaScript, Julia, Haskell)
  • Prerequisites: Project 1
  • Source: HS P12

What You Will Build

Build a CLI reasoning lab with three connected modes. truth parses propositions containing not, and, or, and implication, generates every assignment, and classifies the formula as a tautology, contradiction, or contingency. quantify evaluates bounded forall and exists statements over explicit finite sets, preserving quantifier order and reporting witnesses or the smallest counterexample. proof-check reads a structured proof note and checks that assumptions, proof method, legal step annotations, and conclusion are present. It does not pretend to prove arbitrary mathematics; it makes logical structure and missing obligations observable.

Real World Outcome

The command (p and q) -> p generates a four-row CSV truth table and a tautology verdict. A nested finite-domain statement prints the witness chosen for each existential obligation or the first assignment that refutes it. An induction proof note missing its base case fails with a focused diagnostic, while a structurally complete proof produces a checklist suitable for review.

Core Question

What distinguishes a convincing example from a valid argument, and which parts of logical validity can a finite program check deterministically?

Concepts You Must Understand First

  1. Sets and membership: union, intersection, difference, Cartesian products, and finite domains. See Orland, Math for Programmers, logic and set chapters.
  2. Propositional logic: truth values, connective precedence, implication, equivalence, and inference rules.
  3. Quantifiers: forall versus exists, variable binding, and why swapping quantifier order changes meaning.
  4. Proof methods: direct proof, contraposition, contradiction, counterexample, and mathematical induction. See Graham, Knuth, and Patashnik, Concrete Mathematics, Chapter 1.
  5. Sound tool scope: structural validation can reveal omissions but cannot certify unrestricted natural-language reasoning.

Build Milestones

  1. Parse proposition expressions into an AST and generate deterministic truth tables for two to four variables.
  2. Add equivalence, tautology, contradiction, and contingency classification.
  3. Parse finite set declarations and nested quantifiers, returning explicit witness/counterexample traces.
  4. Define a small proof-note schema for assumptions, method, steps, base/induction cases, and conclusion.
  5. Create valid and deliberately broken examples for each reasoning mode.

Hints in Layers

  1. Reuse the parsing discipline from Project 1, but make every AST node return a Boolean.
  2. Evaluate quantifiers recursively: universal nodes short-circuit on a counterexample; existential nodes short-circuit on a witness.
  3. Label proof-check results as structural diagnostics, never as proof of semantic truth.

Common Pitfalls and Debugging

  • Symptom: p -> q behaves like p and q. Cause: implication was encoded incorrectly. Fix: verify it against not p or q for all four assignments.
  • Symptom: forall x exists y and exists y forall x give identical traces. Cause: quantifiers were flattened. Fix: preserve nesting in the AST and bind variables per recursive frame.
  • Symptom: the checker approves an invalid argument. Cause: “all sections present” was reported as semantic validity. Fix: separate completeness warnings from verified finite truth claims.

Definition of Done

  • Truth tables and formula classifications match hand-worked cases.
  • Bounded nested quantifiers preserve order and report concrete witnesses/counterexamples.
  • Set operations are deterministic and covered by tests.
  • Proof notes receive method-specific structural checks, including induction base cases.
  • Output clearly states what the tool has and has not proved.

Previous: Project 1 · Complete learning path · Next: Project 3