Tags: definition-interpretation python declaration class

DefinitionInterpretationDeclaration (python class)

This section presents the DefinitionInterpretationDeclaration python class.

This class models the declaration of the definition-interpretation inference-rule in the target universe-of-discourse.

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

class punctilious.DefinitionInterpretationDeclaration(u, echo=None)

This python class models the declaration of the definition-interpretation inference-rule in a universe-of-discourse.

Inherits from InferenceRuleDeclaration .

TODO: DefinitionInterpretation (Declaration and Inclusion): Add a data validation step to assure that term p is propositional. TODO: DefinitionInterpretation (Declaration and Inclusion): Add a verification step: the axiom is not locked.

class Premises(d: FlexibleDefinition, x: FlexibleFormula, y: FlexibleFormula)

This python NamedTuple is used behind the scene as a data structure to manipulate the premises required by the inference-rule .

d: Union[punctilious.core.DefinitionDeclaration, punctilious.core.DefinitionInclusion, str]: Alias for field number 0

x: Union[punctilious.core.Formula, punctilious.core.FormulaStatement, punctilious.core.CompoundFormula, tuple, list]: Alias for field number 1

y: Union[punctilious.core.Formula, punctilious.core.FormulaStatement, punctilious.core.CompoundFormula, tuple, list]: Alias for field number 2

construct_formula(d, x, y)

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