Inference Rule Calculus¶
Formal calculus — instantiates Formal Derivation System Design
Declares the finite set of inference rules that license moving from accepted expressions to new ones, and thereby fixes exactly what is derivable in the system.
An Inference Rule Calculus is the declarative logic of licensed moves. Each rule has the shape "given premises matching these patterns, you may assert this conclusion," and the finite collection of such rules — together with the axioms — determines the entire set of derivable statements: the system's closure. Its defining commitment is that it declares rather than executes: it says which steps are permitted and, by consequence, what is and is not provable, but it runs nothing. It is order-independent, direction-neutral, and silent about strategy — a specification of the derivability relation ⊢, not a machine that computes it.
Example¶
An authorization platform decides who may act on which resource by derivation. Its facts are statements like owns(alice, doc1), and its calculus is a small set of inference rules stated as premise-patterns over a conclusion:
- from
owns(P, R)infermayRead(P, R); - from
mayRead(P, R)anddelegates(P, Q, R)infermayRead(Q, R); - from
role(P, editor)andresource(R, project X)infermayWrite(P, R).
The calculus itself is just these rules. What it fixes is the closure: the complete set of mayRead/mayWrite facts derivable from any given collection of ownership and delegation facts. When a security reviewer asks "could a contractor ever end up able to write to the finance folder?", the question is answered entirely by inspecting the rules and the closure they generate — no execution trace required, because the calculus already pins down the boundary of the derivable.
How it works¶
- Rules as schemas. Each inference rule is a pattern: premise shapes above the line, a conclusion shape below, with metavariables shared across them. A rule matches whenever accepted expressions fit its premise shapes.
- Declared, not run. The calculus states which single steps are legal. It does not choose which rule to apply next or in what order — that operational question belongs elsewhere.
- Closure by consequence. The axioms plus the rules define the derivable set: everything reachable by finitely many rule applications. Adding or removing a rule redraws that boundary, which is why the rules and the closure are two faces of one artifact.
- Truth-preservation intent. Rules are chosen so that if the premises hold, the conclusion is meant to hold — soundness is a design goal the calculus is answerable to, later audited by metatheory.
Tuning parameters¶
- Expressiveness vs. decidability — richer rules (recursion, negation, quantifiers) enlarge what can be said but can make derivability undecidable. Restraint keeps the closure computable.
- Rule minimality — a small primitive set vs. many convenient derived rules. Fewer primitives ease metatheoretic analysis; admissible shortcuts ease everyday derivation.
- Admissibility policy — whether derived rules may be added as shortcuts. Admissible rules speed proofs without changing the closure, but obscure what is primitive.
- Directionality — whether rules are read only forward (premises → conclusion) or also used backward for goal-directed search. Bidirectional reading aids proof search but complicates the presentation.
When it helps, and when it misleads¶
Its strength is making "what follows" fully inspectable and closed: given the rules, the set of derivable statements is determined, so questions about reach — can this ever be concluded? — become questions about the rules, not about anyone's judgment.
Its failure mode is an over-powerful rule whose consequences outrun intuition. A single rule that licenses slightly too much can silently enlarge the closure — the authorization example's real danger is a delegation rule that permits an unintended privilege-escalation chain nobody traced by hand.[n1] Rules also interact: two individually reasonable rules can combine into derivations no one anticipated. The classic misuse is bolting on a convenient rule to make one derivation succeed, without asking what else the enlarged closure now contains. The guarding discipline is to treat every rule change as a change to the closure boundary and to hand the result to a consistency check and independent verification rather than eyeballing it.
How it implements the components¶
inference_rule_set— it is the finite collection of inference rules, each a premise-to-conclusion pattern that licenses a single derivation step.closure_boundary— by fixing the rules, it fixes the derivability relation, and thus the exact boundary between what is provable inside the system and what is not.
It declares which steps are licensed and what is provable, but it never runs anything: it does not execute rules into an actual result or step-log (derivation_trace_record) and it does not guard whether that execution terminates or is confluent (consistency_guardrail) — those belong to its nearest twin, the Rewrite or Transition Rule Engine.
Related¶
- Instantiates: Formal Derivation System Design — supplies the inference rules that define the system's derivability relation.
- Consumes: Formal Grammar Specification and Axiom Schema Catalog — the calculus operates over well-formed expressions, starting from the granted axioms.
- Sibling mechanisms: Formal Grammar Specification · Well-Formedness Linter · Axiom Schema Catalog · Rewrite or Transition Rule Engine · Proof Tree or Derivation Log · Mechanical Proof Checker · Metatheory Review Checklist · Consistency and Contradiction Test · Formal-System Change-Control Workflow
Editorial Notes¶
Form Classification¶
Form family: Rule, Policy & Commitment
Rationale: Inference Rule Calculus operates as a standing rule, threshold, contractual commitment, or policy constraint governing future conduct because it declares the finite set of inference rules that license moving from accepted expressions to new ones, and thereby fixes exactly what is derivable in the system
Independent corroboration: The frozen evidence defines Inference Rule Calculus as 'Declares the finite set of inference rules that license moving from accepted expressions to new ones, and thereby fixes exactly what is derivable in the system', so its operative form is Rule, Policy & Commitment.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Mathematics
Origin pattern: Convergent development
Present-day reach: Multi-domain
Rationale: Finite formal inference calculi were canonically developed in mathematical logic, including Gentzen's natural-deduction systems.
Related originating lineages:
- Computer Science & Software Engineering — Programming-language semantics, type systems, and automated deduction materially develop executable rule calculi.
- Philosophy — The normative study of valid inference and logical consequence materially underlies the calculus tradition.
Review resolution: Both independent reviews place the primary lineage in mathematics. The queued differences (alternate_origin_disagreement, domain_reach_disagreement) concern secondary metadata rather than primary provenance. The final retains philosophy, computer_science only where a reviewer supplied a formative-lineage rationale; this does not convert downstream applicability into origin. origin_mode=convergent because the reviewers document independently established or materially co-developing traditions. domain_reach=multi_domain records application breadth separately from provenance.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
[n1] Natural deduction, introduced by Gerhard Gentzen, presents a logic as a set of introduction and elimination rules for each connective rather than a long axiom list — the paradigm case of defining a system by its inference rules. Its discipline of stating each rule explicitly is precisely what makes the closure it generates inspectable. ↩