predicates.deduction module¶
Useful proof manipulation maneuvers in Predicate Logic.

predicates.deduction.
remove_assumption
(proof, assumption, print_as_proof_forms=False)¶ Converts the given proof of some
conclusion
formula, an assumption of which isassumption
, to a proof of'(
assumption
>
conclusion
)'
from the same assumptions exceptassumption
. Parameters
proof (
Proof
) – valid proof to convert, from assumptions/axioms that includeAXIOMS
.assumption (
Formula
) – formula that is a simple assumption (i.e., without any templates) of the given proof, such that no line of the given proof is a UG line over a variable name that is free in this assumption.print_as_proof_forms (
bool
) – flag specifying whether the proof of'(
assumption
>
conclusion
)'
is to be printed in real time as it is being created.
 Return type
 Returns
A valid proof of
'(
assumption
>
conclusion
)'
from the same assumptions/axioms as the given proof exceptassumption
.

predicates.deduction.
prove_by_way_of_contradiction
(proof, assumption)¶ Converts the given proof of a contradiction, an assumption of which is
assumption
, to a proof of'~
assumption
'
from the same assumptions exceptassumption
. Parameters
proof (
Proof
) – valid proof of a contradiction (i.e., a formula whose negation is a tautology) to convert, from assumptions/axioms that includeAXIOMS
.assumption (
Formula
) – formula that is a simple assumption (i.e., without any templates) of the given proof, such that no line of the given proof is a UG line over a variable name that is free in this assumption.
 Return type
 Returns
A valid proof of
'~
assumption
'
from the same assumptions/axioms as the given proof exceptassumption
.