Natural deduction
This chapter builds a sequent-style natural deduction system for intuitionistic logic, with quantifiers. Each annotation that appears here was introduced in one of the design chapters.
Formulas
This theory has three sorts. Only seq, the sort of sequents, is provable.
Formulas and contexts are syntax, not assertions: a proof cannot assert a
bare wff. The sort system also rejects combinations such as a conjunction
of two sequents. Each connective carries an ASCII alias alongside its
Unicode notation.
Sequents and contexts
This cell declares judgment forms. A sequent like g ⊢ a is what deduction
rules actually derive. The other three judgments express equivalence: ↔
for formulas, ctx_eq for contexts, and ⟚ for sequents. The compiler uses
them to justify normalization. Because ↔ produces a seq, not a wff,
this theory cannot place an equivalence inside a formula such as a
conjunction or implication.
Contexts are built from single formulas (hence the coercion from wff to
ctx) with the join ,, whose @acui annotation makes them behave as sets:
order, grouping, and duplication are normalized when lines are checked. The
empty context is written _.
The equational layer
This follows the pattern of the Equality and
normalization chapter: a @relation bundle for
each equivalence judgment, plus the context laws the @acui annotation cited.
Only the sequent bundle carries a transport member, since seq is the only
provable sort. The @congr axioms assist with deeply nested rewrites: a
rewrite inside a formula lifts through hyp_congr and nd_congr to a ⟚ that
the transport can use.
The rules
The system is intuitionistic. Rules such as imp_elim combine the contexts
of their premises; and_intro uses the same context for both. ax is the
only deduction rule with no hypotheses. Its arbitrary context g permits
extra assumptions, so proofs do not need a separate weakening step.
A first proof, elimination followed by re-introduction:
The currying proof illustrates context handling. Lines l2 and l3 use
ax with extra assumptions. imp_elim combines contexts on l5, then each
imp_intro step moves one assumption into the conclusion:
Excluded middle is not provable here, but its double negation is. Note l7:
not_elim concludes g , h ⊢ ⊥ where g and h are the same
hypothesis. Idempotence collapses the join, so the line can state the
context once:
Quantifiers
The quantifier layer adds a sort of objects, with a variable pool, and the binding syntax:
The substitution operator [x := t] p is an ordinary term with no built-in
meaning. Designated @rewrite equations push it through each connective and
discharge it at atoms, allowing the normalizer to compute substitutions during
rule applications. The @alpha axioms at the end prove the renaming principles
used by the freshness machinery described in Ergonomics.
The four quantifier rules have several additional annotations: @freshen
repairs from Ergonomics, @view/@recover pairs from Views
and recovery, and @auto enrollments from Powering
search. Plain --| lines are doc comments; hover a
rule’s name to read them:
Here all_elim’s conclusion is [x := u] (P x), but l2 states the
normalized form P u, with a witness u from the @vars pool:
Existential elimination can use the bound x itself as the fresh name. The
rule’s dependency constraints ensure that neither the conclusion c nor the
side context h mentions that variable. If x occurs bound in h or c,
alpha-freshening renames it before applying the rule and restores the original
form afterward.