Is proof of the law of identity a case of circular reasoning?

Question

I am reading "Logic" by Paul Tomassi. While discussing first-order logic in Chapter $6$ p. $310$, he provides the following justification for the inference rule known as identity introduction:

"The intuition which identity introduction exploits is [...] that everything is identical with itself, i.e. the law of identity."

Elsewhere, on p. $311$, he offers proof of the law identity as follows

$\vdash \forall x [x=x]$

$\emptyset \:\:\:$ $1. a=a \:\:\:\:\:\:\:\:\:\:\:\:\:$ =I

$\emptyset \:\:\:$ $2. \forall x [x=x] \:\:\:\:\:\:$ $1$ UI

As you can see, the law of identity is proven using identity introduction, denoted as =I, which exploits the idea that everything is identical to itself, which is in turn expressed by the law of identity. This kind of reasoning appears circular to me.

Can someone bring some clarity? My initial thought is that the law of identity is taken as an axiom of classical logic. However, if that was the case, then why would Tomassi bother offerring a proof of the law identity?

Answer 1

There is a difference between $a=a$ and $\forall x[x=x]$. The second one has a quantifier. Of course passing from one to the other is completely trivial, given the introduction rule for the universal quantifier. So the first one is taken as an axiom, and the second one as a very easy consequence.

Answer 2

I don't understand where you think the circularity is coming from. We have an intuition about equality, namely "everything is equal to itself". We'd like to formalize this intuition as a logical proof rule. There are two reasonable ways to do this:

(1) By a proof rule $({=}I)$, which says that if $t$ is any term, from no hypotheses, we can conclude $t = t$.

(2) By a logical axiom which I'll call $(\mathrm{Ref})$, which says that from no hypotheses, we can conclude $\forall x\,(x = x)$.

Relative to the usual rules for the universal quantifier, these rules are equivalent, in the sense that each can be derived from the other.

Given the proof rule $({=}I)$, we can derive $(\mathrm{Ref})$, by the argument given by Tomassi. Taking $x$ to be a fresh variable, we have $x = x$ by $({=}I)$, and then we have $\forall x\,(x = x)$ by the $\forall$ introduction rule.

On the other hand, given the axiom $(\mathrm{Ref})$, we can derive any instance of $({=}I)$. If $t$ is any term, we have $\forall x\,(x = x)$, and then we have $t = t$ by the $\forall$ elimination rule.

It's no surprise that $({=}I)$ and $(\mathrm{Ref})$ are so trivially interderivable: they both express the same intuitive concept, that everything is equal to itself. There's no circularity here: you have to make a choice of which one to include in your system, and you can motivate either choice by the intuitive "law of identity", and once you've chosen one, you can easily derive the other.

I would actually argue that Tomassi makes the better choice here, in including $({=}I)$ instead of $(\mathrm{Ref})$ as a basic rule. If we decided on $(\mathrm{Ref})$, it would make it look like basic reasoning about equality was somehow entangled with the logic of quantification. From a practical standpoint, we'd like our proof systems to be as "modular" as possible: if we wanted to work with a logic that didn't have the universal quantifier, the rule $({=}I)$ would still work just fine, but the $(\mathrm{Ref})$ axiom would fail to be well-formed.

Answer 3

You have to make a distinction between the idea of the law of identity and its formal logic statement $\forall x \ x=x$. All formal logic statements are just that: a bunch of symbol strings. But they are of course meant to have a certain meaning ... a meaning that reflects the idea that we have in mind for those symbols. We can use formal semantics to provide some further clarity as to this connection between symbols and their meaning, but the point is that you have to distinguish between symbols and their meaning.

The Identity Introduction of $a=a$ is justified based on the idea of the law of identity. That is, the $=I$ rule reflects the idea that anything is identical to itself. One could say that the idea 'justifies' the rule of $=I$, but this is quite different from the kinds of formal rule justifications we use in formal derivations. Indeed, we don't have $\forall x \ x=x$ as a premise, so it is certainly not circular as a formal proof.

Indeed, consider if we were to introduce a single formal rule that says that $\forall x \ x=x$ can be introduced at any point during a proof. Now that is a formal inference rule whose existence is justified by the idea of the law of identity. So if we now use that rule and indeed derive $\forall x \ x=x$ from nothing, would you still complain that this is a circular proof? Because if so, wouldn't that make all rules of formal logic 'circular' in the sense that whatever you do in the rule is justified by an idea that does the same thing?

Answer 4

'a' in a = a refers to the name 'a'.

'x' in ∀x[x=x] refers to the variable 'x'.

Thus, 'a = a' only means that the name 'a' is identical to the name 'a'. What you call something is what you call that something.

On the other hand, "∀x[x=x]" says that for any thing (Tomassi defines a variable as a thing), then that thing is equal to itself.

Assuming that the proof is circular, then the distinction between a variable and a name would have to collapse. Tomassi's distinction between a 'name' and a 'variable' would have to fail, or he had definitions of 'name' and 'variable' such that they could not get distinguished. Tomassi writes on page 195:

"Names plug gaps in predicates and, in so doing, generate sentences"

Variables don't similarly generate sentences. Variables plug gaps in predicates, but what results is not a sentence. "x=x" is unclear in first-order logic, not only literally, but also because no one knows if the intended sentence is ∀x[x=x] or ∃x[x=x]. In a domain of at least two objects, those are different sentences, since ∃x[x=x] could in principle get replaced by recognizing which member of the domain of discourse where that held true, which I'll call '7', and then writing 7=7. But, ∀x[x=x] cannot similarly get replaced, since it refers to more than one object. So, '∀x[x=x]' and '∃x[x=x]' won't lead to the same consequences in most domains, and thus are not equivalent in terms of predictive meaning (or, I think, they are not equivalent in terms of their 'extension'), and so 'x=x' is unclear, and variables and names are distinct.

"As you can see, the law of identity is proven using identity introduction, denoted as =I, which exploits the idea that everything is identical to itself"

Identity introduction only says that a proper name is identical with itself. It doesn't say a word about any thing.

Also, the law of identity ∀x[x=x], can get denied by a sort of Heraclitean philosophy, where every thing is subject to change. At the very least, this post will get subjected to changes in time, and thus tomorrow it won't be the same as it is today (though it's main point and most of it's meaning may remain the same). So, to assert that ∀x[x=x], where 'x' is any statement about it, can get interpreted as false (see the previous sentence in two days from now... the meaning of 'tomorrow' will have changed to a different date on the calendar). However, that the name 'tomorrow' will remain the same, and thus 'a = a' will hold true for this post in it's entirety.