THE LOGIC EDITOR

Welcome to The Logic Editor!

Here you can do natural deduction proofs in propositional logic by entering premises and assumptions, and applying inference rules. This editor follows the rules of G. Forbes' "Modern Logic."

An example proof is currently shown. Click on “Clear all” to begin your own!

To begin your proof, add a premise or an assumption.

Or click on “Download/upload” or “Settings” to see more options.

Add a premise or an assumption.

Or choose an inference rule to be applied.

Or, if the last line contains your desired conclusion, end the proof.

Or click on “Clear latest” to delete a line, or “Clear all” to start over, or “Download/upload” or “Settings” to see more options.

Currently, you cannot end the proof, because the last line depends on one or more assumptions.

Choose the premise’s main connective.

Or, if the premise is atomic, choose its propositional letter.

Or, if you have changed you mind, choose to add an assumption instead.

Or click “Clear all” to start over.

Choose the premise’s main connective.

Or, if the premise is atomic, choose its propositional letter.

Or, if you have changed you mind, choose to add an assumption or apply an inference rule instead.

Or click “Clear all” to start over.

Choose the assumption’s main connective.

Or, if the assumption is atomic, choose its propositional letter.

Or, if you have changed you mind, choose to add a premise instead.

Or click “Clear all” to start over.

Choose the assumption’s main connective.

Or, if the assumption is atomic, choose its propositional letter.

Or, if you have changed you mind, choose to add a premise or apply an inference rule instead.

Or click “Clear all” to start over.

Choose the main connective for the currently selected sub-formula.

Or, if this sub-formula is atomic, choose its propositional letter.

Or click on a different part of the formula to input that first. (Non-empty parts of the formula can be selected to be overwritten.)

Or click "Clear latest" to cancel the addition of the current line.

Or click “Clear all” to start over.

Choose a line in the already existing part of the proof to play the role of the highlighted line in the inference rule. Black lines have the required form, and can be selected.

Or, if you have changed your mind, choose an alternative to this inference rule.

Or click “Clear all” to start over.

Choose a line in the already existing part of the proof to play the role of the highlighted line in the inference rule. Black lines have the required form, and can be selected.

Or, if you have changed your mind, cancel the application of this inference rule.

Or click “Clear all” to start over.

There is no line in the already existing part of the proof that has the form of the highlighted line in the inference rule. Hence, you cannot continue with the application of this rule.

Instead, choose another inference rule to be applied.

Or add a premise or an assumption.

Or click “Clear all” to start over.

There is no line in the already existing part of the proof that has the form of the highlighted line in the inference rule. Hence, you cannot continue with the application of this rule.

Therefore, click on “Clear latest".

Then choose another inference rule to be applied or add a premise or an assumption.

Or click “Clear all” to start over.

Decide if you want the existing disjunct to be the left one in the new line’s formula and the new one the right one, or vise versa.

Or click "Clear latest" to cancel the application of the current rule.

Or click “Clear all” to start over.

Choose the main connective for the new disjunct.

Or, if this disjunct is atomic, choose its propositional letter.

Or, if you have changed your mind, click "Clear latest" to cancel the application of this inference rule.

Or click “Clear all” to start over.

Choose the main connective for the currently selected sub-formula.

Or, if this sub-formula is atomic, choose its propositional letter.

Or click on a different part of the formula to input that first. (Non-empty parts of the new disjunct can be selected to be overwritten.)

Or, if you have changed your mind, click "Clear latest" to cancel the application of this inference rule.

Or click “Clear all” to start over.

Choose the main connective for the new formula.

Or, if this formula is atomic, choose its propositional letter.

Or, if you have changed your mind, click "Clear latest" to cancel the application of this inference rule.

Or click “Clear all” to start over.

Choose the main connective for the currently selected sub-formula.

Or, if this sub-formula is atomic, choose its propositional letter.

Or click on a different part of the formula to input that first. (Non-empty parts of the formula can be selected to be overwritten.)

Or, if you have changed your mind, click "Clear latest" to cancel the application of this inference rule.

Or click “Clear all” to start over.

Choose a conjunct in the already existing part of the proof. The options are shown on a black background.

Or, if you have changed your mind, choose an alternative to this inference rule.

Or click “Clear all” to start over.

None of the lines in the existing part of the proof has a conjunction as its main connective. You therefore cannot continue with the application of this rule.

Instead, choose another inference rule to be applied.

Or add a premise or an assumption.

Or click “Clear all” to start over.

Congratulations, you have proved the displayed sequent!

Click "Clear all" to begin another proof.

Or, if you have changed your mind, "unfinish" the proof by clicking "Clear latest", and add more lines.

Or click on “Download/upload” or “Settings” to see more options.

Click "Clear all" to begin another proof.

Or "unfinish" the proof by clicking "Clear latest", and add more lines.

Or click on “Download/upload” or “Settings” to see more options.

Click here to download the proof as plain text.

Click here to download the proof as LaTeX code.

Click here to download the proof as a file that can later be uploaded to this editor.

Click here to upload a previously downloaded proof.