Wff Helper

Start Proof

Welcome to Wff Helper!

This is a tool to verify and format proofs in propositional logic. You can start a new proof above.

This tool does NOT solve proofs for you. It DOES verify the steps you input are logically valid, and it DOES verify once you have finished the proof.

Operators

Not: ~ (tilde)

And: ^ (caret)

Or: v (the letter v)

Conditional: =>

Biconditional: <=>

Example Usage: Starting a Proof

Example 1: Suppose we want to start a Direct Proof to prove ⊢ (a => (a v b))

• Enter (a => (a v b)) into the "Prove" box above
• Then, select Direct Proof from the drop down
• Leave the "Assumptions" box empty and click "Start Proof"

Example 2: Starting a proof for a => b, b => c ⊢ a => c using No Proof Method

• Enter a => c into the "Prove" box above
• Then, select No Proof Method from the drop down
• Then, enter a => b into the "Assumptions" box
• Then, on a new line, enter b => c into the "Assumptions" box
• Click "Start Proof"

Troubleshooting

If nothing happens when you click "Start Proof", check to make sure you haven't entered something with invalid syntax or an invalid symbol.

Unfortunately I haven't added error messages yet :(