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

[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

 

[Evgeny.Makarov]

Peano Arithmetic is a theory with equality, and $x = y\to Sx = Sy$ is one of the axioms of equality.

 

[agapito]

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]

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]

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]

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]

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]

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