# 32.2 =Intro

Remember way back to Chapter 2, when we discussed the three weird cases of validity?

See if you can recall them.

According to the weird cases, a logically true conclusion follows from anything.

Since a=a follows from anything, we can justify it with =Intro without citing any lines.

That fact can help us understand how =Intro works.

Reflexive identity sentences like a=a, b=b, c=c, etc. are FO validities, and therefore also logical truths.

That means we can always validly write a=a in a proof. When we “introduce” a new symbol like that, we use an Intro rule. So we justify it this way:

1. a=a

=Intro

You can use =Intro with any name at all, as long as it is the same name on both sides of the identity.

=Intro has no semicolon and no line numbers.

Notice that =Intro has no semicolon and no line numbers. That is because a=a does not come from any other lines.

Since it can’t possibly be false, it just comes “out of thin air”.

Compare it to justifying a line with “Premise” or “Assume”. Those justifications also don’t need line numbers.

But =Intro is still unique. It is the only Intro or Elim rule for a symbol that doesn’t depend on any previous lines.

You might be wondering: since a=a is so trivial, why would we ever need it?

Here’s one use for it. We know this is a valid argument:

1. a=b
Thus,
2. b=a

Symmetry of identity: if a=b, then b=a.

That is called the symmetry of identity. But we can’t justify that inference with =Elim;1, because the =Elim rule requires citing two different lines.

=Intro to the rescue!

Let’s see if you can figure it out.