Question on the concept of " Identity "

[Mathelogician]

Hi all;
Look at the attached part from Van Dalen's Logic and structure.
What is he doing exactly?
In axiomatizing 'Identity' as he does, what is gained rather than what we had before (i.e., looking at 'Identity' as a binary predicate)?!
Even in the axioms, he is again using a symbol in the language for identity as a binary predicate (i.e., = ) and then he proves the axioms (or says they are provable) in the language. [note that he also proves I3 and I4 that i haven't shown.]
Thanks.

 

[solakis1]

Hi all;
Look at the attached part from Van Dalen's Logic and structure.
What is he doing exactly?
In axiomatizing 'Identity' as he does, what is gained rather than what we had before (i.e., looking at 'Identity' as a binary predicate)?!
Even in the axioms, he is again using a symbol in the language for identity as a binary predicate (i.e., = ) and then he proves the axioms (or says they are provable) in the language. [note that he also proves I3 and I4 that i haven't shown.]
Thanks.

The axiom I4 is rather an axiom sceme ,because for each "t" and for each "φ" we a corresponding axiom.

Axioms I2 and I3 can be proved using axioms I1 and I4

 

[Mathelogician]

Of course they are axiom schemes; but I'm afraid my question is something else!
Thanks.

 

[Evgeny.Makarov]

When we are talking about semantics (i.e., $\models$), this section may be considered just as an observation that identity satisfies these axioms. The importance of the axioms comes when we consider the derivability relation $\vdash$ (Definition 1.4.2). Then we have to use special axioms or inference rules to say that $=$ is not just an arbitrary predicate symbol.

Axioms I2 and I3 can be proved using axioms I1 and I4

This is true. It is given as an exercise later in the text. The term version of $I_4$ can also be proved from the formula version.