# LP, the Larch Prover -- Proofs by contradiction

Proofs by contradiction provide an indirect method of proof. The command
`prove F by contradiction` directs LP to prove a formula `F` by deriving
an inconsistency from LP's logical system supplemented
by the hypothesis `~F'`, where `F'` is the result of substituting new
constants for the free variables in `F`. (This hypothesis
is logically equivalent to the negation of `F` because introducing new
constants is equivalent to replacing the implicit universal quantifiers by
existential quantifiers.) The name of the hypothesis has the form
<simpleId>`ContraHyp.`<number>, where <simpleId> is the current value
of the name-prefix setting.
The command `resume by contradiction` directs LP to resume the proof of the
current conjecture by contradiction.