More reasoning with Prooftoys

Contents

In the descriptions of rules of inference, capital letters A, B, and C are variables with boolean (true/false) values. The letters x and y are used for variables of any type. You can supply any term you choose for capital letters X and Y without the need to follow the usual rules for substitution.

Some basic facts

The value of any expression is equal to itself. This is often a good way to start a proof that A is equal to something else. Keep replacing one side (usually the right) with something else that is equal to it.

When working with equality in Prooftoys it is important to remember that equivalence (==) is the same concept as equality applied to true/false values.

There are also numerous facts about quantifiers that work as rewrite rules using an extended form of matching, described TBD.

Tautologies

Proving A and B

If statements A and B are both proved, how can I prove the statement A & B?

Removing irrelevant assumptions

If a conditional fact has an assumption with a variable that only appears (free) in that assumption and nowhere else in the statement of the fact, that assumption can be safely be removed. We can suggest the working of the inference like this:

The one limitation is that there must be some value for the variable that can make the irrelevant assumption true. So to use this rule in a proof, there must be a proof that such a value exists. Prooftoys currently supports a couple of common cases. These are useful cases, and Prooftoys can work out the existence fact on its own. The cases are:

In both cases, the variable var does not appear in the fact outside this one assumption.

For every assumption of these kinds, the existence of a value satisfying it is provable, so we can remove the assumption from the proof step.

Definitions

Adding a new axiom

[[discuss]]