The parts of a proof line

Proof lines look like this:

label: $ GOAL $ by rule (bindings) [references]

The label names the line. The goal, between $ signs, is what the line asserts. Everything after by is the justification for the line: the rule being applied, optional bindings in parentheses that assign expressions to the rule’s variables, and optional references in brackets that supply the rule’s hypotheses.

We’ll work in the Hilbert system from the last chapter, extended with the distribution axiom h2:

Three kinds of reference

A reference is a proof of one of the rule’s hypotheses. References can be supplied three ways:

• #1, #2, … indicate the hypotheses of the lemma or theorem being proved, in the order they were declared;
• a label like l1 indicates an earlier line of the same proof;
• an inline application is a rule applied on the spot, inside the brackets, without a line of its own.

As a running example, here’s the usual proof that p -> p, which needs instances of h1, an instance of h2, and two applications of mp.

It checks, but l3 transcribes an axiom instance that the compiler can infer.

Inline applications

When a premise needs only one rule application, you can write that application directly in the reference list. For example:

The second reference, h1 [], applies the axiom in place. The empty brackets say it has no hypotheses of its own. A bare name in a reference list means a line label, so without the brackets h1 would look for a line named h1 rather than the axiom.

Inline applications can be nested, and mixed freely with the other reference kinds. Here is imp_refl again, with the h2 instance and the inner mp folded into the final line:

This version omits the explicit h2 line from the first proof.

When chaining fails

Combining every application into one line can remove formulas that the compiler needs in order to infer bindings. The following cell is intentionally invalid:

The diagnostic says one of h1’s variables could not be determined. Aufbau can only infer what is forced by the goal and the references, and nothing here forces a choice of instance for the first h1 [].

If a variable cannot be determined, you can give the premise its own labeled line, as in imp_refl_chained above, or state the instances yourself with bindings, which work on inline applications the same way they work after by. The single-line proof checks when both h1 applications have explicit bindings:

l1: $ p -> p $ by mp [h1 (a := $ p $, b := $ p $) [],
                      mp [h1 (a := $ p $, b := $ p -> p $) [], h2 []]]

Packing and unpacking

Chains can be unpacked. Place the text cursor on the last line of imp_refl_chained and pause: the lightbulb offers an unpack action that rewrites the line as separate labeled lines, one per inline application, with each goal filled in by the compiler.