Question about identity axioms

[agapito]

I'm going through Peter Smith's book on Godel's Theorems. He mentions a simple formal theory ("Baby Arithmetic") whose logic needs to prove every instance of 'tau = tau'. Does every 'standard deductive apparatus' include the common identity axioms (e.g. 'x = x')?.

The axioms of "Baby Arithmetic" do not include them, so does this mean they are somewhat hidden in the undefined "standard propositional logic" used? He mentions, for instance, that the theory trivially proves '0 = 0'.

The application of Leibniz' Law is explicitly included, however.

Any help greatly appreciated. Agapito

 

[Evgeny.Makarov]

I'm going through Peter Smith's book on Godel's Theorems. He mentions a simple formal theory ("Baby Arithmetic") whose logic needs to prove every instance of 'tau = tau'. Does every 'standard deductive apparatus' include the common identity axioms (e.g. 'x = x')?

One can consider theories with equality and theories without equality. The first ones include the predicate symbol $=$ and axioms saying that equality is a congruence, i.e., an equivalence relation that is respected by all functions and predicates.

The axioms of "Baby Arithmetic" do not include them, so does this mean they are somewhat hidden in the undefined "standard propositional logic" used?

First, in dealing with arithmetic we are working with predicate, or first-order, logic and not propositional logic. Second, the author does include reflexivity of equality. He says, "our logic needs to prove every instance of $\tau = \tau$ , where $\tau$ is a term of our language $\mathcal{L}_B$. And we need a version of Leibniz’s Law". Reflexivity and Leibniz’s Law are treated similarly. These two axioms (or rules of inference; the author leaves the details unspecified because they are not important) are sufficient for proving that equality is a congruence.

 

[agapito]

Thanks for your thoughtful reply. As I read the text, our logic must prove 'τ=τ', that is we're not using reflexivity as an axiom. We are, however, using Leibniz' Law.

Is it possible therefore to prove '0=0' by only using LL and the 6 axiom schemata of the theory?

Thanks again for helping me out with this.

 

[Evgeny.Makarov]

As I read the text, our logic must prove 'τ=τ', that is we're not using reflexivity as an axiom.

This conclusion is not warranted. One of possible definitions of a derivation (in Hilbert-style axiomatic systems) says: a derivation is a sequence of formulas where each formula is either an axiom or is obtained from two previous formulas by Modus Ponens. That is, axioms are allowed in derivations (of course), and there is no restriction that a derivation cannot end with an axiom. In other words, the fact that $x=x$ is proved does not mean that it is not proved directly by an axiom. In fact, $x=x$ is probably derived from the axiom $\forall x.\,x=x$ using a rule like quantifier elimination or some axiom serving a similar purpose.

Is it possible therefore to prove '0=0' by only using LL and the 6 axiom schemata of the theory?

I don't think so. Reflexivity $\forall x.\,x=x$ and Leibniz's law $\forall x.\,(P(x)\to\forall y\,(x=y\to P(y)))$ are in some sense the opposites of each other: reflexivity says how to prove equality, and LL says how to use it to prove other facts. In the same sense they are similar to pairs of axioms like
\begin{align}
&A\to B\to A\land B\\
&A\land B\to A
\end{align}
and
\begin{align}
&A\to A\lor B\\
&(A\to C)\to(B\to C)\to(A\lor B\to C)
\end{align}
that say how to prove and use conjunction and disjunction, respectively. So I believe both are necessary. But deriving symmetry and transitivity from reflexivity and LL is a nice exercise.

 

[agapito]

Thanks again for your help, it's very useful. I will attempt the exercise you mention. Agapito