Implement Modus Ponens Proof Step Checker

[wdcraft01]

The broader development/enhancement issue, of course, is the implementation of an independent general proof checker within the Prove-It system that would deal with all possible types of proof steps and rely on a relatively small (and thus easy -- or easier -- to check) block of code. We can begin, however, with the relatively simple but non-trivial Modus Ponens proof steps as a “demonstration of concept.” Immediate development tasks consist of: (1) deciding exactly where in the extant code to perform such a check; (2) where to “house” the checker code itself; and (3) where to “house” the resulting “check.” For example, concerning item (3), is it possible we might augment the Judgment class to hold a “Checked” object in addition to the expression, assumptions, and proof? And what might a “Checked” object look like? Perhaps “checked” just becomes a Boolean attribute of a Judgment?

[wwitzel]

I think the checker needs to be a separate package. It needs to be independent. It should share concepts but not code. For convenience, we may want to copy some small amounts of code (usually frowned upon, but I think it's justified in this case). We can store it in the same repository (at least initially, and certainly in the same GitHub organization). The main proveit package should call the checker to double-check itself as it makes derivation steps. But we need to be able to run the checker independently by reading data from Prove-It's database (which should really be overhauled as some point).