This proof checker is designed for working with the proof system Gentzen uses in his "Die Wiederspruchsfreiheit der reinen Zahlentheorie" (1936) that I use in my introductory formal logic course. The textbook and other instruction material are available at https://adamay909.github.io/logicbook/.
Here is the short version of the system. A proof is stated as a series of sequents where each sequent must have exactly one formula as its succedent. Here is an inference using what is often called conjunction introduction:
The proof system has 9 inference rules for sentential logic. In the system, you may:
There are four more rules for predicate logic with quantifiers:
Finally, we have axioms and a rule for using axioms:
All sentences of the following forms are axioms:
Axiom (Ax) If α is an axiom, infer ⊢ α.
Notice the lower case x in the abbreviation for Axiom.
For annotations, the proof checker requires you to use the abbreviations given in parentheses.
There are three more rules for rewriting the antecedent side of sequents:
These sequent rewrite rules have no names. When you use them, just give the relevant line numbers in the annotations. The proof checker allows you to use the first two silently. E.g., instead of:
you may, but are not required to, write:
But you are required to be explicit in the use of the third sequent rewrite rule. E.g., the following is not accepted by the proof checker:
You must write the above as:
Notice the use of the keyword "premise" in the annotation. That is what you must use for a premise that is not an assumption (an assumption must take the form s ⊢ s).
To make life easier, you can choose to allow the use of a few theorems by clicking on the gear icon on the top left and then clicking the button that says "Theorems". If theorems are allowed, it will show a check mark next to "Theorems". You can disable theorems by clicking on the button again.
If you do use theorems, you must use their abbreviations in the annotations. The theorems are:
The proof checker will recognize instances of theorems. Here is an example of a use of EM:
The derivations in this system can be trivially converted to proofs in the style of Lemmon's Beginning Logic as well others influenced by him (e.g., Allen and Hand, Logic Primer). E.g., the following proof:
turns into the following in Lemmon's style:
1 (1) P
2 (2) Q
1,2 (3) P and Q
What we do is replace the turnstile with the line number, and replace formulas on the antecedent side of each sequent with the appropriate line numbers (of course, you need to add appropriate annotations). One thing Gentzen's notation allows is the use of placeholders on the antecedent side of a sequent which can be useful.
The proof checker checks you whether each line is in accordance with the proof system. But it does not check whether you have managed to show what you set out to show. You'll have to check that yourself---usually a matter of inspecting the last line of your derivation, possibly in combination with the premises.
You may have to go through several rounds of checking and fixing a derivation because the proof checker stops checking at the first error it encounters.
The editor is very primitive with limited functionality. You can move around the editor with the arrow keys as well position the cursor with your mouse. While it should work on touch devices (not extensively tested, though), using a physical keyboard is highly recommended. No pasting into the editor is allowed.
Apart from the above limitations, The editor is designed to be as transparent as possible: symbols should be easy to type and you should not have to worry about how what's on the screen corresponds to what you see in the course material. Some special key combinations are used for typing symbol like Greek characters and the turnstile. Check the help on how to input symbols.
The proof checker will attempt to store the current state of the editor so that when you open the proof checker again, you will be presented with the last state of things before you quit (or the program crashed). The proof checker will also store a series of snapshots of the editor. This last happens whenever you clear the screen or move to the next exercise. All history is stored in the browser's local cache so how much history is stored for how long depends on your browser settings and the like. You can go back and forth in history using 'back' and 'forward' buttons above the input area. You can see where you are in the lower right corner.
You can find the option to switch to an axiomatic proof system under the advanced option in the settings under the gear icon. The axiomatic system looks as follows:
All instances of the following schemata are axioms:
(notice that A2 and A3 each combine two schemata for ease of use)
There is a single inference rule:
The system is strict and only allows direct proofs. That is: no indirect proofs because there is no way to make assumptions; and no conditional proofs, either.
The editor window looks a little different since each line only needs a formula and an annotation. Use the abbreviations above in the annotations.
You can get the source code at: https://github.com/adamay909/logicTools
It's in the subdirectory named proofChecker.
This proof-checker is designed to run completely inside the browser so it is easy to host yourself so long as you are able to host static websites. The docs directory of the GitHub repository contains all the files you need.
There is also a Makefile with the source code that you can use to make life easier. The files needed for the proofchecker to work will be copied to ../docs/.
The Go, HTML, and CSS sources for this proof checker written by Masahiro Yamada. Licensed under the MIT License.