Inference rules¶

Instead of grinding truth tables, Algae reasons with inference rules: small, fixed steps you chain into a proof. This chapter is about what a rule is — its shape, and how to read it — using conjunction as the running example. We won’t run the checker yet; we’re learning to read.

Sequents and the turnstile `⊢`¶

Everything you prove is a sequent, written with a turnstile ⊢ (ASCII |-):

context ⊢ proposition

Read it “under the context, the proposition holds.” The proposition on the right is the goal — what you’re trying to establish. The context on the left lists what you’re allowed to assume: typed variables and named hypotheses. When there’s nothing to assume, the context is empty and you just write ⊢ proposition.

⊢ A ∧ B                    -- prove A ∧ B, no assumptions
x := A ⊢ A                 -- assuming a proof x of A, prove A
n : Nat, ih := P(n) ⊢ P(s(n))   -- given a number n and a proof of P(n), prove P(s(n))

Two kinds of thing live in a context. A variable like n : Nat is a term you may use. A hypothesis like ih := P(n) is evidence — a proof you’ve been handed and may cite by its name (here ih). Keep those apart: n is a number, ih is a proof.

Anatomy of a rule¶

An inference rule is a fixed pattern with premises above a line and a conclusion below it:

premise₁     premise₂     …     premiseₙ
─────────────────────────────────────────
               conclusion

Read top-to-bottom it says: if you can establish all the premises, then you may conclude the conclusion. Each premise and the conclusion is itself a sequent. A rule with no premises is an axiom — an unconditional fact, true on its own with nothing to establish first.

Conjunction, in words and in Algae¶

Take the rule that builds a conjunction. In words:

To prove ``A ∧ B`` you need a proof of ``A``, and a proof of ``B``.

That is two premises (a proof of A; a proof of B) and one conclusion (A ∧ B). As an inference rule:

⊢ A          ⊢ B
─────────────────────
     ⊢ A ∧ B

Algae writes exactly this. Here is and_intro from the standard library’s core module (and introduction — the rule that introduces a ∧):

rule and_intro(
  P Q : Prop
)
  ⊢ P;
  ⊢ Q
  ────────────────────────
  ⊢ P ∧ Q
end;

Piece by piece:

rule and_intro(…) names the rule and lists its parameters in parentheses. P Q : Prop declares two propositions P and Q — the placeholders the rule is stated over.
The lines above the ──── bar are the premises, separated by ; — here ⊢ P and ⊢ Q.
The line below the bar is the conclusion, ⊢ P ∧ Q.
end; closes the rule. (An axiom has no bar and no premises, and ends with a plain ; instead — you’ll meet refl that way later.)

The bar is just dashes

The separator is a run of ─ (or ASCII -); its exact length carries no meaning. And the parameters P, Q are schematic — the rule works for any propositions you plug in, not two specific ones.

The companion rules take a conjunction apart again. and_left recovers the left half and and_right the right — one premise each (the conjunction), one conclusion (the half):

rule and_left(
  P Q : Prop
)
  ⊢ P ∧ Q
  ────────────────────────
  ⊢ P
end;

That “build one / use one” pairing — an introduction rule and an elimination rule per connective — runs through the whole logic module. You’ll see it again in The logical toolkit.

So a rule is a template: premises on top, conclusion on the bottom, schematic parameters standing in for the specifics. The next chapter puts one to work — and reveals that in a proof you read these rules bottom-to-top.

Inference rules¶

Sequents and the turnstile ⊢¶

Anatomy of a rule¶

Conjunction, in words and in Algae¶

Sequents and the turnstile `⊢`¶