?

Natural Deduction Contraption

WFF Constructor

Propositional Logic

Drag Variables:

P
Q
R
S

Drop on Connectives:

~
∧
∨
→
↔

WFF Output

🗑️

Proof

    Subproofs

    Conditional Introduction (→I)
    Goal (e.g., φ → ψ)
    Universal Introduction (∀I)
    Goal (e.g., ∀xφx)
    Existential Elimination (∃E)
    Major Premise (e.g., ∃xφx)
    Subproof Conclusion (e.g., ψ)

    Inference Rules

    Modus Ponens (MP / →E)
    Premise 1 (e.g., φ → ψ)
    Premise 2 (e.g., φ)
    Modus Tollens (MT)
    Premise 1 (e.g., φ → ψ)
    Premise 2 (e.g., ~ψ)
    And Introduction (∧I)
    Premise 1 (e.g., φ)
    Premise 2 (e.g., ψ)
    And Elimination (∧E)
    Premise (e.g., φ ∧ ψ)
    Existential Introduction (∃I)
    Formula (e.g., F(a))
    Variable to Generalize (e.g., x)
    Double Negation (DN)
    Premise (e.g., ~~φ or φ)
    Reiteration (Re)
    Line to Reiterate