This page does not represent the most current semester of this course; it is present merely as an archive.
Proof techniques we’ve learned so far:
See also MCS 3.3 and MCS 3.4.2, our list of equivalences, and our guide to direct proof.
In a small step proof, write an equivalent expression and cite the rule used to reach it. If several rules are needed, write them out one by one.
The following uses a note per line to show how it is equivalent to the preceding line
| 1 | A \lor (B \lor C) | |
| 2 | (A \lor B) \lor C | Associative property of \lor |
| 3 | (B \lor A) \lor C | Commutative property of \lor |
| 4 | B \lor (A \lor C) | Associative property of \lor |
| 5 | (\lnot (\lnot B)) \lor (A \lor C) | Double negation |
| 6 | (\lnot B) \rightarrow (A \lor C) | Disjunction to implication |
In a prose proof, write the original and the new expression, separated by can be re-written as
or is equivalent to
. Only include intermediate steps or identified proof rules if you believe your audience would take more than a few minutes to figure them out themselves. Common shortcut phrases for guiding through steps include
This is the same example as the previous one, but written in prose style instead.
A \lor (B \lor C) can be re-written as (\lnot \lnot B) \lor (A \lor C), which is equivalent to (\lnot B) \rightarrow A \lor C by the equivalence of implication and disjuction.
See also our list of entailments.
Applying entailment is very much like applying equivalence rule, except it only needs to work in one direction. Because A \equiv B implies A \vDash B, you can use equivalence rules in a proof that applies entailment.
There are many more entailments (sometimes called proof rules
or inference rules
) than there are equivalence rules, so using them can make proof construction much easier than limiting yourself to equivalences.
A proof that only uses proof rules is sometimes called a direct proof.
See also MCS 1.7, ∀x 17.5, and our proof of one of De Morgan’s laws
State a disjunctive tautology. For a simple tautology like P \lor \lnot P, stating it is enough; for more complicated tautologies, you may need to add a sub-proof or lemma1 that it is tautological.
Then proceed to consider several cases: one for each term of the disjunctive tautology, in each case assuming that that clause is true.
After completing all of the cases, the full proof is also completed: we may not know which case’s assumption is true, but because the disjunction is a tautology, we know at least one of them must be.
This is a full proof of one of our known equivalences
P \rightarrow Q \equiv \lnot P \lor Q
Either P is true or P is false.
The expression P \rightarrow Q in this case is equivalent to \top \rightarrow Q, which can be simplified to Q.
The expression \lnot P \lor Q in this case is equivalent to \bot \lor Q, which can be simplified to Q.
Since the two are equivalent to the same thing, they are equivalent to each other.
The expression P \rightarrow Q in this case is equivalent to \bot \rightarrow Q, which can be simplified to \top.
The expression \lnot P \lor Q in this case is equivalent to \top \lor Q, which can be simplified to \top.
Since the two are equivalent to the same thing, they are equivalent to each other.
Since P \rightarrow Q \equiv \lnot P \lor Q is true in both cases, it is true in general.
Case analysis in small-step proofs involves embedded sub-proofs, as is described in ∀x 17.5 and used in ∀x 17.1 and ∀x 19.6.
a lemma is a helper proof made before the main proof it will be used inside of↩︎