# 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 is `assumption`, to a proof of `'(``assumption``->``conclusion``)'` from the same assumptions except `assumption`.

Parameters
• proof (`Proof`) – valid proof to convert, from assumptions/axioms that include `AXIOMS`.

• 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 that is free in this assumption.

Return type

`Proof`

Returns

A valid proof of `'(``assumption``->``conclusion``)'` from the same assumptions/axioms as the given proof except `assumption`.

`predicates.deduction.``proof_by_way_of_contradiction`(proof, assumption, print_as_proof_forms=False)

Converts the given proof of a contradiction, an assumption of which is `assumption`, to a proof of `'~``assumption``'` from the same assumptions except `assumption`.

Parameters
• proof (`Proof`) – valid proof of a contradiction (i.e., a formula whose negation is a tautology) to convert, from assumptions/axioms that include `AXIOMS`.

• 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 that is free in this assumption.

Return type

`Proof`

Returns

A valid proof of `'~``assumption``'` from the same assumptions/axioms as the given proof except `assumption`.