A Hilbert calculus

Each chapter in this part develops a theory, alternating declarations and proofs with explanations. Cells with the same document name share one theory: theory cells add MM0 declarations, and proof cells add theorems and proofs. Editing a cell rechecks its document. Later cells can use earlier declarations in that document.

We start with a small classical system: a Hilbert calculus for propositional logic.

The signature

Two connectives suffice, implication and negation:

Each connective registers its notation twice, giving every Unicode token an ASCII alias that can be typed easily. Negation binds tighter than implication, and implication associates to the right.

The axioms

A Hilbert calculus uses axiom schemes with few inference rules. This theory has three schemes with no hypotheses and one inference rule:

h1 and h2 are the K and S schemes, and h3 is classical contraposition. Modus ponens is the only inference rule. MM0 represents it as an axiom with hypotheses.

Implication is reflexive

Here’s a classic proof of a simple tautology:

Hypothetical syllogism

A theorem’s hypotheses are cited as #1, #2, … like any other reference:

Negation

To shorten the double-negation proofs, we add one more axiom scheme:

con2 is derivable from the three schemes above, but this small development assumes it to keep the example short. Double-negation introduction then takes three lines:

The first line cites imp_refl from earlier on the page. Elimination uses the same pattern with h3:

The whole page

The index lists every statement the page has built, in order, with a marker for each proof obligation. The document behind it is an ordinary .mm0/.auf pair, and everything on the page is live, so you can edit any of the theorems, axioms, or proofs.