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.