Skip to content
๐Ÿ” Inference Rules

๐Ÿ” Inference Rules

Inference rules are the formal templates that govern how valid conclusions are derived from known premises. They form the syntactic backbone of mathematical proofs, logical arguments, and audit logic systems. Each rule defines a structurally sound transformation, ensuring that truth is preserved from input to output.


๐Ÿง  Structural Principle

Inference rules operate independently of the content of the statements. They apply to logical form, not semantic meaning.

This modularity makes them ideal for:

  • Proof construction
  • Predicate logic evaluation
  • Programming and AI reasoning
  • Ethical and legal audit frameworks

๐Ÿงฉ Categories of Inference Rules

1. Propositional Logic Rules

These work with whole statements (propositions) and logical connectives.

Rule NameFormSemantic Flag
Modus Ponens

(Implication Elimation)
If $p \rightarrow q$ and $p$, then $q$Direct Implication
Modus Tollens

(Contrapositive)
If $p \rightarrow q$ and $\neg q$, then $\neg p$If the conclusion is not true, the precondition didnt happen
Hypothetical Syllogism

(Chain Reasoning)
If $p \rightarrow q$ and $q \rightarrow r$, then $p \rightarrow r$Transitive Property
Disjunctive Syllogism

(Conjunctive Elimination)
If $p \lor q$ and $\neg p$, then $q$Eliminate the already false in an OR statement
Conjunction

(Conjunctive Introduction)
If $p$ and $q$, then $p \land q$Combine Truths
Simplification

(Conjunctive Elimination)
If $p \land q$, then $p$Eliminate the already true in an AND statement
Addition

(Disjunctive Introduction)
If $p$, then $p \lor q$Add any other condition, as one is already True

2. Predicate Logic Rules

These extend propositional rules to include quantifiers and variables.

Rule NameFormSemantic Flag
Universal InstantiationFrom $\forall x,\;P(x)$ infer $P(a)$<code>#quantifier-unpack</code>
Existential InstantiationFrom $\exists x,\;P(x)$ infer $P(a)$ (with scope)<code>#quantifier-unpack</code>
Universal GeneralizationFrom $P(x)$ for arbitrary $x$, infer $\forall x,\;P(x)$<code>#quantifier-pack</code>
Existential GeneralizationFrom $P(a)$, infer $\exists x,\;P(x)$<code>#quantifier-pack</code>

๐Ÿ” Predicate rules require careful handling of variable scope and instantiation.


๐Ÿงช Audit Examples

Modus Ponens

  • Premises:
    • $p$: “It is raining”
    • $p \rightarrow q$: “If it is raining, the ground is wet”
  • Conclusion:
    • $q$: “The ground is wet”

Disjunctive Syllogism

  • Premises:
    • $p \lor q$: “It is either raining or sunny”
    • $\neg p$: “It is not raining”
  • Conclusion:
    • $q$: “It is sunny”

๐Ÿง  Why Inference Rules Matter

  • Soundness: Guarantees that conclusions are valid if premises are true
  • Modularity: Enables chaining, nesting, and audit tracing
  • Teachability: Each rule is a reusable pattern for reasoning
  • Cross-domain utility: Applies to logic, ethics, programming, and law
Last updated on