Welcome to our community

Be a part of something great, join today!

Proof that S (the successor function) is, in fact a Function.

agapito

Member
Apr 18, 2018
42
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
 

Evgeny.Makarov

Well-known member
MHB Math Scholar
Jan 30, 2012
2,489
Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.
 

agapito

Member
Apr 18, 2018
42
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
 

Evgeny.Makarov

Well-known member
MHB Math Scholar
Jan 30, 2012
2,489
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 Wikipedia.
 

agapito

Member
Apr 18, 2018
42
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 Wikipedia.
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.
 

Ackbach

Indicium Physicus
Staff member
Jan 26, 2012
4,184
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.
 

Evgeny.Makarov

Well-known member
MHB Math Scholar
Jan 30, 2012
2,489
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.
 

agapito

Member
Apr 18, 2018
42
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 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
I posted this same question some time back and it was ably answered by Evgeny and Bachrack. My apologies for this oversight, I should have checked before posting. Agapito