Section Progress:

# 30.2 ∀Intro

The formal rule ∀Intro works just like Universal Generalization (UG).

[a]: how we assume “a” is arbitrary.

The new device we need is how to declare that a name is arbitrary. We’ll do it by putting the name in square brackets in a subproof: [a]. We then end that subproof by proving that a has some property, which allows us to infer on the parent proof that the same holds ∀x. We cite the whole subproof with the arbitrary [a].

Here’s an example.

In order for “a” to be allowed as an arbitrary name, it must not appear anywhere outside the subproof.

When we make “a” arbitrary with [a], we must put it in a subproof and justify it with Assume.

The other key fact about arbitrary names is that, when a name is arbitrary, it cannot appear anywhere outside the subproof. For example, it cannot appear in any of the premises or conclusion.

When we make the inference with ∀x, we must replace all the occurrences of xs with a.

If the name “a” does appear in a premise, and you need an arbitrary name, then just choose the next free letter in the alphabet.

30.2 AIntro