Tags: biconditional-elimination-1 python inclusion class

BiconditionalElimination1Inclusion (python class)

See also

math concept | python declaration class | python sample

This section presents the BiconditionalElimination1Inclusion python class.

This class models the inclusion of the biconditional-elimination-1 inference-rule in the target theory-derivation.

Punctilious users do not need to instanciate objects from this class. In effect, the TheoryElaborationSequence class exposes the biconditional_elimination_1 property, and instanciation is automatic when this property is accessed for the first time.

class punctilious.BiconditionalElimination1Inclusion(t, echo=None, proof=None)

This python class models the inclusion of biconditional-elimination-1 as a valid inference-rule in a theory-derivation .

check_premises_validity(p_iff_q)

This python method verifies the validity of the premises. It is called by the python constructor of the InferredStatement python class to assure that formula-statements are inferred if and only if they are valid.

Returns True if the premises are valid and allow the execution of the inference algorithm. In this case, the constructor of the InferredStatement class will succeed and create an InferredStatement instance.

Returns False if the premises are not valid and do not allow the execution of the inference algorithm. In this case, the constructor of the InferredStatement class will fail and raise a PunctiliousException error.

Note

Note the critical distinction between the construct_formula and the infer_formula_statement methods. The former only verifies the syntactic correctness but does not verify the validity of the premises, it then applies the inference-rule algorithm, and produces a formula that may be invalid . The later verifies the validity of the premises, applies the inference-rule algorithm, and produces a formula-statement that is valid by definition.

Taking the modus-ponens inference-rule as an example, the construct_formula method requires two premise arguments: p_implies_q and p. One may pass a formula as the p_implies_q argument that is not valid in the theory-derivation under consideration, but that is syntactically correct. On the other hand, the infer_formula_statement method requires that both premise arguments be valid.

This distinction makes it possible to use the algorithms of inference-rules in “what if” scenarii, i.e. building invalid formulae. And at the same time, it assures that all formula_statements are valid.

Return type

Tuple[bool, Premises]

construct_formula(p_iff_q)

This python method verify the syntactic correctness of the premises, but does not verify the validity of the premises, it then applies the inference-rule algorithm, and returns a formula.

Note

Note the critical distinction between the construct_formula and the infer_formula_statement methods. The former only verifies the syntactic correctness but does not verify the validity of the premises, it then applies the inference-rule algorithm, and produces a formula that may be invalid . The later verifies the validity of the premises, applies the inference-rule algorithm, and produces a formula-statement that is valid by definition.

Taking the modus-ponens inference-rule as an example, the construct_formula method requires two premise arguments: p_implies_q and p. One may pass a formula as the p_implies_q argument that is not valid in the theory-derivation under consideration, but that is syntactically correct. On the other hand, the infer_formula_statement method requires that both premise arguments be valid.

This distinction makes it possible to use the algorithms of inference-rules in “what if” scenarii, i.e. building invalid formulae. And at the same time, it assures that all formula_statements are valid.

Return type

CompoundFormula

property i: punctilious.core.BiconditionalElimination1Declaration

Override the base class i property with a specialized inherited class type.

Return type

BiconditionalElimination1Declaration

infer_formula_statement(p_iff_q, ref=None, paragraph_header=None, subtitle=None, echo=None)

This python method verifies the syntactic correctness and validity of the premises, it then applies the inference-rule algorithm, and returns a formula-statement.

Note

Note the critical distinction between the construct_formula and the infer_formula_statement methods. The former only verifies the syntactic correctness but does not verify the validity of the premises, it then applies the inference-rule algorithm, and produces a formula that may be invalid . The later verifies the validity of the premises, applies the inference-rule algorithm, and produces a formula-statement that is valid by definition.

Taking the modus-ponens inference-rule as an example, the construct_formula method requires two premise arguments: p_implies_q and p. One may pass a formula as the p_implies_q argument that is not valid in the theory-derivation under consideration, but that is syntactically correct. On the other hand, the infer_formula_statement method requires that both premise arguments be valid.

This distinction makes it possible to use the algorithms of inference-rules in “what if” scenarii, i.e. building invalid formulae. And at the same time, it assures that all formula_statements are valid.