# 31.2 AIntro

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

@n: how we assume “n” is arbitrary.

The new device we need is how to declare that a name is arbitrary. We’ll do it by a new symbol for arbitrariness: @.

We put a name right after it like this: @n.

@n declares that n is an arbitrary name. (It’s a mnemonic initialism: the “a” in the @ symbol stands for arbitrary and the “n” stands for name.)

Up until this point in the textbook, we have been allowing almost every lower case letter from the alphabet to stand for a specific, non-arbitrary object in the domain. For example, we must use a for Alberto, b for Beatrice, and c for Chadwick.

But we reserved the end of the alphabet, like x, y and z, for variables.

Now we’ll do something similar for n and m. We will no longer use those to stand for particular individuals like Neela and Murphy. n and m will still be names, but they will be reserved for arbitrary names.

Rule: for the first arbitrary name we need, we will always use n. If we need a second one in the same proof, we use m.

Here’s the rule: for the first arbitrary name we need, we will always use n. If we need a second one in the same proof, we use m.

If we need more, we just keep going backward from the middle of the alphabet: l, k, j, etc.

We start a AIntro proof by putting @n on the assumption line of a new subproof.

Like the universal generalization (UG) proof method you learned in section 31.1, we start a AIntro proof by assuming that n is arbitrary.

We do that by putting @n on the assumption line of a new subproof.

We then end that subproof by proving that n 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 @n.

Here’s an example.

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

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

The key idea 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 AIntro inference to prove Ax, we must replace all the occurrences of ns with xs.

If the name “n” were to appear in a premise, then it wouldn’t be a truly arbitrary name.

That is why we won’t use n or m to stand for specific individuals anymore.