Project 12: The Logic and Proof Lab

Build a CLI-first reasoning lab that checks propositional formulas, quantifier statements on finite domains, and proof skeleton completeness.

Quick Reference

Attribute Value
Difficulty Intermediate (Level 2)
Time Estimate 8-16 hours
Main Programming Language Python
Alternative Programming Languages JavaScript, Julia, Haskell
Key Topics Logic operators, quantifiers, contradiction, induction
Input Mode CLI statements and markdown proof notes
Output Mode Truth tables, witness/counterexample reports, proof diagnostics

1) Learning Objectives

By finishing this project, you will:

  1. Evaluate compound propositions with deterministic truth tables.
  2. Distinguish forall and exists statements and explain quantifier order.
  3. Detect and report counterexamples on finite domains.
  4. Validate whether a proof skeleton contains assumptions, legal steps, and conclusion mapping.
  5. Explain method selection: direct proof vs contradiction vs induction.

2) All Theory Needed (Per-Concept Breakdown)

Concept A: Propositions and Inference Rules

A proposition is a statement that can be true or false. Compound propositions connect atomic statements with logical operators (and, or, not, implies). A valid argument is not just a true conclusion; it is a conclusion reached by legal inference from assumptions. In this project, inference is simplified into explicit rule checks and table-based verification.

Concept B: Quantifiers and Domain Semantics

Quantifiers bind variables over a domain. forall x means a claim must hold for every value in domain. exists x means at least one value works. The order of quantifiers changes meaning, so parser and evaluator must preserve order exactly. On finite domains, exhaustive evaluation gives deterministic truth/counterexample results.

Concept C: Proof Structure as a Pipeline

A proof can be treated as a pipeline:

  1. Define domain and assumptions.
  2. Choose method.
  3. Apply legal transformations.
  4. Reach conclusion.
  5. Verify no hidden assumptions were introduced.

Failure modes include missing base case in induction, assuming what you are trying to prove, and conflating examples with general proof.

3) Project Specification

3.1 What You Will Build

A terminal tool with three modes:

  1. truth: generate truth tables for proposition strings.
  2. quantify: evaluate quantified statements on user-provided finite sets.
  3. proof-check: parse structured markdown proof notes and validate section completeness.

3.2 Functional Requirements

  1. Parse proposition expressions with parentheses and operator precedence.
  2. Compute full truth table with derived column values.
  3. Evaluate quantified predicates on finite integer sets.
  4. Emit smallest counterexample (if statement false).
  5. Validate proof skeleton fields: assumptions, method, steps, conclusion.

3.3 Non-Functional Requirements

  • Deterministic output ordering.
  • Clear error messages for invalid syntax.
  • Reproducible tests with fixed domain ordering.

3.4 Real World Outcome

$ python proof_lab.py --mode truth --statement "(p and q) -> p"
[result] tautology: true
[rows] 4
[output] saved: outputs/truth_table_implication.csv

$ python proof_lab.py --mode quantify --statement "forall x in {1,2,3}: exists y in {1,2,3}: x<=y"
[result] true
[witnesses] x=1->1, x=2->2, x=3->3

$ python proof_lab.py --mode proof-check --proof-file proofs/induction_sum.md
[check] sections present: assumptions, base_case, induction_step, conclusion
[status] structurally valid

4) Solution Architecture

4.1 High-Level Design

Input Parser -> AST Builder -> Evaluator Engine -> Reporter
                              |                |
                              v                v
                      Counterexample Finder   Proof Skeleton Checker

4.2 Key Components

Component Responsibility
Parser Convert logical text into structured tree
Evaluator Compute truth values for rows/domain assignments
Quantifier Runner Enumerate domain values in quantifier order
Reporter Print tables, witnesses, and diagnostics

5) Implementation Guide

Phase 1: Proposition Engine

  • Build tokenizer for variables/operators.
  • Implement precedence-aware expression parser.
  • Generate truth tables for 2-4 variables.

Phase 2: Quantifier Evaluator

  • Parse bounded domain declarations.
  • Evaluate predicates with nested loops.
  • Return witness/counterexample traces.

Phase 3: Proof Skeleton Check

  • Define required markdown sections.
  • Parse and validate structure.
  • Emit missing-section and method mismatch warnings.

6) Validation Checklist

  • Tautology/contradiction/contingency classifications are correct.
  • Quantifier order changes results when expected.
  • Counterexamples are concrete and minimal.
  • Proof skeleton checks fail on intentionally broken samples.

7) Extension Ideas

  1. Add predicate simplification and equivalence checks.
  2. Support small symbolic rewrite rules for proof-step validation.
  3. Export HTML reports for classroom review.

8) Books and References

  • Math for Programmers (Paul Orland) - logic and proof chapters.
  • Concrete Mathematics - proof style and discrete reasoning sections.
  • Common Core High School Mathematical Practices - reasoning and proof expectations.