# propositions.deduction module¶

Useful proof manipulation maneuvers in Propositional Logic.

`propositions.deduction.``prove_corollary`(antecedent_proof, consequent, conditional)

Converts the given proof of a formula `antecedent` to a proof of the given formula `consequent` by using the given assumptionless inference rule of which `'(``antecedent``->``consequent``)'` is a specialization.

Parameters
• antecedent_proof (`Proof`) – valid proof of `antecedent`.

• consequent (`Formula`) – formula to prove.

• conditional (`InferenceRule`) – assumptionless inference rule of which the assumptionless inference rule with conclusion `'(``antecedent``->``consequent``)'` is a specialization.

Return type

`Proof`

Returns

A valid proof of `consequent` from the same assumptions as the given proof, via the same inference rules as the given proof and in addition `MP` and `conditional`.

`propositions.deduction.``combine_proofs`(antecedent1_proof, antecedent2_proof, consequent, double_conditional)

Combines the given proofs of two formulas `antecedent1` and `antecedent2` into a proof of the given formula `consequent` by using the given assumptionless inference rule of which `'(``antecedent1``->(``antecedent2``->``consequent``))'` is a specialization.

Parameters
• antecedent1_proof (`Proof`) – valid proof of `antecedent1`.

• antecedent2_proof (`Proof`) – valid proof of `antecedent2` from the same assumptions and inference rules as `antecedent1_proof`.

• consequent (`Formula`) – formula to prove.

• double_conditional (`InferenceRule`) – assumptionless inference rule of which the assumptionless inference rule with conclusion `'(``antecedent1``->(``antecedent2``->``consequent``))'` is a specialization.

Return type

`Proof`

Returns

A valid proof of `consequent` from the same assumptions as the given proofs, via the same inference rules as the given proofs and in addition `MP` and `double_conditional`.

`propositions.deduction.``remove_assumption`(proof)

Converts the given proof of some `conclusion` formula, the last assumption of which is an assumption `assumption`, to a proof of `'(``assumption``->``conclusion``)'` from the same assumptions except `assumption`.

Parameters

proof (`Proof`) – valid proof to convert, with at least one assumption, via some set of inference rules all of which have no assumptions except perhaps `MP`.

Return type

`Proof`

Returns

A valid proof of `'(``assumption``->``conclusion``)'` from the same assumptions as the given proof except the last one, via the same inference rules as the given proof and in addition `MP`, `I0`, `I1`, and `D`.

`propositions.deduction.``prove_from_opposites`(proof_of_affirmation, proof_of_negation, conclusion)

Combines the given proofs of a formula `affirmation` and its negation `'~``affirmation``'` into a proof of the given formula.

Parameters
• proof_of_affirmation (`Proof`) – valid proof of `affirmation`.

• proof_of_negation (`Proof`) – valid proof of `'~``affirmation``'` from the same assumptions and inference rules of `proof_of_affirmation`.

• conclusion (`Formula`) – formula to prove.

Return type

`Proof`

Returns

A valid proof of `conclusion` from the same assumptions as the given proofs, via the same inference rules as the given proofs and in addition `MP` and `I2`.

`propositions.deduction.``prove_by_way_of_contradiction`(proof)

Converts the given proof of `'~(p->p)'`, the last assumption of which is an assumption `'~``formula``'`, to a proof of `formula` from the same assumptions except `'~``formula``'`.

Parameters

proof (`Proof`) – valid proof of `'~(p->p)'` to convert, the last assumption of which is of the form `'~``formula``'`, via some set of inference rules all of which have no assumptions except perhaps `MP`.

Return type

`Proof`

Returns

A valid proof of `formula` from the same assumptions as the given proof except the last one, via the same inference rules as the given proof and in addition `MP`, `I0`, `I1`, `D`, and `N`.