InferenceRuleInclusionCollection (python class)
- class punctilious.InferenceRuleInclusionCollection(t)
This python class models the collection of inference-rules included in a theory-derivation.
In complement, it conveniently exposes as python properties a catalog of natively supported inference-rules that are automatically included in the theory-derivation when they are accessed for the first time.
- property absorb: punctilious.core.AbsorptionInclusion
The well-known absorption inference-rule: (P ⟹ Q) ⊢ (P ⟹ (P ∧ Q)).
Unabridged property: u.i.absorption
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property absorption: punctilious.core.AbsorptionInclusion
The well-known absorption inference-rule: (P ⟹ Q) ⊢ (P ⟹ (P ∧ Q)).
Abridged property: u.i.absorb
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property axiom_interpretation: punctilious.core.AxiomInterpretationInclusion
The axiom_interpretation inference-rule: 𝒜 ⊢ P.
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
Warning
This inference-rule is interpretative, i.e.: it interprets a truth expressed in natural-language (e.g.: an axiom, or a definition) and translates it to a formula-statement. Theory authors must be critically attentive to the semantic accuracy of this interpretation . In effect, punctilious does not verify semantic consistency, it only covers syntactical consistency.
In straightforward language, one may introduce arbitrary statements in a theory with interpretative inference-rules.
- Return type
- property bel: punctilious.core.BiconditionalElimination1Inclusion
The well-known biconditional-elimination #1 inference-rule: P ⟺ Q ⊢ P ⟹ Q.
Unabridged property: u.i.biconditional_elimination_1
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property ber: punctilious.core.InferenceRuleInclusion
The well-known biconditional-elimination #2 inference-rule: P ⟺ Q ⊢ Q ⟹ P.
Unabridged property: u.i.biconditional_elimination_2
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property bi: punctilious.core.BiconditionalIntroductionInclusion
The well-known biconditional-introduction inference-rule: : P ⟹ Q, Q ⟹ P ⊢ P ⟺ Q.
Unabridged property: u.i.biconditional_introduction
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property biconditional_elimination_1: punctilious.core.BiconditionalElimination1Inclusion
The well-known biconditional-elimination #1 inference-rule: P ⟺ Q ⊢ P ⟹ Q.
Abridged property: u.i.bel
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property biconditional_elimination_2: punctilious.core.BiconditionalElimination2Inclusion
The well-known biconditional-elimination #2 inference-rule: P ⟺ Q ⊢ Q ⟹ P.
Abridged property: u.i.ber()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property biconditional_introduction: punctilious.core.BiconditionalIntroductionInclusion
The well-known biconditional-introduction inference-rule: : P ⟹ Q, Q ⟹ P ⊢ P ⟺ Q.
Abridged property: u.i.bi
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property cd: punctilious.core.ConstructiveDilemmaInclusion
The well-known constructive-dilemma inference-rule
Unabridged property: universe_of_discourse.inference_rule.constructive_dilemma(…)
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property cel: punctilious.core.ConjunctionElimination1Declaration
The well-known conjunction-elimination #1 inference-rule: (P ∧ Q) ⊢ P.
Unabridged property: universe_of_discourse.inference_rule.conjunction_elimination_1()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property cer: punctilious.core.ConjunctionElimination2Inclusion
The well-known conjunction-elimination #2 inference-rule: P ∧ Q ⊢ Q.
Unabridged property: universe_of_discourse.inference_rule.conjunction_elimination_2()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property ci: punctilious.core.ConjunctionIntroductionInclusion
The well-known conjunction-introduction inference-rule: P, Q ⊢ P ∧ Q.
Unabridged property: universe_of_discourse.inference_rule.conjunction_introduction()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property conjunction_elimination_1: punctilious.core.ConjunctionElimination1Inclusion
The well-known conjunction-elimination #1 inference-rule: P ∧ Q ⊢ P.
Abridged property: t.i.cel()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property conjunction_elimination_2: punctilious.core.ConjunctionElimination2Inclusion
The well-known conjunction-elimination #2 inference-rule: P ∧ Q ⊢ Q.
Abridged property: t.i.cer
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property conjunction_introduction: punctilious.core.ConjunctionIntroductionInclusion
The well-known conjunction-introduction inference-rule: P, Q ⊢ P ∧ Q.
Abridged property: t.i.ci()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property constructive_dilemma: punctilious.core.ConstructiveDilemmaInclusion
The well-known constructive-dilemma inference-rule
Abridged property: t.i.cd()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property definition_interpretation: punctilious.core.DefinitionInterpretationInclusion
The definition_interpretation inference-rule: 𝒟 ⊢ (P = Q).
If the inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
Warning
This inference-rule is interpretative, i.e.: it interprets a truth expressed in natural-language (e.g.: an axiom, or a definition) and translates it to a formula-statement. Theory authors must be critically attentive to the semantic accuracy of this interpretation . In effect, punctilious does not verify semantic consistency, it only covers syntactical consistency.
In straightforward language, one may introduce arbitrary statements in a theory with interpretative inference-rules.
- Return type
- property destructive_dilemma: punctilious.core.DestructiveDilemmaInclusion
The well-known destructive-dilemma inference-rule
Abridged property: t.i.cd()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property double_negation_elimination: punctilious.core.DoubleNegationEliminationInclusion
The well-known double-negation-elimination inference-rule: ¬¬P ⊢ P.
Abridged property: t.i.dne()
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property double_negation_introduction: punctilious.core.DoubleNegationIntroductionInclusion
The well-known double-negation-introduction inference-rule: P ⊢ ¬¬P.
Abridged property: t.i.dni
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property modus_ponens: punctilious.core.ModusPonensInclusion
The well-known modus-ponens inference-rule: (P ⟹ Q), P ⊢ Q.
Abridged property: u.i.mp
The implication (P ⟹ Q) may contain variables. If such is the case, the resulting Q’ is computed by extracting variable-values from P’ and applying variable-substitution.
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property mp: punctilious.core.ModusPonensInclusion
The well-known modus-ponens inference-rule: (P ⟹ Q), P ⊢ Q.
Unabridged property: u.i.modus_ponens
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property pbc: punctilious.core.ProofByContradiction1Inclusion
Unabridged property: u.i.proof_by_contradiction
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property pbr: punctilious.core.ProofByRefutation1Inclusion
Unabridged property: u.i.proof_by_refutation
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property proof_by_contradiction_1: punctilious.core.ProofByContradiction1Inclusion
Abridged property: u.i.pbc
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property proof_by_refutation_1: punctilious.core.ProofByRefutation1Inclusion
Abridged property: u.i.pbr
If the well-known inference-rule does not exist in the universe-of-discourse, the inference-rule is automatically declared.
- Return type
- property variable_substitution: punctilious.core.VariableSubstitutionInclusion
- Return type