
#1
October 7th, 2019,
16:28
In axioms containg S one invariably finds:
Sx = Sy > x = y
The converse, which characterizes S as a function:
x = y > Sx = Sy
Is never shown. Neither is it shown as an Axiom of FOL or formal Theory of Arithmetic. From the basic axioms and rules of FOL, how does one go about deriving the latter expression formally? Any help or references appreciated. am

October 7th, 2019 16:28
# ADS
Circuit advertisement

#2
October 7th, 2019,
17:21
Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.

#3
October 8th, 2019,
17:03
Thread Author
Originally Posted by
Evgeny.Makarov
Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.
Thanks for responding. All descriptions of Peano Arithmetic I have seen indicate only the converse:
Sx = Sy > x=y
Can you please give me a reference containing
x=y > Sx=Sy
As a Peano axiom?
Many thanks again, am

#4
October 8th, 2019,
17:27
In the book
Peter Smith. An Introduction to Gödel's Theorems. Cambridge University Press: 2013
the description of BA on p. 62 includes Leibniz’s Law. The axiom you are talking about is its special case. Robinson's Arithmetic and Peano Arithmetic are extensions of BA and so inherit this law.
Putting it another way, all theories of arithmetic considered in that book are theories with equality. This means that they include axioms that define properties of =. For the list of axioms see .

#5
October 9th, 2019,
16:33
Thread Author
Originally Posted by
Evgeny.Makarov
In the book
Peter Smith. An Introduction to Gödel's Theorems. Cambridge University Press: 2013
the description of BA on p. 62 includes Leibniz’s Law. The axiom you are talking about is its special case. Robinson's Arithmetic and Peano Arithmetic are extensions of BA and so inherit this law.
Putting it another way, all theories of arithmetic considered in that book are theories with equality. This means that they include axioms that define properties of =. For the list of axioms see
.
Many thanks Evgeny. My interest in this is having a feel for what would be needed by a machine to perform these proofs. Obviously in that case no amount of metalanguage verbiage would help. A machine would have no way of "knowing" whether a certain symbol represents a function or something else to be able to apply the axioms. As an example, could a Turing Machine be programmed to do it?
Thanks again for your valuable help.

#6
October 9th, 2019,
16:44
Originally Posted by
agapito
In axioms containg S one invariably finds:
Sx = Sy > x = y
The converse, which characterizes S as a function:
x = y > Sx = Sy
Is never shown. Neither is it shown as an Axiom of FOL or formal Theory of Arithmetic. From the basic axioms and rules of FOL, how does one go about deriving the latter expression formally? Any help or references appreciated. am
In Landau's Foundations of Analysis, on page 2, he simply incorporates it into his version of the Peano axiom 2, which he phrases as, "For each $x$ there exists exactly one natural number, called the successor of $x$, which will be denoted by $x'.$" The implication $x=y\implies x'=y'$ is a direct consequence of uniqueness.

#7
October 9th, 2019,
17:17
Originally Posted by
agapito
A machine would have no way of "knowing" whether a certain symbol represents a function or something else to be able to apply the axioms. As an example, could a Turing Machine be programmed to do it?
Of course. There are programs called interactive theorem provers, or proof assistants, where you can construct proofs in Peano Arithmetic.