Natural Deduction Proof Builder

About Natural Deduction

Natural deduction is a proof system that captures how we reason informally. Unlike axiomatic systems, natural deduction introduces inference rules that directly mirror logical reasoning patterns. Fitch-style notation uses vertical lines to track which assumptions are in effect for each step of the proof.

Fitch Notation

In Fitch diagrams, each line of the proof is numbered and shows:

• Formula: The logical statement at this step
• Justification: The inference rule and which lines it depends on
• Scope lines: Vertical bars showing active assumptions

When you introduce an assumption (for conditional introduction or reductio), a new vertical line begins. When you discharge that assumption, the line ends.

Key Inference Rules

• → Elimination (Modus Ponens): From P→Q and P, infer Q
• → Introduction: To prove P→Q, assume P and derive Q, then discharge the assumption
• ∧ Introduction: From P and Q, infer P∧Q
• ∧ Elimination: From P∧Q, infer P (or Q)
• ∨ Introduction: From P, infer P∨Q
• ∨ Elimination: From P∨Q, and subproofs P⊢R and Q⊢R, infer R
• ¬ Introduction: To prove ¬P, assume P and derive ⊥ (contradiction)
• ¬ Elimination: From ¬¬P, infer P
• Reductio ad Absurdum: To prove P, assume ¬P and derive ⊥

Building Proofs

Start with your premises. At each step, apply an inference rule to derive a new formula. Some rules require subproofs—introduce an assumption, derive consequences, then discharge it. The goal is to derive your conclusion using only valid inference rules.

Common Patterns

• Conditional proof: To prove P→Q, assume P and derive Q
• Proof by contradiction: To prove P, assume ¬P and derive ⊥
• Disjunction elimination: Case analysis on P∨Q by proving both P⊢R and Q⊢R
• DeMorgan's laws: ¬(P∧Q) ↔ (¬P∨¬Q), requiring careful subproof management

Notation Guide

Use these symbols in your formulas:

• ¬ for negation (NOT)
• ∧ for conjunction (AND)
• ∨ for disjunction (OR)
• → for implication (IF...THEN)
• ⊥ for contradiction (falsum)

Type these symbols directly or use keyboard shortcuts: & for ∧, | for ∨, - for →, ~ for ¬

Educational Value

Natural deduction helps you understand:

• The structure of logical arguments
• How assumptions work and when they can be discharged
• The relationship between syntax (proof rules) and semantics (truth)
• Why certain inferences are valid and others are fallacious