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.