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.
Expand the "Sections and exercises" section above and then click on the "Exercise 1.1" button to begin the text and start the sequence of exercises!
The current version is 2.0.2.
Version 2.0.2 (released Aug 21, 2018) Code moved to Github, now under an MIT license.
Version 2.0.1 (released Aug 20, 2018) Meta-key now has same functionality as CTRL-key (for Mac users). (Thanks to Jacob H. for the suggestion.)
Version 2.0 (released Aug 18, 2018) Cleaned up version of Version 1.17, hopefully stable release.
Version 1.17 (released Aug 16, 2018) Alpha version of Section 24, introducing the equality relation.
Version 1.16.1 (released Aug 15, 2018) New records for 22.4(ae), using some additional formulas that were not previously available until the predicates and operators window was unlocked. (These formulas have since been added to the problem.)
Version 1.16 (released Aug 13, 2018) Alpha version of Section 23, introducing the predicates and operators window.
Version 1.15.5 (released Aug 13, 2018) New record for 22.6(b). Spelling corrections.
Version 1.15.4 (released Aug 13, 2018) Text for Exercise 22.4(ce) and 22.5(a) fixed (thanks to Anders Kaseorg for pointing out the issue). Three new exercises added to Section 22.
Version 1.15.3 (released Aug 12, 2018) New records for Exercises 22.4(acd), 22.5(c). Text for Exercise 22.4(c) fixed.
Version 1.15.2 (released Aug 12, 2018) New records for Exercises 18.4, 22.2. Further bug in universal specification legality checking patched (thanks to Andre Maute for reporting the error), as well as a technical bug in the search-and-replace code. UI for pull (arbitrary variables) changed.
Version 1.15.1 (released Aug 12, 2018) Bug with variable matching fixed (thanks to dP dt and Andre Maute for reporting the error). Also patched bugs in universal specification and universal introduction (thanks to dP dt for reporting the first error).
Version 1.15 (released Aug 11, 2018) Alpha version of Section 22, introducing the existential introduction law (the first law in which one can have multiple deductions from a single choice of inputs for reasons other than permutation of the inputs). Several "invisible" changes to data structures. Some helper exercises in earlier sections added.
Version 1.14.3 (released Aug 9, 2018) Sections and exercises layout revamped (thanks to dP dt for the suggestion). Exercises now come with the section title as well.
Version 1.14.2 (released Aug 9, 2018) Instructions for Exercise 21.1 corrected (thanks to Andrew Lei for pointing out the error). Link to blog post added at bottom of page (thanks to dP dt for the suggestion).
Version 1.14.1 (released Aug 9, 2018) More accurate discussion of boolean duality in Exercise 12.5(d). New record for Exercise 18.6. Enforced a further requirement in the law of universal specification, namely that the term one specifies also cannot use free variables that are not recognised by the current environment (thanks to Pranjal Vachaspati for discovering this issue).
Version 1.14 (released Aug 9, 2018) Alpha versions of Sections 20, 21 added, introducing a "pull" law and also an existence law to rule out empty domains of discourse. Section 13 rearranged and expanded, with a new helper exercise (13.2(b)) that shortens some subsequent proofs. Enforced an important requirement in the law of universal specification, namely that the term one specifies to cannot involve bound variables.
Version 1.13.1 (released Aug 8, 2018) Text of Exercise 19.1 fixed. Double push exercise added in Exercise 15.2. Deductions resulting in ill-formed statements will now be displayed but grayed out, rather than hidden completely (thanks to Keith Winstein for this suggestion). Layout of main windows rearranged.
Version 1.13 (released Aug 7, 2018) Alpha version of Section 19 added, introducing the existential quantifier and the ability to instantiate an existential statement using a "setting" environment. Section 10 reorganised with a new exercise intended to shorten the proofs of subsequent exercises proving IFF statements (in particular, several exercises in Section 10 onwards (particularly those whose conclusion involves IFF) now have shorter proofs). New hotkeys: 'n' for first available unsolved exercise, 'N' for last available unsolved exercise. New record for 9.5(a). Bug with new free and bound variables in Exercise 18.2(a) fixed, as well as incorrect text for Exercise 18.4 (thanks to Keith Winstein for reporting these bugs).
Version 1.12 (released Aug 7, 2018) Alpha version of Section 18 added, introducing the ability to specialise a universal statement to a term. Primitive terms also introduced.
Version 1.11 (released Aug 7, 2018) Alpha version of Section 17 added, introducing the ability to introduce a universal quantifier over a bound variables (which is now equipped with a button to generate such variables). Some bugs with finding available deductions fixed. Alternate push law functionality added in which one can push to an environment not yet created by dragging to a formula rather than to the environment. (As a consequence, Exercises 7.1 and 7.2 now have shorter proofs.) Bad hyperlink (to idempotence) fixed.
Version 1.10.1 (released Aug 6, 2018) An exploit involving enabling a deduction, undoing the previous deduction, then selecting a (now unjustified) deduction has been patched (thanks to Keith Winstein for finding the exploit). Some rewording for the Exercise 1.1 text (following suggestions by arch1).
Version 1.10 (released Aug 5, 2018) Alpha version of Section 16 added, introducing the ability to introduce free variables from a new Term window (which is also equipped with a button to generate new variables). Code separated into logic.js, which contains the GUI-independent components of the code, and gui.js, which contains the GUI-dependent components (for future modularity).
Version 1.9 (released Aug 4, 2018) Environments now clickable. Hotkeys "u" for immediate undo and "r" for restart. Alpha version of Sections 14, 15 added, introducing free variable environments and atomic sentences involving predicates and free variables, and a new PUSH law. Some bad hyperlinks (reported by Mauricio de Oliveira) repaired. Fixed a bug (reported by Matthew Steffen) regarding whether cloned laws qualified for non-circular proofs. Some laws taking a target environment as an input now have that environment removed in view of the clone functionality.
Version 1.8.1 (released Aug 4, 2018) Error in PUSH law (and other laws involving a non-root environment) fixed. (Thanks to Andre Maute for reporting the bug.)
Version 1.8 (released Aug 3, 2018) Restart exercise button added. Further "under the hood" changes. Laws with root environment default now come with a "clone" with one additional hypothesis that allows one to select the root environment.
Version 1.7.1 (released Aug 2, 2018) Can now use ctrl-click to select items, in particular allowing for more than two items to be selected. The numbers 1-9 are now keyboard shortcuts for the first 9 deductions in the Available deductions window.
Version 1.7 (released Aug 2, 2018). Dragging X to Y now also checks for laws available from dragging Y to X. Exercise 1.1 changed (so legacy players may artificially have beaten the shortest length now for this exercise). Various "under the hood" code changes in preparation for extension to first order logic. Various sections of game now collapsed by default.
Version 1.6.2 (released Aug 1, 2018). New records for Exercises 9.5(b), 10.1(b), 13.2(a), 13.3(a), 13.3(d). Duplicate unlocking of laws prevented. Table of boolean duality added to Exercise 12.5(d). Typo corrections.
Version 1.6.1 (released July 31, 2018). New records for Exercises 9.5(a), 13.3(a), 13.3(d).
Version 1.6 (released July 31, 2018). New 0-ary operators TRUE and FALSE; new exercises (and a new section) added.
Version 1.5.3 (released July 31, 2018). Rules appearing in text at or after an exercise can still be used, but have an asterisk attached to them and no longer trigger records.
Version 1.5.2 (released July 30, 2018). New record for Exercise 10.4.
Version 1.5.1 (released July 30, 2018). New record for Exercise 9.3(d). Improved backwards capability (game states from prior versions should now be able to re-unlock exercises and laws).
Version 1.5 (released July 30, 2018). Completing all exercises allows one to reveal the shortest known proofs. Some inaccuracies in the shortest known proofs corrected. A bug regarding the interaction between the UNDO button and the number of lines of the proof has been fixed.
Version 1.4 (released July 30, 2018). Exercises organised by section. Solved exercises are now green or blue depending on whether the shortest length was achieved. HTML links now open in a new tab so as not to disrupt game state. Immediate UNDO button added.
Version 1.3.2 (released July 30, 2018). New records for Exercises 2.2(b), 12.5(c). Clarifications and typo fixes to text.
Version 1.3.1 (released July 30, 2018). Implemented the styling suggestions of redblobgames.
Version 1.3 (released July 30, 2018). Newer record for Exercise 12.6(a). Bad hyperlink (pointed out by Andrew Lei) fixed. Successful proofs can now be expanded and collapsed in the notifications window.
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.)
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 (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 twice 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.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.0 (released July 28, 2018). Beta release.
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, or at least redo some of the exercises that unlock certain laws. This page works best when viewed on a large screen and with the ability to drag-and-drop; in particular, this page is unlikely to be all that functional on a cell phone. Also one may need a recently updated browser in order for the page to work properly (in particular, grid layouts and local storage should be supported for the best experience).
Further discussion this text may be found at this blog post.