MHB Does Every Standard Deductive Apparatus Include Common Identity Axioms?

  • Thread starter Thread starter agapito
  • Start date Start date
  • Tags Tags
    Axioms Identity
AI Thread Summary
The discussion centers on whether every standard deductive apparatus includes common identity axioms, specifically in the context of Peter Smith's "Baby Arithmetic." It is noted that "Baby Arithmetic" does not explicitly include identity axioms like 'x = x', yet it requires proving instances such as 'τ = τ' using Leibniz's Law. The participants clarify that reflexivity and Leibniz's Law serve different roles in proving equality and that reflexivity is not treated as an axiom in this theory. Additionally, it is suggested that while reflexivity is essential for establishing equality, both reflexivity and Leibniz's Law are necessary for a complete understanding of equality in formal logic. The conversation concludes with a plan to explore the derivation of symmetry and transitivity from these principles.
agapito
Messages
46
Reaction score
0
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
 
Technology news on Phys.org
agapito said:
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.

agapito said:
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.
 
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.
 
agapito said:
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.

agapito said:
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.
 
Thanks again for your help, it's very useful. I will attempt the exercise you mention. Agapito
 
Dear Peeps I have posted a few questions about programing on this sectio of the PF forum. I want to ask you veterans how you folks learn program in assembly and about computer architecture for the x86 family. In addition to finish learning C, I am also reading the book From bits to Gates to C and Beyond. In the book, it uses the mini LC3 assembly language. I also have books on assembly programming and computer architecture. The few famous ones i have are Computer Organization and...
I have a quick questions. I am going through a book on C programming on my own. Afterwards, I plan to go through something call data structures and algorithms on my own also in C. I also need to learn C++, Matlab and for personal interest Haskell. For the two topic of data structures and algorithms, I understand there are standard ones across all programming languages. After learning it through C, what would be the biggest issue when trying to implement the same data...
Back
Top