Welcome to QED, a short interactive text in propositional logic arranged in the format of a computer game.

Propositional logic is the logic of atomic propositions (which in this text are given names such as A, B, or C) and the statements one can form from these propositions using logical connectives such as AND, OR, and IMPLIES. It is a subset of first-order logic, which is the main form of logic used in mathematics.

The objective of this "game" is to prove statements in propositional logic from the given hypotheses by clicking and dragging on statements that one has already deduced. By solving exercises in this game, you should develop a greater understanding of propositional logic.

Click on the "Exercise 1.1" button above to begin the text and start the sequence of exercises!

Version notes:

Version 1.0 (released July 28, 2018). Beta release.

Version 1.1 (released July 29, 2018). Tests if local storage is supported. Exercise 7.2 repaired (and all subsequent exercises now accessible). All exercise buttons now visible (not just unlocked ones). Spelling corrections.

Version 1.2 (released July 29, 2018). Achievements and notifications windows now side-by side. Achievements now list from newest to oldest rather than vice versa. "No available deductions" response added. Clicking on deductions no longer creates duplicates (thanks to ahartel for this suggestion). Some clarifications added to text. Best known proof lengths added. Exercises 5.1 and 12.1(c) corrected; other minor corrections. Some new exercises added.

Version 1.2.1 (released July 29, 2018). New records for Exercises 7.2, 9.2(a), 12.2(b), 12.2(c), 12.4(b), 12.6(c). Some incorrect proof lengths fixed.

Version 1.2.2 (released July 29, 2018). New record for Exercise 12.6(a). A typo causing exercises to not load beyond 12.2(b) has been repaired. (Thanks to William Chargin for pointing out the issue and providing a fix.)

If the text has updated to a new version since your last session, you may need to reset the text in order for it to work correctly.