David's Proof Checker

This is an alpha version. I cannot guarantee that it is bug-free.

Please report any potential bugs that you find!

But before you're sure the checker is wrong, check the developer console (Control+Shift+J or Command+Option+J) to see the checker's comments.


Add Line
Report Bug

Saved Proofs


This is a proof checker for propositional logic (and hopefully, soon, predicate logic too) proofs, using the proof system set out in How Logic Works by Hans Halvorson, Princeton University Press, forthcoming. (sample)

For those curious, it's written in pure JavaScript (with some jQuery to make my life easier on the front end). It all takes place in this single HTML file -- this is a single-page web app in the truest sense of the term :)

This app is currently under development. When the final product is released, it will not be at this URL.

How to Use

The proof checker is pretty picky about formatting. If you're having issues, make sure you've read this all the way through before submitting a bug report.

Click "Add Line" to get started. After that, click any part of a line to edit it. You can press "enter" to save, or "tab" to move to the next part of the line, or onto the next line. (If there is no next line, it will automatically create a next line for easy proof writing.)

To delete a line, just leave the sentence part blank, and the line will be deleted.

You can type in English or any of the shortcodes listed below, and your text will automatically be converted into nice pretty symbols, as long as the sentence is valid. A complete list of shortcodes that will be converted is listed below. You must leave a space before anything you want converted.

The proof checker is very particular about parentheses; don't leave them off. Only unambiguous input is accepted.

It is also very picky about citations; you must cite lines in the proper order. Eg "1,2 ∧I" is not treated as the same as "2,1 ∧I", and the sentences in your conjunction must correspond properly to the order you cited them.

Also, all propositions must be capital letters; lowercase letters will be interpreted as names for predicate logic.

When your proof is ready, click "Check". The proof checker will examine your proof; if it is valid, the whole thing will be highlighted in green. If it is not, lines that have errors will be highlighted in red.

That's pretty much it right now! If you have any questions, comments, concerns, or most importantly, bug reports, email dmcelroy [at] princeton.edu.

List of shortcodes:

















List of Inference Rules:

  • Assumption: "A"
  • Conjunction Introduction: "andI"
  • Conjunction Elimination: "andE"
  • Disjunction Introduction: "orI"
  • Disjunction Elimination: "orE"
  • Conditional Proof: "CP"
  • Modus Ponendo Ponens: "MPP"
  • Modus Tollendo Tollens: "MTT"
  • Reductio ad Absurdum: "RAA"
  • Double Negation Entroduction: "DNi"
  • Double Negation Elimination: "DNe"
  • Double Negation: "DN"
  • Universal Introduction: "UI"
  • Universal Elimination: "UE"
  • Existential Introduction: "EI"
  • Existential Elimination: "EE"