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
conclusionformula, 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.