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.